Classical lambda calculus in modern dress

Abstract

Recent developments in the categorical foundations of universal algebra have given fresh impetus to an understanding of the lambda calculus coming from categorical logic: an interpretation is a semi-closed algebraic theory. Scott's representation theorem is then completely natural and leads to precise theorems showing the essential equivalence with more familiar notions. Simple abstract proofs of fundamental results in the semantics of the lambda calculus are given.

21 pages, submitted for 90th Birthday of Corrado Bohm Second version accepted by MSCS. Material filled out at the request of referees. Now 28 pages but nothing essentially new

Cited by in corpus (7)

• Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
• A correspondence between rooted planar maps and normal planar lambda terms
• Linear lambda terms as invariants of rooted trivalent maps
• Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
• The linear-non-linear substitution 2-monad
• Braids, twists, trace and duality in combinatory algebras
• Clones, closed categories, and combinatory logic