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

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)

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

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)