The lambda calculus. Its syntax and semantics. Rev. ed.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)
This revised version of the lambda calculus book by H. Barendregt can be considered as a fundamental work in the subject (for a review of the first edition (1981) see [Zbl 0467.03010]). The various aspects of that calculus have been explored and explained: conversion, reduction, theories and models. After the classical books by \textit{H. B. Curry} and \textit{R. Feys} [Combinatory logic. Vol. I (1958; Zbl 0081.241)] and \textit{H. B. Curry}, \textit{J. R. Hindley}, \textit{J. P. Seldin} [Combinatory logic. Vol. II (1972; Zbl 0242.02029)], the lambda calculus community finds in Barendregt's book a very interesting and comprehensive account of what has been done in the area, especially during the 70's and the early 80's. The revised edition of that book gives a closer look at the models of lambda calculus and includes recent results. Another reference for persons interested in the subject is \textit{J. W. Klop's} work: [Combinatory reduction systems (1980; Zbl 0466.03006)].
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
- A solution to Curry and Hindley's problem on combinatory strong reduction
- On structural properties of eta-expansions of identity
- From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality
- Applications of infinitary lambda calculus
- On the completeness of order-theoretic models of the \(\lambda \)-calculus
- A construction of one-point bases in extended lambda calculi
- CPS-translation as adjoint
- Strong normalization property for second order linear logic
- A characterization of F-complete type assignments
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Substitution revisited
- Algebra of constructions. I. The word problem for partial algebras
- Principal type scheme and unification for intersection type discipline
- Polymorphic type inference and containment
- Conditional rewrite rules: Confluence and termination
- Lazy variable-renumbering makes substitution cheap
- Equivalence of bar recursors in the theory of functionals of finite type
- Unique normal forms for lambda calculus with surjective pairing
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- Generalization from partial parametrization in higher-order type theory
- Higher-order rewrite systems and their confluence
- A lambda-calculus for dynamic binding
- A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\)
- Domain theory in logical form
- Polymorphic rewriting conserves algebraic strong normalization
- A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
- Filter models with polymorphic types
- An algebraic model of synchronous systems
- Conditional rewriting logic as a unified model of concurrency
- Complete restrictions of the intersection type discipline
- Fairness, distances and degrees
- On the adequacy of representing higher order intuitionistic logic as a pure type system
- Confluence of the lambda calculus with left-linear algebraic rewriting
- An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
- The systematic construction of a one-combinator basis for lambda-terms
- Adding algebraic rewriting to the untyped lambda calculus
- Capturing strong reduction in director string calculus
- An interpretation of typed objects into typed -calculus
- Full abstractness for a functional/concurrent language with higher-order value-passing
- Diagram techniques for confluence
- Reaction graph
- Structures definable in polymorphism
- A conservative look at operational semantics with variable binding
- An algebraic generalization of Frege structures -- binding algebras
- Semantical analysis of perpetual strategies in -calculus
- Orders, reduction graphs and spectra
- An algebraic view of the Böhm-out technique
- On functions preserving levels of approximation: A refined model construction for various lambda calculi
- Decidability of behavioural equivalence in unary PCF
- Perpetual reductions in -calculus
- Some results on cut-elimination, provable well-orderings, induction and reflection
- Typability and type checking in System F are equivalent and undecidable
- On -conversion in the -cube and the combination with abbreviations
- Type inference, abstract interpretation and strictness analysis
- Combinatory reduction systems: Introduction and survey
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Combining type disciplines
- An internal language for autonomous categories
- Confluence by decreasing diagrams
- \(F\)-semantics for type assignment systems
- Proof-functional connectives and realizability
- Embedding -continuous posets in function spaces of domains
- Eta-conversion for the languages of explicit substitutions
- Semantics of weakening and contraction
- Reduction and unification in lambda calculi with a general notion of subtype
- Head linear reduction and pure proof net extraction
- Algebraic domains of natural transformations
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- A meta-language for typed object-oriented languages
- Intersection type assignment systems
- On reduction-based process semantics
- Normalization results for typeable rewrite systems
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Non-existent Statman's double fixed point combinator does not exist, indeed
- On the Jacopini technique
- A conjecture on numeral systems
- A semantical storage operator theorem for all types
- Lambda calculus with explicit recursion
- The simply typed theory of \(\beta\)-conversion has no maximum extension
- A syntactical proof of the operational equivalence of two -terms
- Infinitary lambda calculus
- Unifying overloading and \(\lambda\)-abstraction: \(\lambda^{\{\,\}}\)
- Revisiting the notion of function
- On the strong normalisation of intuitionistic natural deduction with permutation-conversions
- The subtyping problem for second-order types is undecidable.
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- A binary modal logic for the intersection types of lambda-calculus.
- The semantics of entailment omega
- Intersection types and domain operators
- Behavioural inverse limit -models
- On the relationship between compact regularity and Gentzen's cut rule
- Uncomputability: The problem of induction internalized
- Generalized filter models
- Proof-search in type-theoretic languages: An introduction
- Lambda-dropping: Transforming recursive equations into programs with block structure
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- On infinite -expansion
- A coinductive completeness proof for the equivalence of recursive types
- Relating conflict-free stable transition and event models via redex families
This page was built for publication: The lambda calculus. Its syntax and semantics. Rev. ed.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q801050)
