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) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Combinatory logic and lambda calculus (03B40)

Related Items

Reversibility in the higher-order $\pi$-calculus, A type assignment for $\lambda$-calculus complete both for FPTIME and strong normalization, Towards a notion of lambda monoid, Relational graph models, Taylor expansion and extensionality, Graph easy sets of mute lambda terms, Gödelization in the lambda calculus, A characterization of F-complete type assignments, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Simplifying the signature in second-order unification, Productivity of stream definitions, The expectation monad in quantum foundations, Type theories, normal forms, and $D_{\infty}$-lambda-models, Mechanising $\lambda$-calculus using a classical first order theory of terms with permutations, An initial algebra approach to term rewriting systems with variable binders, Bridging Curry and Church's typing style, Substitution revisited, Expressing combinatory reduction systems derivations in the rewriting calculus, Algebra of constructions. I. The word problem for partial algebras, Type checking a multithreaded functional language with session types, Principal type scheme and unification for intersection type discipline, Polymorphic type inference and containment, Conditional rewrite rules: Confluence and termination, A two-valued logic for properties of strict functional programs allowing partial functions, Boolean-like algebras, Weak typed Böhm theorem on IMLL, Continuous monoids and semirings, A decidable theory of type assignment, Strong normalisation in the $\pi$-calculus, 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, Monoidal computer. I: Basic computability by string diagrams, Synthesizable high level hardware descriptions, Semantic types and approximation for Featherweight Java, Analytic proof systems for $\lambda$-calculus: the elimination of transitivity, and why it matters, A relational semantics for parallelism and non-determinism in a functional setting, Theory of interaction, Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility, Setting the facts straight, Pointfree expression and calculation: From quantification to temporal logic, Alpha equivalence equalities, 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, A Church-style intermediate language for ML$^{\text F}$, A synthetic axiomatization of map theory, Completeness and partial soundness results for intersection and union typing for $\overline{\lambda}\mu\tilde{\mu}$, A logic of abstraction related to finite constructive number classes, Categorical pairs and the indicative shift, A category-theoretic characterization of functional completeness, A note on harmony, Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation), A metamodel of access control for distributed environments: applications and properties, The logic of message-passing, Quantum computation: from a programmer's perspective, The heart of intersection type assignment: Normalisation proofs revisited, Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage, An irregular filter model, 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, The search for a reduction in combinatory logic equivalent to $\lambda \beta$-reduction. II., On abstract normalisation beyond neededness, Computational interpretations of linear logic, Spaces with combinators, Using typed lambda calculus to implement formal systems on a machine, On generic context lemmas for higher-order calculi with sharing, On the observational theory of the CPS-calculus, External and internal syntax of the $\lambda $-calculus, Forcing in stable models of untyped $\lambda$-calculus, On the membership problem for non-linear abstract categorial grammars, A faithful representation of non-associative Lambek grammars in abstract categorial grammars, On equal $\mu $-terms, Simulations in coalgebra, Linear realizability and full completeness for typed lambda-calculi, Cut-elimination in the strict intersection type assignment system is strongly normalizing, A semantic proof of polytime soundness of light affine logic, On the confluence of lambda-calculus with conditional rewriting, Computability in higher types, P$\omega$ and the completeness of type assignment, The stream-based service-centred calculus: a foundation for service-oriented programming, A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets, N. G. de Bruijn's contribution to the formalization of mathematics, De Bruijn's weak diamond property revisited, Viewing ${\lambda}$-terms through maps, A solution to Curry and Hindley's problem on combinatory strong reduction, On structural properties of eta-expansions of identity, The semantics of second-order lambda calculus, 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, Type inference with recursive types: Syntax and semantics, A construction of one-point bases in extended lambda calculi, CPS-translation as adjoint, Strong normalization property for second order linear logic, 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, Formal metatheory of the lambda calculus using Stoughton's substitution, On the expressiveness of choice quantification, Infinitary lambda calculus and discrimination of Berarducci trees., Eager functions as processes, Proving soundness of extensional normal-form bisimilarities, Self-quotation in a typed, intensional lambda-calculus, Pattern matching as cut elimination, Nominal unification, Easiness in graph models, Intersection types and lambda models, 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, On bisimilarity in lambda calculi with continuous probabilistic choice, Limiting partial combinatory algebras, Functions-as-constructors higher-order unification: extended pattern unification, Intersection types for explicit substitutions, Nominal logic, a first order theory of names and binding, Infinite intersection types, Nominal rewriting, A general mathematics of names, Strong normalization in type systems: A model theoretical approach, Plotkin's call-by-value $\lambda$-calculus as a modal calculus, Infinitary rewriting: closure operators, equivalences and models, OTTER experiments in a system of combinatory logic, Crowd behavior dynamics: entropic path-integral model, Some results on numerical systems in $\lambda$-calculus, Normal forms in combinatory logic, Encoding abstract syntax without fresh names, On explicit substitution with names, Semantics of quantum programming languages: Classical control, quantum control, A class of bounded functions, a database language and an extended lambda calculus, Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping, Highlights in infinitary rewriting and lambda calculus, A type-assignment of linear erasure and duplication, A formalisation of nominal $\alpha$-equivalence with A, C, and AC function symbols, Projections for infinitary rewriting (extended version), The differential method and the causal incompleteness of programming theory in molecular biology, Spinal atomic $\lambda$-calculus, Game-theoretic analysis of call-by-value computation, Operational semantics for declarative multi-paradigm languages, Decidability of bounded higher-order unification, Factorization in call-by-name and call-by-value calculi via linear logic, The self-reduction in lambda calculus, Open bisimulation, revisited, Expression reduction systems with patterns, On randomised strategies in the $\lambda $-calculus, Effectful applicative similarity for call-by-name lambda calculi, A formal system of reduction paths for parallel reduction, Full abstraction for polymorphic $\pi $-calculus, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, A core model for choreographic programming, Evaluating lambda terms with traversals, A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG, A simplified proof of the Church-Rosser theorem, Lambda-calculus with director strings, Comparing and implementing calculi of explicit substitutions with eta-reduction, Investigations on the dual calculus, On the interactive power of higher-order processes extended with parameterization, Whither semantics?, The bang calculus revisited, Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract), A proof of the substitution lemma in de Bruijn's notation, Strong storage operators and data types, A thesis for interaction, Automorphisms of types and their applications, Building continuous webbed models for system F, Call-by-value lambda calculus as a model of computation in Coq, Processes against tests: on defining contextual equivalences, A modern elaboration of the ramified theory of types, Normalization without reducibility, Linear numeral systems, (In)efficiency and reasonable cost models, Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory, The sequentially realizable functionals, Skew confluence and the lambda calculus with letrec, Observational program calculi and the correctness of translations, A Knuth-Bendix-like ordering for orienting combinator equations, 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, Rensets and renaming-based recursion for syntax with bindings, A note on subject reduction in $(\to, \exists)$-Curry with respect to complete developments, Rule-based transformation of graph rewriting rules: towards higher-order graph grammars, LF+ in Coq for "fast and loose" reasoning, On the Versatility of Open Logical Relations, Types as parameters, Open problems in rewriting, Confluence and superdevelopments, More problems in rewriting, A termination ordering for higher order rewrite systems, Infinitary lambda calculi and böhm models, Combinatory reduction systems with explicit substitution that preserve strong normalisation, Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), On the power of simple diagrams, Higher-order families, Trees from Functions as Processes, Unnamed Item, More Church-Rosser proofs (in Isabelle/HOL), A resource aware semantics for a focused intuitionistic calculus, On modular properties of higher order extensional lambda calculi, A proof theoretical approach to communication, The geometry of orthogonal reduction spaces, Labelled reductions, runtime errors, and operational subsumption, Algebras of UTxO blockchains, Execution time of λ-terms via denotational semantics and intersection types, Some properties of the -calculus, A semantics for type checking, Type inference in polymorphic type discipline, Parametricity of extensionally collapsed term models of polymorphism and their categorical properties, Intersection and union types, On the semantics of second order lambda calculus: From bruce-meyer-mitchell models to hyperdoctrine models and vice-versa, Higher-order narrowing with convergent systems, The virtues of eta-expansion, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi, Storage Operators and ∀‐positive Types in TTR Type System, Higher-order pattern generalization modulo equational theories, Implicative algebras: a new foundation for realizability and forcing, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, An analysis of the Core-ML language: Expressive power and type reconstruction, A confluent reduction for the λ-calculus with surjective pairing and terminal object, Collapsing partial combinatory algebras, A complete proof system for Nested Term Graphs, The variable containment problem, Development closed critical pairs, Reflection of formal tactics in a deductive reflection framework, A simple model construction for the Calculus of Constructions, Modal Objection to Naive Leibnizian Identity, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, From Böhm's Theorem to Observational Equivalences, Towards Lambda Calculus Order-Incompleteness, Comparing Calculi of Explicit Substitutions with Eta-reduction, Demonstrating Lambda Calculus Reduction, New Developments in Environment Machines, An abstract monadic semantics for value recursion, An Essay in λ‐Calculus, Unfixing the Fixpoint: The Theories of the λY-Calculus, Remarks on Isomorphisms of Simple Inductive Types, Ticket Entailment is decidable, Unnamed Item, Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction, A semantic basis for Quest, Theoretical Pearls, Type inference with simple subtypes, Call-by-value Solvability, Unnamed Item, Lazy Lambda calculus: Theories, models and local structure characterization, ARITHMETIC IN THE FORM, Unnamed Item, Unnamed Item, Transfinite reductions in orthogonal term rewriting systems, Decidable higher-order unification problems, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus, Reflexive objects in topological categories, Opérateurs de mise en mémoire et types $\forall $-positifs, On the Taylor expansion of probabilistic λ-terms, Normalization by Evaluation for Typed Weak lambda-Reduction, From term models to domains, Characterizations of semantic domains for randomized algorithms, Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms, Encoding many-valued logic in $\lambda$-calculus, Aspects of Categorical Recursion Theory, Normalization by Evaluation for Martin-Löf Type Theory with One Universe, 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, Taming the Merge Operator, Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention, The approximation theorem for the Λμ-calculus, Essential and relational models, The infinitary lambda calculus of the infinite eta Böhm trees, Higher-order narrowing with definitional trees, Context rewriting, Explicit cyclic substitutions, Simple type inference for term graph rewriting systems, Parallel graph rewriting on loosely coupled machine architectures, A generalized Kahn Principle for abstract asynchronous networks, An investigation into functions as processes, A chemical abstract machine for graph reduction extended abstract, Denotational aspects of untyped normalization by evaluation, Realist Consequence, Epistemic Inference, Computational Correctness, A Survey of the Proof-Theoretic Foundations of Logic Programming, A correct-by-construction conversion from lambda calculus to combinatory logic, Recursion-free modular arithmetic in the lambda-calculus, Proving strong normalization of CC by modifying realizability semantics, Machine Deduction, Semantics for abstract clauses, Multityped abstract categorial grammars and their composition, Rensets and renaming-based recursion for syntax with bindings extended version, Adding Negation to Lambda Mu, Flexible Correct-by-Construction Programming, Embeddings between partial combinatory algebras, Quantitative weak linearisation, Classical realizability and arithmetical formulæ, Call-by-value combinatory logic and the lambda-value calculus, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, The average size of ordered binary subgraphs, Parallelism in realizability models, Core Type Theory, Linear lambda terms as invariants of rooted trivalent maps, Reasoning about multi-stage programs, Normal-order reduction grammars, Call-by-name extensionality and confluence, Unnamed Item, Unnamed Item, Psi-calculi in Isabelle, a-Logic With Arrows, Functional Type Assignment for Featherweight Java, Functional Semantics, Clocks for Functional Programs, Programming in the λ-Calculus: From Church to Scott and Back, A Mechanized Model of the Theory of Objects, A fully abstract denotational semantics for the calculus of higher-order communicating systems, Objects and their lambda calculus, Type system in programming languages, The bang calculus revisited, 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, Recursive Domain Equations of Filter Models, Why Sets?, Bounded Linear Logic, Revisited, Preserving Sharing in the Partial Evaluation of Lazy Functional Programs, Taming the wild ant-lion; a counterexample to a conjecture of Böhm, Redexes are stable in the λ-calculus, Classical lambda calculus in modern dress, Clocked lambda calculus, Relative normalization in Deterministic Residual Structures, Effective longest and infinite reduction paths in untyped λ-calculi, On reduction and normalization in the computational core, $F$-semantics for type assignment systems, A computable expression of closure to efficient causation, 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, The Church-Rosser theorem and quantitative analysis of witnesses, 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, 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 the Jacopini technique, 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, 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, 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$, Denotational semantics of membrane systems by using complete metric spaces, 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, Fixed points in lambda calculus. an eccentric survey of problems and solutions, 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, Domain theory in logical form, Polymorphic rewriting conserves algebraic strong normalization, 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, Intensional computation with higher-order functions, 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, Programs as data structures in $\lambda$SF-calculus, Strong normalization through intersection types and memory, A formalisation of nominal $\alpha$-equivalence with A and AC function symbols, Projections for infinitary rewriting, On the number of unary-binary tree-like structures with restrictions on the unary height, 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, 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, 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, Generalized filter models, Proof-search in type-theoretic languages: An introduction, Some results on cut-elimination, provable well-orderings, induction and reflection, 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, Typability and type checking in System F are equivalent and undecidable, On $\Pi$-conversion in the $\lambda$-cube and the combination with abbreviations, On infinite $\eta$-expansion, Type inference, abstract interpretation and strictness analysis, Combinatory reduction systems: Introduction and survey, A type-theoretical alternative to ISWIM, CUCH, OWHY, Combining type disciplines, A coinductive completeness proof for the equivalence of recursive types, An internal language for autonomous categories, Relating conflict-free stable transition and event models via redex families, Comparing logics for rewriting: Rewriting logic, action calculi and tile logic, Confluence by decreasing diagrams, Consistency argument and classification problem in $\lambda$-calculus, The interpretation of unsolvable λ-terms in models of untyped λ-calculus, What is a categorical model of the differential and the resource λ-calculi?, Easy lambda-terms are not always simple, Sharing in the Graph Rewriting Calculus, A Short Introduction to Implicit Computational Complexity, Unnamed Item, Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices, Regular Patterns in Second-Order Unification, The Role of Indirections in Lazy Natural Semantics, Binding in Nominal Equational Logic, New, Call-by-Value Non-determinism in a Linear Logic Type Discipline, A Realizability Interpretation for Intersection and Union Types, The Prismoid of Resources, A General Class of Models of $\mathcal{H}^*$, Kernel-LEAF: A logic plus functional language, Building domains from graph models, Categorical models for non-extensional λ-calculi and combinatory logic, A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types, A Complete, Co-inductive Syntactic Theory of Sequential Control and State, Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle, An application of PER models to program extraction, Automath Type Inclusion in Barendregt’s Cube, Lambda-calcul, évaluation paresseuse et mise en mémoire, Provable isomorphisms of types, Rewriting Strategies and Strategic Rewrite Programs, On Normalization by Evaluation for Object Calculi, Simulating expansions without expansions, Inter-deriving Semantic Artifacts for Object-Oriented Programming, Pure type systems with more liberal rules, Computation with classical sequents, An insertion operator preserving infinite reduction sequences, Safety of Nöcker's strictness analysis, Lambda theories allowing terms with a finite number of fixed points, Towards a homotopy domain theory, Unnamed Item, Graph lambda theories, Metric Reasoning About $$\lambda $$-Terms: The General Case, Unnamed Item, A Type Theory for Probabilistic $$\lambda $$–calculus, Toward a semantics for the QUEST language, Domain-Freeλµ-Calculus, Three Syntactic Theories for Combinatory Graph Reduction, Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey, Logic and functional programming by retractions, Classical Call-by-Need and Duality, Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus, Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion, A Filter Model for the λμ-Calculus, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Structural recursion with locally scoped names, Measurement-Based and Universal Blind Quantum Computation, 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, Unnamed Item, ASMs and Operational Algorithmic Completeness of Lambda Calculus, LesI-types du système ${\cal F}$, An Introduction to the Lambda Calculus, Abstract λ-Calculus Machines, A Relational Model of a Parallel and Non-deterministic λ-Calculus, An Interaction Net Encoding of Gödel’s System $$\mathcal {T}$$, Classical By-Need, First-class patterns, Mechanised Computability Theory, BUNDER’S PARADOX, Local Termination, Relating Classical Realizability and Negative Translation for Existential Witness Extraction, A Polymorphic Type System for the Lambda-Calculus with Constructors, A Comparison of Equality in Computer Algebra and Correctness in Mathematical Pedagogy, The λ-calculus in the π-calculus, Effective λ-models versus recursively enumerable λ-theories, Typed Applicative Structures and Normalization by Evaluation for System F ω, The λ-calculus with constructors: Syntax, confluence and separation, Complete Types in an Extension of the System AF2, SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★, Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information, Unnamed Item, Intersection Types for the Resource Control Lambda Calculi, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types., The Theory of Contexts for First Order and Higher Order Abstract Syntax, Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic, Strongly Normalising Cut-Elimination with Strict Intersection Types, Reducibility, Intersection Typed λ-calculus, On a monadic semantics for freshness, Weak linearization of the lambda calculus, Compositional characterisations of $\lambda$-terms using intersection types, Remarks on applicative theories, Automorphisms of types in certain type theories and representation of finite groups, λν, a calculus of explicit substitutions which preserves strong normalisation, The conflict-free reduction geometry, Nominal Equational Logic, Term Collections in λ and ρ-calculi, From Functional Programs to Interaction Nets via the Rewriting Calculus, Local Bigraphs and Confluence: Two Conjectures, Sub-λ-calculi, Classified, Complete Laziness: a Natural Semantics, Computational Soundness of a Call by Name Calculus of Recursively-scoped Records, Minimality in a Linear Calculus with Iteration