The Impact of the Lambda Calculus in Logic and Computer Science

DOI10.2307/421013MaRDI QIDQ4359526zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Henk Barendregt

Publication date 20 October 1997

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

Full work available at URL http://hdl.handle.net/2066/17274, http://www.math.ucla.edu/~asl/bsl/0302-toc.htm

zbMATH Keywords

functional programmingcomputationlogiclambda calculus

Mathematics Subject Classification ID

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

Recommendations

• Proofs and programs
• An Introduction to the Lambda Calculus
• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• Models of the lambda calculus: an introduction
• scientific article; zbMATH DE number 4002064

Cites work

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

Cited in

(27)

• The lambda calculus: practice and principle
• What is the Church-Turing Thesis?
• Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
• Russell's 1903 - 1905 Anticipation of the Lambda Calculus
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• Weak consequence relation between -terms
• The classical -calculus characteristics and their application for the effective outcome of the logic equations
• Incorporating quotation and evaluation into Church's type theory
• A computational interpretation of forcing in type theory
• Judgmental and definitional equality from a Fregean perspective
• Models of the lambda calculus: an introduction
• From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
• Untyped lambda-calculus with input-output
• Many more predecessors: a representation workout
• An Essay in λ‐Calculus
• Programming in the λ-Calculus: From Church to Scott and Back
• If structured propositions are logical procedures then how are procedures individuated?
• scientific article; zbMATH DE number 2242116 (Why is no real title available?)
• The calculus of natural calculation
• scientific article; zbMATH DE number 599579 (Why is no real title available?)
• Twin procedures, two kinds of variable binding, and two kinds of computation
• On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
• A system at the cross-roads of functional and logic programming
• A semantic framework for proof evidence
• Why Sets?
• A Constructive Logic for Services and Information Flow in Computer Networks

Describes a project that uses

Uses Software

• LISP
• Automath
• Haskell

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4359526)