The lambda calculus. Its syntax and semantics. Rev. ed.

zbMATH Open0551.03007MaRDI QIDQ801050FDOQ801050

Authors: Henk Barendregt 

Publication date: 1984

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 6148924
• scientific article
• scientific article; zbMATH DE number 783760
• scientific article; zbMATH DE number 3875232
• scientific article; zbMATH DE number 46869

zbMATH Keywords

semanticsmodelssyntaxreduction systemstype-free lambda calculus

Mathematics Subject Classification ID

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) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)

Cited In (only showing first 100 items - show all)

• Properties of a first-order functional language with sharing
• Lambda-calculus with director strings
• Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
• Higher-order families
• Viewing \({\lambda}\)-terms through maps
• Programs as data structures in \(\lambda\)SF-calculus
• Adding algebraic rewriting to the untyped lambda calculus
• Infinitary lambda calculi and böhm models
• A semantic proof of polytime soundness of light affine logic
• Filter models for conjunctive-disjunctive \(\lambda\)-calculi
• Substitution revisited
• On equal \(\mu \)-terms
• Rewriting strategies and strategic rewrite programs
• Type inference in polymorphic type discipline
• A Church-style intermediate language for ML\(^{\text F}\)
• Internal models of system F for decompilation
• On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation
• Context rewriting
• The subtyping problem for second-order types is undecidable.
• A simplified proof of the Church-Rosser theorem
• Productivity of stream definitions
• Call-by-value non-determinism in a linear logic type discipline
• A Mechanized Model of the Theory of Objects
• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
• Residual theory in λ-calculus: a formal development
• Computability in higher types, P\(\omega\) and the completeness of type assignment
• Confluence of the coinductive \(\lambda\)-calculus
• An interpretation of typed objects into typed \(\pi\)-calculus
• Categorical pairs and the indicative shift
• Semantics of weakening and contraction
• A characterization of F-complete type assignments
• Polymorphic type inference and containment
• Continuous monoids and semirings
• On the membership problem for non-linear abstract categorial grammars
• Synthesizable high level hardware descriptions
• Infinitary lambda calculus
• The semantics of entailment omega
• Bisimilarity of open terms.
• A metamodel of access control for distributed environments: applications and properties
• Confluence by decreasing diagrams
• Head linear reduction and pure proof net extraction
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• A category-theoretic characterization of functional completeness
• Weak typed Böhm theorem on IMLL
• First-class patterns
• The semantics of second-order lambda calculus
• Building continuous webbed models for system F
• Intersection type assignment systems with higher-order algebraic rewriting
• The sequentially realizable functionals
• A full continuous model of polymorphism
• Infinitary lambda calculus and discrimination of Berarducci trees.
• Combining type disciplines
• Local Termination
• Setting the facts straight
• Fair ambients
• Bunder's paradox
• Nominal rewriting
• Strong normalisation in the \(\pi\)-calculus
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• The λ-calculus with constructors: Syntax, confluence and separation
• Pointfree expression and calculation: From quantification to temporal logic
• A general mathematics of names
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Strongly normalising cut-elimination with strict intersection types
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• Title not available (Why is that?)
• The search for a reduction in combinatory logic equivalent to \(\lambda \beta\)-reduction. II.
• Three Syntactic Theories for Combinatory Graph Reduction
• On tree automata that certify termination of left-linear term rewriting systems
• Normalization without reducibility
• Parallel beta reduction is not elementary recursive
• Kernel-LEAF: A logic plus functional language
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Aspects of categorical recursion theory
• Call-by-value Solvability
• Descendants and origins in term rewriting.
• Development closed critical pairs
• The theory of contexts for first order and higher order abstract syntax
• Collapsing partial combinatory algebras
• A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\)
• On the observational theory of the CPS-calculus
• Functional semantics
• Algebra of constructions. I. The word problem for partial algebras
• Compositional characterisations of \(\lambda\)-terms using intersection types
• Weak linearization of the lambda calculus
• Strong normalization in type systems: A model theoretical approach
• Operational semantics for declarative multi-paradigm languages
• The variable containment problem
• On the confluence of lambda-calculus with conditional rewriting
• Intersection typed \(\lambda \)-calculus
• On modular properties of higher order extensional lambda calculi
• The self-reduction in lambda calculus
• Confluence of the lambda calculus with left-linear algebraic rewriting
• A proof theoretical approach to communication
• From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality
• Observational program calculi and the correctness of translations
• On the power of simple diagrams

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)