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)
- A conjecture on numeral systems
- A semantical storage operator theorem for all types
- The simply typed theory of \(\beta\)-conversion has no maximum extension
- On infinite \(\eta\)-expansion
- Encoding linear logic with interaction combinators
- Unifying overloading and \(\lambda\)-abstraction: \(\lambda^{\{\,\}}\)
- A coinductive completeness proof for the equivalence of recursive types
- Revisiting the notion of function
- Intensional computation with higher-order functions
- Relating conflict-free stable transition and event models via redex families
- Consistency argument and classification problem in \(\lambda\)-calculus
- A sequent calculus for subtyping polymorphic types
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Projections for infinitary rewriting
- Strong normalization through intersection types and memory
- Functions-as-constructors higher-order unification: extended pattern unification
- Multityped abstract categorial grammars and their composition
- Ranking/unranking of lambda terms with compressed de Bruijn indices
- The Church-Rosser theorem and quantitative analysis of witnesses
- A cartesian closed category in Martin-Löf's intuitionistic type theory
- A binary modal logic for the intersection types of lambda-calculus.
- On the relationship between compact regularity and Gentzen's cut rule
- Uncomputability: The problem of induction internalized
- Full abstraction for polymorphic \(\pi \)-calculus
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Call-by-value combinatory logic and the lambda-value calculus
- Intersection types for the resource control lambda calculi
- Title not available (Why is that?)
- Rule-based transformation of graph rewriting rules: towards higher-order graph grammars
- Comparing higher-order encodings in logical frameworks and tile logic
- Normalisation for higher-order calculi with explicit substitutions
- Nominal unification with atom and context variables
- The interpretation of unsolvable λ-terms in models of untyped λ-calculus
- Normalization by Evaluation for Typed Weak lambda-Reduction
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- Monoidal computer. III: A coalgebraic view of computability and complexity (extended abstract)
- A proof of the substitution lemma in de Bruijn's notation
- Strong storage operators and data types
- Storage Operators and ∀‐positive Types in TTR Type System
- Denotational semantics of membrane systems by using complete metric spaces
- Fixed points in lambda calculus. an eccentric survey of problems and solutions
- A core model for choreographic programming
- Explicit cyclic substitutions
- On the number of unary-binary tree-like structures with restrictions on the unary height
- Infinitary rewriting: closure operators, equivalences and models
- Proof-search in type-theoretic languages: An introduction
- Bounded Linear Logic, Revisited
- On the Jacopini technique
- Relative normalization in Deterministic Residual Structures
- Lambda-dropping: Transforming recursive equations into programs with block structure
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
- 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
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)
