The lambda calculus, its syntax and semantics
From MaRDI portal
Publication:1155602
zbMath0467.03010MaRDI QIDQ1155602
Publication date: 1981
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
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) Computability and recursion theory (03D99) Combinatory logic and lambda calculus (03B40)
Related Items (only showing first 100 items - show all)
Structured algebraic specifications: A kernel language ⋮ When is partial trace equivalence adequate? ⋮ Partial evaluation and \(\omega\)-completeness of algebraic specifications ⋮ Third order matching is decidable ⋮ Regular expressions with nested levels of back referencing form a hierarchy ⋮ Universal profinite domains ⋮ Skeletons, bodies and generalized \(E(R)\)-algebras. ⋮ Implication and analysis in classical Frege structures ⋮ \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule ⋮ Constructive domain theory as a branch of intuitionistic pointfree topology ⋮ Functional programming with combinators ⋮ Strong normalization for non-structural subtyping via saturated sets ⋮ Word operation definable in the typed \(\lambda\)-calculus ⋮ Parameter-reduction of higher level grammars ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ A syntactic theory of sequential control ⋮ One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus ⋮ Interaction and program generators. ⋮ Call-by-push-value: Decomposing call-by-value and call-by-name ⋮ The calculus of constructions ⋮ Strictness analysis of the untyped \(\lambda\)-calculus ⋮ The word problem for Smullyan's lark combinator is decidable ⋮ E-ccc: Between ccc and topos ⋮ An intersection problem for finite automata ⋮ Concurrent transition systems ⋮ A type-free system extending (ZFC) ⋮ On a conjecture of Bergstra and Tucker ⋮ Invertible terms in the lambda calculus ⋮ An algebra of behavioural types ⋮ Meta-circular interpreter for a strongly typed language ⋮ E-ccc: between ccc and topos, - its expressive power from the viewpoint of data type theory ⋮ A typed calculus based on a fragment of linear logic ⋮ A category-theoretic characterization of functional completeness ⋮ Constructive system for automatic program synthesis ⋮ A characterization of lambda definable tree operations ⋮ Fuzzy topology with respect to continuous lattices ⋮ Sequential algorithms on concrete data structures ⋮ Nominal techniques in Isabelle/HOL ⋮ Inheritance as implicit coercion ⋮ Parametric \(\lambda \)-theories ⋮ Universal homogeneous event structures and domains ⋮ Frame-fuzzy points and membership ⋮ Type checking with universes ⋮ Finite type structures within combinatory algebras ⋮ \(\pi\)-calculus, internal mobility, and agent-passing calculi ⋮ Uniqueness of Scott's reflexive domain in \(P\omega \) ⋮ Term rewriting and Hoare logic -- Coded rewriting ⋮ Lambda abstraction algebras: representation theorems ⋮ The chemical abstract machine ⋮ An intuitionistic theory of types with assumptions of high-arity variables ⋮ Equational theories for inductive types ⋮ Map theory ⋮ Lambek calculus with restricted contraction and expansion ⋮ A theory of binding structures and applications to rewriting ⋮ On stable domains ⋮ The revised report on the syntactic theories of sequential control and state ⋮ Constructing type systems over an operational semantics ⋮ On the expressiveness of interaction ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Strong normalization from an unusual point of view ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Normal forms have partial types ⋮ Conditional linearization ⋮ The correctness of Newman's typability algorithm and some of its extensions ⋮ Computability in higher types, P\(\omega\) and the completeness of type assignment ⋮ Cartesian closed categories of algebraic cpos ⋮ Types as graphs: Continuations in type logical grammar ⋮ Denotational semantics of an object-oriented programming language with explicit wrappers ⋮ Abstraction problems in combinatory logic: A compositive approach ⋮ A syntactic theory of sequential state ⋮ The development of a partial evaluator for extended lambda calculus ⋮ Extensional models for polymorphism ⋮ Functorial polymorphism ⋮ Reduction of higher type levels by means of an ordinal analysis of finite terms ⋮ On combinatory algebras and their expansions ⋮ Infinite \(\lambda\)-calculus and types ⋮ Expressive power of typed and type-free programming languages ⋮ Une nouvelle C\(\beta\)-réduction dans la logique combinatoire ⋮ Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions ⋮ Learning problem for functional programming and model of biological evolution ⋮ Quantum implicit computational complexity ⋮ Topology, domain theory and theoretical computer science ⋮ Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms ⋮ Principal type schemes for an extended type theory ⋮ Reduction graphs in the lambda calculus ⋮ Completeness of type assignment in continuous lambda models ⋮ A proof description language and its reduction system ⋮ On graph rewritings ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ \(\lambda\)-definability of free algebras ⋮ Constructive proofs of the range property in lambda calculus ⋮ Some new results on easy lambda-terms ⋮ An analysis of Böhm's theorem ⋮ The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus ⋮ Set-theoretical and other elementary models of the \(\lambda\)-calculus ⋮ The absence and the presence of fixed point combinators ⋮ Essence of generalized partial computation ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction ⋮ Complexity of the combinator reduction machine ⋮ Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus
This page was built for publication: The lambda calculus, its syntax and semantics
