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$
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
A fully abstract denotational semantics for the calculus of higher-order communicating systems
An abstract monadic semantics for value recursion
A computable expression of closure to efficient causation
The Prismoid of Resources
Higher order unification via explicit substitutions
A Filter Model for the λμ-Calculus
Type checking a multithreaded functional language with session types
De Bruijn's syntax and reductional behaviour of $\lambda$-terms: the untyped case
Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
Local bigraphs and confluence: two conjectures (extended abstract)
A variadic extension of Curry's fixed-point combinator
The stream-based service-centred calculus: a foundation for service-oriented programming
Normal forms in combinatory logic
De Bruijn's weak diamond property revisited
N. G. de Bruijn's contribution to the formalization of mathematics
Transfinite reductions in orthogonal term rewriting systems
Resource operators for $\lambda$-calculus
A semantic basis for Quest
On abstract normalisation beyond neededness
A confluent reduction for the extensional typed $\lambda$-calculus with pairs, sums, recursion and terminal object
On the construction of stable models of untyped $\lambda$-calculus
Retractions of dI-domains as a model for Type:Type

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)