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

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.