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)

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
A coinductive completeness proof for the equivalence of recursive types
A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
Projections for infinitary rewriting
Strong normalization through intersection types and memory
Explicit cyclic substitutions
The interpretation of unsolvable λ-terms in models of untyped λ-calculus
scientific article; zbMATH DE number 7215287 (Why is no real title available?)
Rule-based transformation of graph rewriting rules: towards higher-order graph grammars
Revisiting the notion of function
Comparing higher-order encodings in logical frameworks and tile logic
Call-by-value combinatory logic and the lambda-value calculus
Functions-as-constructors higher-order unification: extended pattern unification
On infinite \(\eta\)-expansion
Unifying overloading and \(\lambda\)-abstraction: \(\lambda^{\{\,\}}\)
Relative normalization in Deterministic Residual Structures
Multityped abstract categorial grammars and their composition
A general mathematics of names
Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
Residual theory in λ-calculus: a formal development
An interpretation of typed objects into typed \(\pi\)-calculus
Normalization without reducibility
Completeness of type assignment systems with intersection, union, and type quantifiers
Setting the facts straight
Fair ambients
Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
Nominal rewriting
Bunder's paradox
Categorical pairs and the indicative shift
Computability in higher types, P\(\omega\) and the completeness of type assignment
Three Syntactic Theories for Combinatory Graph Reduction
Parallel beta reduction is not elementary recursive
The mechanisation of Barendregt-style equational proofs (the residual perspective)
Productivity of stream definitions
Confluence by decreasing diagrams
On equal \(\mu \)-terms
Viewing \({\lambda}\)-terms through maps
A Mechanized Model of the Theory of Objects
Lambda-calculus with director strings
A Polymorphic Type System for the Lambda-Calculus with Constructors
Local Termination
A Church-style intermediate language for ML\(^{\text F}\)
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
Filter models for conjunctive-disjunctive \(\lambda\)-calculi
A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
Head linear reduction and pure proof net extraction
The λ-calculus with constructors: Syntax, confluence and separation
First-class patterns
Adding algebraic rewriting to the untyped lambda calculus
Rewriting strategies and strategic rewrite programs
Context rewriting
Semantics of weakening and contraction
Call-by-value non-determinism in a linear logic type discipline
The semantics of second-order lambda calculus
Typed Applicative Structures and Normalization by Evaluation for System F ω
Some results on cut-elimination, provable well-orderings, induction and reflection
Intersection type assignment systems with higher-order algebraic rewriting
Building continuous webbed models for system F
scientific article; zbMATH DE number 6148924 (Why is no real title available?)
Synthesizable high level hardware descriptions
The sequentially realizable functionals
The subtyping problem for second-order types is undecidable.
A characterization of F-complete type assignments
A full continuous model of polymorphism
Confluence of the coinductive \(\lambda\)-calculus

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)