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\)
Intersection types for the resource control lambda calculi
A proof of the substitution lemma in de Bruijn's notation
Strong storage operators and data types
Normalization by Evaluation for Typed Weak lambda-Reduction
Lambda-dropping: Transforming recursive equations into programs with block structure
Encoding linear logic with interaction combinators
Intensional computation with higher-order functions
Normalisation for higher-order calculi with explicit substitutions
Full abstraction for polymorphic \(\pi \)-calculus
A conjecture on numeral systems
A semantical storage operator theorem for all types
Nominal unification with atom and context variables
The simply typed theory of \(\beta\)-conversion has no maximum extension
Ranking/unranking of lambda terms with compressed de Bruijn indices
Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
Storage Operators and ∀‐positive Types in TTR Type System
On the relationship between compact regularity and Gentzen's cut rule
Uncomputability: The problem of induction internalized
The Church-Rosser theorem and quantitative analysis of witnesses
On the Jacopini technique
A cartesian closed category in Martin-Löf's intuitionistic type theory
On the number of unary-binary tree-like structures with restrictions on the unary height
Normalization by Evaluation for Martin-Löf Type Theory with One Universe
Proof-search in type-theoretic languages: An introduction
Fixed points in lambda calculus. an eccentric survey of problems and solutions
A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
Monoidal computer. III: A coalgebraic view of computability and complexity (extended abstract)
A binary modal logic for the intersection types of lambda-calculus.
Infinitary rewriting: closure operators, equivalences and models
Relating conflict-free stable transition and event models via redex families
Consistency argument and classification problem in \(\lambda\)-calculus
Bounded Linear Logic, Revisited
Denotational semantics of membrane systems by using complete metric spaces
A sequent calculus for subtyping polymorphic types
A core model for choreographic programming

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)