Reviewing the classical and the de Bruijn notation for λ-calculus and pure type systems

Research output: Contribution to journalArticle

13 Citations (Scopus)

Abstract

This article is a brief review of the type-free ?-calculus and its basic rewriting notions, and of the pure type system framework which generalises many type systems. Both the type-free ?-calculus and the pure type systems are presented using variable names and de Bruijn indices. Using the presentation of the ?-calculus with de Bruijn indices, we illustrate how a calculus of explicit substitutions can be obtained. In addition, de Bruijn's notation for the ?-calculus is introduced and some of its advantages are outlined.

Original languageEnglish
Pages (from-to)363-394
Number of pages32
JournalJournal of Logic and Computation
Volume11
Issue number3
DOIs
Publication statusPublished - Jun 2001

Keywords

  • λ-calculus and de Bruijn's notation
  • Rewriting
  • Types

Fingerprint Dive into the research topics of 'Reviewing the classical and the de Bruijn notation for λ-calculus and pure type systems'. Together they form a unique fingerprint.

Cite this