The lambda calculus. Its syntax and semantics. Rev. ed.
From MaRDI portal
Publication:801050
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
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)
- Execution time of λ-terms via denotational semantics and intersection types
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Title not available (Why is that?)
- A calculus of coroutines
- Reversibility in the higher-order \(\pi\)-calculus
- The heart of intersection type assignment: Normalisation proofs revisited
- Alpha equivalence equalities
- A note on harmony
- A relational semantics for parallelism and non-determinism in a functional setting
- Title not available (Why is that?)
- Title not available (Why is that?)
- Principal type scheme and unification for intersection type discipline
- Complete restrictions of the intersection type discipline
- A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
- Essential and relational models
- An algebraic generalization of Frege structures -- binding algebras
- Intersection type assignment systems
- Theoretical Pearls:Representing ‘undefined’ in lambda calculus
- CPS-translation as adjoint
- Towards a notion of lambda monoid
- Relational graph models, Taylor expansion and extensionality
- Equivalence of bar recursors in the theory of functionals of finite type
- Classical lambda calculus in modern dress
- Efficient self-interpretation in lambda calculus
- Computational interpretations of linear logic
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- Domain theory in logical form
- Graph easy sets of mute lambda terms
- Normalization, approximation, and semantics for combinator systems
- Higher-order rewrite systems and their confluence
- Game-theoretic analysis of call-by-value computation
- Strong normalization property for second order linear logic
- Intersection types for \(\lambda\)-trees
- Perpetual reductions in \(\lambda\)-calculus
- Typability and type checking in System F are equivalent and undecidable
- Forcing in stable models of untyped \(\lambda\)-calculus
- Combinatory reduction systems: Introduction and survey
- Psi-calculi in Isabelle
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models
- Pure type systems with more liberal rules
- Monoidal computer. I: Basic computability by string diagrams
- Modal objection to naive Leibnizian identity
- Full abstraction for PCF
- Binding in nominal equational logic
- Nominal logic, a first order theory of names and binding
- Simulations in coalgebra
- An internal language for autonomous categories
- The expectation monad in quantum foundations
- From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
- Nominal unification
- Simple consequence relations
- Böhm's theorem for resource lambda calculus through Taylor expansion
- Gödelization in the lambda calculus
- Domain-free \(\lambda\mu\)-calculus
- Bridging Curry and Church's typing style
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- Computation with classical sequents
- Nominal equational logic
- Boolean-like algebras
- Structural recursion with locally scoped names
- Quantum computation: from a programmer's perspective
- A two-valued logic for properties of strict functional programs allowing partial functions
- Linear realizability and full completeness for typed lambda-calculi
- From functional programs to interaction nets via the rewriting calculus
- Easiness in graph models
- On Normalization by Evaluation for Object Calculi
- A Relational Model of a Parallel and Non-deterministic λ-Calculus
- What is a categorical model of the differential and the resource \(\lambda \)-calculi?
- On the strong normalisation of intuitionistic natural deduction with permutation-conversions
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
- A decidable theory of type assignment
- On generic context lemmas for higher-order calculi with sharing
- A General Class of Models of $\mathcal{H}^*$
- Easy lambda-terms are not always simple
- Conditional rewrite rules: Confluence and termination
- SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
- On reduction-based process semantics
- Conditional rewriting logic as a unified model of concurrency
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Normalization results for typeable rewrite systems
- Semantic types and approximation for Featherweight Java
- Graph lambda theories
- Embedding \(\omega\)-continuous posets in function spaces of domains
- Crowd behavior dynamics: entropic path-integral model
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Ticket Entailment is decidable
- 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
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)
