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)
- 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
- Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
- On structural properties of eta-expansions of identity
- Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
- Taming the merge operator
- Reflexive objects in topological categories
- Applications of infinitary lambda calculus
- On the completeness of order-theoretic models of the \(\lambda \)-calculus
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- A construction of one-point bases in extended lambda calculi
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- A meta-language for typed object-oriented languages
- Non-existent Statman's double fixed point combinator does not exist, indeed
- The geometry of orthogonal reduction spaces
- The systematic construction of a one-combinator basis for lambda-terms
- A synthetic axiomatization of map theory
- Intersection and union types
- A realizability interpretation for intersection and union types
- Title not available (Why is that?)
- Pattern matching as cut elimination
- A first-order one-pass CPS transformation
- Intersection types for explicit substitutions
- On explicit substitution with names
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- Towards lambda calculus order-incompleteness
- Order-incompleteness and finite lambda reduction models
- A logic of abstraction related to finite constructive number classes
- A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG
- A termination ordering for higher order rewrite systems
- Highlights in infinitary rewriting and lambda calculus
- Some results on extensionality in lambda calculus
- Inter-deriving Semantic Artifacts for Object-Oriented Programming
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- The logic of message-passing
- The \(\lambda \)-calculus in the \(\pi \)-calculus
- Intersection types and lambda models
- An irregular filter model
- Complete laziness: a natural semantics
- The differential method and the causal incompleteness of programming theory in molecular biology
- Semantical analysis of perpetual strategies in \(\lambda\)-calculus
- Behavioural inverse limit \(\lambda\)-models
- Intersection types and domain operators
- Normal-order reduction grammars
- Generalized filter models
- From Böhm's theorem to observational equivalences: an informal account
- Discrimination by parallel observers: the algorithm.
- 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
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)
