# Re: Questions on LU and ITT



> 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)