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^{\{\,\}}\)
- Title not available (Why is that?)
- 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
- 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
- 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
- Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices
- 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
- A fully abstract denotational semantics for the calculus of higher-order communicating systems
- On abstract normalisation beyond neededness
- Spaces with combinators
- Type inference with recursive types: Syntax and semantics
- Title not available (Why is that?)
- Title not available (Why is that?)
- Lazy Lambda calculus: Theories, models and local structure characterization
- Polymorphic rewriting conserves algebraic strong normalization
- Filter models with polymorphic types
- Fairness, distances and degrees
- Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
- Type inference, abstract interpretation and strictness analysis
- A Filter Model for the λμ-Calculus
- On the construction of stable models of untyped \(\lambda\)-calculus
- Retractions of dI-domains as a model for Type:Type
- Opérateurs de mise en mémoire et types $\forall $-positifs
- Simplifying the signature in second-order unification
- Sharing in the graph rewriting calculus
- A faithful representation of non-associative Lambek grammars in abstract categorial grammars
- Unique normal forms for lambda calculus with surjective pairing
- An investigation into functions as processes
- A lambda-calculus for dynamic binding
- Normal forms in combinatory logic
- Transfinite reductions in orthogonal term rewriting systems
- An initial algebra approach to term rewriting systems with variable binders
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Expressing combinatory reduction systems derivations in the rewriting calculus
- A conservative look at operational semantics with variable binding
- A \(\rho\)-calculus of explicit constraint application
- Type inference with simple subtypes
- Local bigraphs and confluence: two conjectures (extended abstract)
- λν, a calculus of explicit substitutions which preserves strong normalisation
- The Prismoid of Resources
- On the expressive power of abstract categorial grammars: Representing context-free formalisms
- Innocent game models of untyped \(\lambda\)-calculus
- Higher order unification via explicit substitutions
- Safety of Nöcker's strictness analysis
- On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa
- Lambda calculus with explicit recursion
- The stream-based service-centred calculus: a foundation for service-oriented programming
- De Bruijn's weak diamond property revisited
- N. G. de Bruijn's contribution to the formalization of mathematics
- A solution to Curry and Hindley's problem on combinatory strong reduction
- Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
- Type checking a multithreaded functional language with session types
- A semantics for type checking
- An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
- External and internal syntax of the \(\lambda \)-calculus
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
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)
