Journal of Logic and Computation, Volume 11, Issue 3, pp. 363-394: Abstract.
Reviewing the Classical and the de Bruijn Notation for [lambda]-calculus and Pure Type Systems
Department of Computing and Electrical Engineering, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, Scotland. E-mail: email@example.com
This article is a brief review of the type-free [lambda]-calculus and its basic rewriting notions, and of the pure type system framework which generalises many type systems. Both the type-free [lambda]-calculus and the pure type systems are presented using variable names and de Bruijn indices. Using the presentation of the [lambda]-calculus with de Bruijn indices, we illustrate how a calculus of explicit substitutions can be obtained. In addition, de Bruijn's notation for the [lambda]-calculus is introduced and some of its advantages are outlined.
Keywords: Types, rewriting, [lambda], -, calculus, de Bruijn', s notation