Re: Questions on LU and ITT

• To: linear@cs.stanford.edu
• Subject: Re: Questions on LU and ITT
• From: David J Pym <dpym@dcs.edinburgh.ac.uk>
• Date: Thu, 13 May 93 16:53:27 BST
• Approved: types@dcs.gla.ac.uk

> I seem to have evermore questions as I learn more about proof theory, linear
> logic and LU.
> 
> 1.  Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been
>     published?

My 1990 University of Edinburgh Ph.D. thesis contains, amongst other
things, a sequent calculus for the lambdaPi-calculus, a theory of
first-order dependent function types (just Pi, no Sigma, a fragment of ITT).

This is discussed, as part of a different analysis, in 

``Proof-search in the $\lambda\Pi$-calculus'', by D.J. Pym and L.A. Wallen.
In: Logical Frameworks, Gerard Huet and Gordon Plotkin (editors), 
Cambridge University Press, 1991. 

I have just submitted a paper, ``A Note on the Proof Theory of the 
$\lambda\Pi$-calculus'' to a journal. This paper discusses the 
sequent calculus for lambdaPi and some resolution calculi that 
arise from it. 

I am preparing papers on these sorts of issues for Sigma types and 
also for PTSs. 

> 
> (This message was earlier posted to the logic mailing 
>  list, but no responses were received.)
>

I read this list, but didn't get this message. 

Sincerely, 

David. 


(I believe he is referring to "logic@cs.cornell.edu" moderated 
 by Bard Bloom.  I received his earlier message to that list.
 - Patrick Lincoln, linear mod)

• Prev: IL -- LU -- LL
• Next: New book on TERM GRAPH REWRITING
• Index(es):
  • Main
  • Thread