Pure Type Systems Formalized

James McKinna, Robert Pollack

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

Abstract

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 languageEnglish
Title of host publicationTyped Lambda Calculi and Applications. TLCA 1993
PublisherSpringer
Pages289-305
Number of pages17
ISBN (Electronic)9783540475866
ISBN (Print)9783540565178
DOIs
Publication statusPublished - 1993

Publication series

NameLecture Notes in Computer Science
Volume664
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

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

Fingerprint Dive into the research topics of 'Pure Type Systems Formalized'. Together they form a unique fingerprint.

Cite this