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

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) 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)

Cited in

(only showing first 100 items - show all)

A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
A solution to Curry and Hindley's problem on combinatory strong reduction
On structural properties of eta-expansions of identity
From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality
Applications of infinitary lambda calculus
On the completeness of order-theoretic models of the \(\lambda \)-calculus
A construction of one-point bases in extended lambda calculi
CPS-translation as adjoint
Strong normalization property for second order linear logic
A characterization of F-complete type assignments
Type theories, normal forms, and \(D_{\infty}\)-lambda-models
Substitution revisited
Algebra of constructions. I. The word problem for partial algebras
Principal type scheme and unification for intersection type discipline
Polymorphic type inference and containment
Conditional rewrite rules: Confluence and termination
Lazy variable-renumbering makes substitution cheap
Equivalence of bar recursors in the theory of functionals of finite type
Unique normal forms for lambda calculus with surjective pairing
On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
Generalization from partial parametrization in higher-order type theory
Higher-order rewrite systems and their confluence
A lambda-calculus for dynamic binding
A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\)
Domain theory in logical form
Polymorphic rewriting conserves algebraic strong normalization
A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
Filter models with polymorphic types
An algebraic model of synchronous systems
Conditional rewriting logic as a unified model of concurrency
Complete restrictions of the intersection type discipline
Fairness, distances and degrees
On the adequacy of representing higher order intuitionistic logic as a pure type system
Confluence of the lambda calculus with left-linear algebraic rewriting
An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
The systematic construction of a one-combinator basis for lambda-terms
Adding algebraic rewriting to the untyped lambda calculus
Capturing strong reduction in director string calculus
An interpretation of typed objects into typed -calculus
Full abstractness for a functional/concurrent language with higher-order value-passing
Diagram techniques for confluence
Reaction graph
Structures definable in polymorphism
A conservative look at operational semantics with variable binding
An algebraic generalization of Frege structures -- binding algebras
Semantical analysis of perpetual strategies in -calculus
Orders, reduction graphs and spectra
An algebraic view of the Böhm-out technique
On functions preserving levels of approximation: A refined model construction for various lambda calculi
Decidability of behavioural equivalence in unary PCF
Perpetual reductions in -calculus
Some results on cut-elimination, provable well-orderings, induction and reflection
Typability and type checking in System F are equivalent and undecidable
On -conversion in the -cube and the combination with abbreviations
Type inference, abstract interpretation and strictness analysis
Combinatory reduction systems: Introduction and survey
A type-theoretical alternative to ISWIM, CUCH, OWHY
Combining type disciplines
An internal language for autonomous categories
Confluence by decreasing diagrams
\(F\)-semantics for type assignment systems
Proof-functional connectives and realizability
Embedding -continuous posets in function spaces of domains
Eta-conversion for the languages of explicit substitutions
Semantics of weakening and contraction
Reduction and unification in lambda calculi with a general notion of subtype
Head linear reduction and pure proof net extraction
Algebraic domains of natural transformations
Combining algebraic rewriting, extensional lambda calculi, and fixpoints
A meta-language for typed object-oriented languages
Intersection type assignment systems
On reduction-based process semantics
Normalization results for typeable rewrite systems
Strong normalization from weak normalization in typed \(\lambda\)-calculi
Non-existent Statman's double fixed point combinator does not exist, indeed
On the Jacopini technique
A conjecture on numeral systems
A semantical storage operator theorem for all types
Lambda calculus with explicit recursion
The simply typed theory of \(\beta\)-conversion has no maximum extension
A syntactical proof of the operational equivalence of two -terms
Infinitary lambda calculus
Unifying overloading and \(\lambda\)-abstraction: \(\lambda^{\{\,\}}\)
Revisiting the notion of function
On the strong normalisation of intuitionistic natural deduction with permutation-conversions
The subtyping problem for second-order types is undecidable.
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
A binary modal logic for the intersection types of lambda-calculus.
The semantics of entailment omega
Intersection types and domain operators
Behavioural inverse limit -models
On the relationship between compact regularity and Gentzen's cut rule
Uncomputability: The problem of induction internalized
Generalized filter models
Proof-search in type-theoretic languages: An introduction
Lambda-dropping: Transforming recursive equations into programs with block structure
From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models
On infinite -expansion
A coinductive completeness proof for the equivalence of recursive types
Relating conflict-free stable transition and event models via redex families

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)