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

03-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations

03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations

68Q55: Semantics in the theory of computing

68Q65: Abstract data types; algebraic specification

03B40: Combinatory logic and lambda calculus

Related Items

Building domains from graph models, 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 $\lambda$-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 $\lambda$-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 $\eta$-expansion, A coinductive completeness proof for the equivalence of recursive types, Relating conflict-free stable transition and event models via redex families, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Consistency argument and classification problem in $\lambda$-calculus, De Bruijn's syntax and reductional behaviour of $\lambda$-terms: the untyped case, Some results on extensionality in lambda calculus, Normalisation for higher-order calculi with explicit substitutions, On the expressive power of abstract categorial grammars: Representing context-free formalisms, Lambda-calculus with director strings, Comparing and implementing calculi of explicit substitutions with eta-reduction, A proof of the substitution lemma in de Bruijn's notation, Strong storage operators and data types, Building continuous webbed models for system F, Normalization without reducibility, The sequentially realizable functionals, Skew confluence and the lambda calculus with letrec, An interpretation of $\lambda \mu$-calculus in $\lambda$-calculus., A cartesian closed category in Martin-Löf's intuitionistic type theory, A full continuous model of polymorphism, Normalization, approximation, and semantics for combinator systems, Discrimination by parallel observers: the algorithm., Bisimilarity of open terms., Higher order unification via explicit substitutions, The combinator S, Descendants and origins in term rewriting., Full abstraction for PCF, Perpetuality and uniform normalization in orthogonal rewrite systems, A sequent calculus for subtyping polymorphic types, Dependent types with subtyping and late-bound overloading, Parallel beta reduction is not elementary recursive, A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser, Encoding linear logic with interaction combinators, Intersection and singleton type assignment characterizing finite Böhm-trees, Conservation and uniform normalization in lambda calculi with erasing reductions, On the expressiveness of choice quantification, Infinitary lambda calculus and discrimination of Berarducci trees., Pattern matching as cut elimination, Nominal unification, A first-order one-pass CPS transformation, Adapting innocent game models for the Böhm tree $\lambda$-theory, Order-incompleteness and finite lambda reduction models, Confluence of the coinductive $\lambda$-calculus, Limiting partial combinatory algebras, Intersection types for explicit substitutions, Nominal logic, a first order theory of names and binding, Infinite intersection types, Strong normalization in type systems: A model theoretical approach, OTTER experiments in a system of combinatory logic, Some results on numerical systems in $\lambda$-calculus, Normal forms in combinatory logic, Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping, Game-theoretic analysis of call-by-value computation, The self-reduction in lambda calculus, Easiness in graph models, Intersection types and lambda models, Nominal rewriting, A general mathematics of names, A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG, Investigations on the dual calculus, A modern elaboration of the ramified theory of types, On a monadic semantics for freshness, Weak linearization of the lambda calculus, Compositional characterisations of $\lambda$-terms using intersection types, Remarks on applicative theories, The conflict-free reduction geometry, Kernel-LEAF: A logic plus functional language, Domain-Freeλµ-Calculus, LesI-types du système ${\cal F}$, λν, a calculus of explicit substitutions which preserves strong normalisation, Lambda-calcul, évaluation paresseuse et mise en mémoire, Unnamed Item, Logic and functional programming by retractions, Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle, Provable isomorphisms of types, Unnamed Item, The interpretation of unsolvable λ-terms in models of untyped λ-calculus, Linear realizability and full completeness for typed lambda-calculi, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Computability in higher types, P$\omega$ and the completeness of type assignment, Continuous monoids and semirings, Strong normalisation in the $\pi$-calculus, Comparing models of the intensional typed $\lambda$-calculus, Filter models for conjunctive-disjunctive $\lambda$-calculi, Intersection type assignment systems with higher-order algebraic rewriting, Principles of programming with complex objects and collection types, Properties of a first-order functional language with sharing, Computational interpretations of linear logic, Spaces with combinators, Using typed lambda calculus to implement formal systems on a machine, Forcing in stable models of untyped $\lambda$-calculus, Simulations in coalgebra, The semantics of second-order lambda calculus, Type inference with recursive types: Syntax and semantics, Retractions of dI-domains as a model for Type:Type, Simple consequence relations, A variadic extension of Curry's fixed-point combinator, A calculus of coroutines, Mechanising $\lambda$-calculus using a classical first order theory of terms with permutations, An initial algebra approach to term rewriting systems with variable binders, Expressing combinatory reduction systems derivations in the rewriting calculus, Type checking a multithreaded functional language with session types, Weak typed Böhm theorem on IMLL, Resource operators for $\lambda$-calculus, On tree automata that certify termination of left-linear term rewriting systems, Fair ambients, A $\rho$-calculus of explicit constraint application, Analytic proof systems for $\lambda$-calculus: the elimination of transitivity, and why it matters, A logic of abstraction related to finite constructive number classes, A category-theoretic characterization of functional completeness, Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation), 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 $\lambda$- 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 $\pi$-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 $\lambda$-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 $\lambda$-calculus, Some results on cut-elimination, provable well-orderings, induction and reflection, Typability and type checking in System F are equivalent and undecidable, On $\Pi$-conversion in the $\lambda$-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 $\omega$-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, Categorical models for non-extensional λ-calculi and combinatory logic, An application of PER models to program extraction, Simulating expansions without expansions, Pure type systems with more liberal rules, Toward a semantics for the QUEST language, Résultats de complétude pour des classes de types du système $\mathcal {AF}2$, Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés, An abstract monadic semantics for value recursion, An Essay in λ‐Calculus, ARITHMETIC IN THE FORM, Reflexive objects in topological categories, Opérateurs de mise en mémoire et types $\forall $-positifs, Characterizations of semantic domains for randomized algorithms, Quantifier elimination and parametric polymorphism in programming languages, Efficient self-interpretation in lambda calculus, Theoretical Pearls:Representing ‘undefined’ in lambda calculus, Residual theory in λ-calculus: a formal development, The virtues of eta-expansion, Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi, Storage Operators and ∀‐positive Types in TTR Type System, A confluent reduction for the λ-calculus with surjective pairing and terminal object, A semantic basis for Quest, Theoretical Pearls, Type inference with simple subtypes, Call-by-value Solvability, Denotational aspects of untyped normalization by evaluation, A fully abstract denotational semantics for the calculus of higher-order communicating systems, Objects and their lambda calculus, Type system in programming languages, Full intersection types and topologies in lambda calculus, Intersection types for $\lambda$-trees, Innocent game models of untyped $\lambda$-calculus, Completeness of type assignment systems with intersection, union, and type quantifiers, Minimality and separation results on asynchronous mobile processes -- representability theorems by concurrent combinators, On the construction of stable models of untyped $\lambda$-calculus, Weak normalization implies strong normalization in a class of non-dependent pure type systems, On the longest perpetual reductions in orthogonal expression reduction systems, An induction principle for pure type systems