Type Inference using Sequent Calculus formulation of IPL

• To: types
• Subject: Type Inference using Sequent Calculus formulation of IPL
• From: Sanjiva Prasad <sanjiva@ecrc.de>
• Date: Thu, 27 Aug 92 10:59:57 EDT
• Sender: meyer@theory.lcs.mit.edu

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

• Prev: ISABELLE-92
• Next: Two papers on object-oriented programming
• Index(es):
  • Main
  • Thread