Type Inference using Sequent Calculus formulation of IPL

Article View: fj.mail-lists.types

Article #24

Back to fj.mail-lists.types Previous Next

#24

From: 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

Technical Details

Message-ID: <314446@nttlab.ntt.JP>

Path:

arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-snd-ss2!akiu!hakata!kudpc!nuis!tutgw!lab!nttlab!daemon

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!stanford.edu!sun-barr!sh.wide!wnoc-snd-ss2!akiu!hakata!kudpc!nuis!tutgw!lab!nttlab!daemon
From: sanjiva@ecrc.de
Newsgroups: fj.mail-lists.types
Subject: Type Inference using Sequent Calculus formulation of IPL
Message-ID: <314446@nttlab.ntt.JP>
Date: 27 Aug 92 15:53:21 GMT
Sender: daemon@nttlab.ntt.JP
Distribution: fj
Lines: 12
Approved: news@nttlab.ntt