Pure Type Systems Formalized

James McKinna, Robert Pollack

Research output: Chapter in Book/Report/Conference proceedingConference contribution


In doing this work of formalizing a well known body of mathematics, we spent a large amount of time solving mathematical problems, e.g. the Thinning Lemma. Another big problem was maintaining and organizing the formal knowledge, e.g. allowing two people to extend different parts of the data base at the same time, and finding the right lemma in the mass of checked material. We feel that better understanding of mathematical issues of formalization (e.g. names/namefree, intentional/extentional), and organization of formal development are the most useful areas to work on now for the long-term goal of formal mathematics.

Finally, it is not so easy to understand the relationship between some informal mathematics and a claimed formalization of it. Are you satisfied with our definition of reduction? It might be more satisfying if we also defined de Bruijn terms and their reduction, and proved a correspondence between the two representations, but this only changes the degree of the problem, not its nature. What about the choice between the typing rules Lda and Lda'? There may be no “right” answer, as we may have different ideas in mind informally. There is no such thing as certain truth, and formalization does not change this state of affairs.
Original languageUndefined/Unknown
Title of host publicationTyped Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings
EditorsM. Bezem, J.F. Groote
PublisherSpringer Berlin
Number of pages17
ISBN (Electronic)978-3-540-47586-6
ISBN (Print)978-3-540-56517-8
Publication statusPublished - 18 Mar 1993
EventInternational Conference on Typed Lambda Calculi and Applications TLCA'93 - Utrecht, Netherlands
Duration: 16 Mar 199318 Apr 1993
Conference number: 1


ConferenceInternational Conference on Typed Lambda Calculi and Applications TLCA'93
Abbreviated titleTLCA 1993
Internet address


  • Type Theory
  • Typing Rule
  • Inductive Type
  • Structural Induction
  • Lambda Calculus

Cite this