Type Inference using Sequent Calculus formulation of IPL

Thread View: fj.mail-lists.types

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by sanjiva Thu, 27 Aug 1992 15:53

#24

Author: sanjiva
Date: Thu, 27 Aug 1992 15:53

12 lines
862 bytes

Date: Thu, 27 Aug 92 14:53:27 +0200

Is there a reference in the existing literature where a type
inference algorithm for a functional language (with ML-like
polymorphism) is based on the Sequent Calculus formulation
of Intuitionistic Propositional Logic, rather than on the
Natural Deduction formulation?  If yes, how does it handle the
cases where the subformula property doesn't hold (in the
Implies-left rule for example)?

Thanks,
Sanjiva				sanjiva@ecrc.de

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads