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)

Cut-elimination in the strict intersection type assignment system is strongly normalizing
Relative normalization in Deterministic Residual Structures
Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information
Discrimination by parallel observers: the algorithm.
A conjecture on numeral systems
A semantical storage operator theorem for all types
Completeness and partial soundness results for intersection and union typing for $\overline{\lambda}\mu\tilde{\mu}$
The simply typed theory of $\beta$-conversion has no maximum extension
From Böhm's theorem to observational equivalences: an informal account
Combinatory reduction systems with explicit substitution that preserve strong normalisation
Call-by-value lambda calculus as a model of computation in Coq
The theory of contexts for first order and higher order abstract syntax
An interpretation of $\lambda \mu$-calculus in $\lambda$-calculus.
A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser
Dependent types with subtyping and late-bound overloading
Conservation and uniform normalization in lambda calculi with erasing reductions
Perpetuality and uniform normalization in orthogonal rewrite systems
The combinator S
Embeddings between partial combinatory algebras
Ticket Entailment is decidable
Properties of a first-order functional language with sharing
Execution time of λ-terms via denotational semantics and intersection types
scientific article; zbMATH DE number 7453187 (Why is no real title available?)
On infinite -expansion
A fully abstract denotational semantics for the calculus of higher-order communicating systems
Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping
Type system in programming languages
Encoding linear logic with interaction combinators
Lambda-calculus with director strings
On abstract normalisation beyond neededness
Spaces with combinators
A calculus of coroutines
Towards a homotopy domain theory
Reversibility in the higher-order $\pi$-calculus
Type inference with recursive types: Syntax and semantics
Rensets and renaming-based recursion for syntax with bindings
Unifying overloading and $\lambda$-abstraction: $\lambda^{\{\,\}}$
Collapsing partial combinatory algebras
scientific article; zbMATH DE number 3993540 (Why is no real title available?)
The heart of intersection type assignment: Normalisation proofs revisited
A formal system of reduction paths for parallel reduction
Effectful applicative similarity for call-by-name lambda calculi
On randomised strategies in the $\lambda $-calculus
Lambda-calcul, évaluation paresseuse et mise en mémoire
Polymorphic rewriting conserves algebraic strong normalization
Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
Adding Negation to Lambda Mu
Flexible Correct-by-Construction Programming
Automorphisms of types in certain type theories and representation of finite groups
Filter models with polymorphic types
scientific article; zbMATH DE number 1231611 (Why is no real title available?)
A coinductive completeness proof for the equivalence of recursive types
Revisiting the notion of function
A logical aspect of parametric polymorphism
A new proposal of concurrent process calculus
Fairness, distances and degrees
Representing unification in a logical framework
Rewriting with extensional polymorphic $\lambda $-calculus
Lambda-definable term rewriting systems
Asymptotic speedup via effect handlers
A decidable canonical representation of the compact elements in Scott's reflexive domain in $P\omega$
Alpha equivalence equalities
Full intersection types and topologies in lambda calculus
Viewing ${\lambda}$-terms through maps
A note on harmony
A relational semantics for parallelism and non-determinism in a functional setting
Intensional computation with higher-order functions
Principal type scheme and unification for intersection type discipline
A fibrational tale of operational logical relations: pure, effectful and differential
On the observational theory of the CPS-calculus
Higher-order families
Type inference, abstract interpretation and strictness analysis
Game semantics and uniqueness of type inhabitance in the simply-typed $\lambda $-calculus
Realist consequence, epistemic inference, computational correctness
Five axioms of alpha-conversion
Minimal relative normalization in orthogonal expression reduction systems
scientific article; zbMATH DE number 5852776 (Why is no real title available?)
A type assignment for -calculus complete both for FPTIME and strong normalization
Programs as data structures in $\lambda$SF-calculus
Confluence and superdevelopments
Open problems in rewriting
scientific article; zbMATH DE number 5318491 (Why is no real title available?)
Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
Inhabitation for non-idempotent intersection types
Linear numeral systems
(In)efficiency and reasonable cost models
Complete restrictions of the intersection type discipline
Logic and functional programming by retractions
scientific article; zbMATH DE number 7526055 (Why is no real title available?)
An Interaction Net Encoding of Gödel’s System $$\mathcal {T}$$
On the expressiveness of choice quantification
The conflict-free reduction geometry
Adding algebraic rewriting to the untyped lambda calculus
Retractions of dI-domains as a model for Type:Type
The approximation theorem for the $\Lambda_{\mu}$-calculus
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
ARITHMETIC IN THE FORM
Relating conflict-free stable transition and event models via redex families
Consistency argument and classification problem in -calculus
Functional semantics

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)