Pure type systems with de Bruijn indices

Fairouz Kamareddine, Alejandro Ríos

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been introduced independently by Terlouw and Berardi in order to provide a unified formalism in which many type systems can be represented. In particular, PTSs allow the representation of the simple theory of types, the polymophic theory of types, the dependent theory of types and various other well-known type systems such as the Edinburgh Logical Frameworks and the Automath system. PTSs are usually presented using variable names. In this article, we present a formulation of PTSs with de Bruijn indices. De Bruijn indices avoid the problems caused by variable names during the implementation of type systems. We show that PTSs with variable names and PTSs with de Bruijn indices are isomorphic. This isomorphism enables us to answer questions about PTSs with de Bruijn indices including confluence, termination (strong normalization) and safety (subject reduction).

Original languageEnglish
Pages (from-to)187-201
Number of pages15
JournalComputer Journal
Volume45
Issue number2
DOIs
Publication statusPublished - 2002

Fingerprint Dive into the research topics of 'Pure type systems with de Bruijn indices'. Together they form a unique fingerprint.

  • Cite this