The Impact of the Lambda Calculus in Logic and Computer Science

DOI10.2307/421013zbMath0887.03008OpenAlexW2095378146WikidataQ63044203 ScholiaQ63044203MaRDI QIDQ4359526

Hendrik Pieter Barendregt

Publication date: 20 October 1997

Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/17274

zbMATH Keywords

logicfunctional programminglambda calculuscomputation

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items (13)

What is the Church-Turing Thesis? ⋮ Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants ⋮ Unnamed Item ⋮ Many more predecessors: A representation workout ⋮ A semantic framework for proof evidence ⋮ Programming in the λ-Calculus: From Church to Scott and Back ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Why Sets? ⋮ Russell's 1903 - 1905 Anticipation of the Lambda Calculus ⋮ If structured propositions are logical procedures then how are procedures individuated? ⋮ The calculus of natural calculation ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ A Computational Interpretation of Forcing in Type Theory

Uses Software

• Haskell
• Automath
• LISP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The categorical abstract machine
• The calculus of constructions
• Language in action. Categories, lambdas and dynamic logic
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A theory of type polymorphism in programming
• The typed lambda-calculus is not elementary recursive
• Untersuchungen über das logische Schliessen. II
• Enumerators of lambda terms are reducing constructively
• The inconsistency of certain formal logics
• \(\lambda\)-definability and recursiveness
• Models of the lambda calculus
• The Category-Theoretic Solution of Recursive Domain Equations
• Can programming be liberated from the von Neumann style?
• A new implementation technique for applicative languages
• Functionality in Combinatory Logic
• Efficient self-interpretation in lambda calculus
• Modified basic functionality in combinatory logic
• The Mechanical Evaluation of Expressions
• The theory of classes A modification of von Neumann's system
• Computability and λ-definability
• A formulation of the simple theory of types

This page was built for publication: The Impact of the Lambda Calculus in Logic and Computer Science