Journal of Logic and Computation, Volume 11, Issue 3, pp. 363394: Abstract.
Reviewing the Classical and the de Bruijn Notation for [lambda]calculus and Pure Type SystemsFairouz Kamareddine^{} ^{}Department of Computing and Electrical Engineering, HeriotWatt University, Riccarton, Edinburgh EH14 4AS, Scotland. Email: fairouz@cee.hw.ac.uk
This article is a brief review of the typefree [lambda]calculus and its basic rewriting notions, and of the pure type system framework which generalises many type systems. Both the typefree [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
