Substitution in the lambda Calculus and the role of the Curry School

Research output: Chapter in Book/Report/Conference proceedingChapter


Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the  lambda calculus, we cannot define congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of  alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution.
Original languageEnglish
Title of host publicationA Century since Principia's Substitution Bedazzled Haskell Curry
Subtitle of host publicationIn Honour of Jonathan Seldin's 80th Anniversary
Place of PublicationLondon
PublisherCollege Publications
Number of pages34
ISBN (Print)9781848904361
Publication statusPublished - 11 Jul 2023

Publication series

PublisherCollege Publications

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)


Dive into the research topics of 'Substitution in the lambda Calculus and the role of the Curry School'. Together they form a unique fingerprint.

Cite this