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)

An irregular filter model
The geometry of orthogonal reduction spaces
A proof theoretical approach to communication
Some results on extensionality in lambda calculus
On explicit substitution with names
Strong normalization in type systems: A model theoretical approach
Inter-deriving Semantic Artifacts for Object-Oriented Programming
Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
Order-incompleteness and finite lambda reduction models
The logic of message-passing
Taming the merge operator
Operational semantics for declarative multi-paradigm languages
The \(\lambda \)-calculus in the \(\pi \)-calculus
The theory of contexts for first order and higher order abstract syntax
On the confluence of lambda-calculus with conditional rewriting
The variable containment problem
A logic of abstraction related to finite constructive number classes
Semantical analysis of perpetual strategies in \(\lambda\)-calculus
Behavioural inverse limit \(\lambda\)-models
Intersection types and domain operators
A synthetic axiomatization of map theory
A construction of one-point bases in extended lambda calculi
Reflexive objects in topological categories
A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG
A termination ordering for higher order rewrite systems
Collapsing partial combinatory algebras
The self-reduction in lambda calculus
Intersection and union types
Highlights in infinitary rewriting and lambda calculus
Intersection typed \(\lambda \)-calculus
Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
Strong normalization from weak normalization in typed \(\lambda\)-calculi
Combining algebraic rewriting, extensional lambda calculi, and fixpoints
Applications of infinitary lambda calculus
On the completeness of order-theoretic models of the \(\lambda \)-calculus
The systematic construction of a one-combinator basis for lambda-terms
From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality
Towards lambda calculus order-incompleteness
Complete laziness: a natural semantics
Observational program calculi and the correctness of translations
From Böhm's theorem to observational equivalences: an informal account
On the observational theory of the CPS-calculus
Confluence of the lambda calculus with left-linear algebraic rewriting
Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
Algebra of constructions. I. The word problem for partial algebras
A realizability interpretation for intersection and union types
The differential method and the causal incompleteness of programming theory in molecular biology
On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
Functional semantics
Compositional characterisations of \(\lambda\)-terms using intersection types
A meta-language for typed object-oriented languages
Weak linearization of the lambda calculus
Normal-order reduction grammars
On structural properties of eta-expansions of identity
scientific article; zbMATH DE number 7577574 (Why is no real title available?)
Pattern matching as cut elimination
A first-order one-pass CPS transformation
Intersection types for explicit substitutions
Non-existent Statman's double fixed point combinator does not exist, indeed
Generalized filter models
On the power of simple diagrams
On modular properties of higher order extensional lambda calculi
Discrimination by parallel observers: the algorithm.
Intersection types and lambda models
A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\)
A general mathematics of names
Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
Residual theory in λ-calculus: a formal development
An interpretation of typed objects into typed \(\pi\)-calculus
Normalization without reducibility
Completeness of type assignment systems with intersection, union, and type quantifiers
Setting the facts straight
Fair ambients
Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
Nominal rewriting
Bunder's paradox
Categorical pairs and the indicative shift
Computability in higher types, P\(\omega\) and the completeness of type assignment
Three Syntactic Theories for Combinatory Graph Reduction
Parallel beta reduction is not elementary recursive
The mechanisation of Barendregt-style equational proofs (the residual perspective)
Productivity of stream definitions
Confluence by decreasing diagrams
On equal \(\mu \)-terms
Viewing \({\lambda}\)-terms through maps
A Mechanized Model of the Theory of Objects
Lambda-calculus with director strings
A Polymorphic Type System for the Lambda-Calculus with Constructors
Local Termination
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
Filter models for conjunctive-disjunctive \(\lambda\)-calculi
A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
Head linear reduction and pure proof net extraction
The λ-calculus with constructors: Syntax, confluence and separation
First-class patterns
Adding algebraic rewriting to the untyped lambda calculus
Rewriting strategies and strategic rewrite programs
Context rewriting

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)