Home  Online Resources  Table of Contents

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

Fairouz Kamareddine

Department of Computing and Electrical Engineering, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, Scotland. E-mail: fairouz@cee.hw.ac.uk

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

  Full-Text PDF  (330 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.