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)
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
03D99: Computability and recursion theory
03B40: Combinatory logic and lambda calculus
Related Items
Computability in higher types, P\(\omega\) and the completeness of type assignment, Cartesian closed categories of algebraic cpos, \(\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, Equational theories for inductive types, A theory of binding structures and applications to rewriting, On stable domains, Conditional linearization, 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, Expressive power of typed and type-free programming languages, Une nouvelle C\(\beta\)-réduction dans la logique combinatoire, Principal type schemes for an extended type theory, Reduction graphs in the lambda calculus, Completeness of type assignment in continuous lambda models, On graph rewritings, \(\lambda\)-definability of free algebras, The absence and the presence of fixed point combinators, Essence of generalized partial computation, Call-by-push-value: Decomposing call-by-value and call-by-name, 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, Nominal techniques in Isabelle/HOL, Parametric \(\lambda \)-theories, Types as graphs: Continuations in type logical grammar, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, A proof description language and its reduction system, 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, Structured algebraic specifications: A kernel language, Partial evaluation and \(\omega\)-completeness of algebraic specifications, Universal profinite domains, Implication and analysis in classical Frege structures, Functional programming with combinators, Word operation definable in the typed \(\lambda\)-calculus, Parameter-reduction of higher level grammars, A syntactic theory of sequential control, One-step recurrent terms in \(\lambda\)-\(\beta\)-calculus, 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, Sequential algorithms on concrete data structures, Inheritance as implicit coercion, Universal homogeneous event structures and domains, Frame-fuzzy points and membership, Type checking with universes, Finite type structures within combinatory algebras, The chemical abstract machine, An intuitionistic theory of types with assumptions of high-arity variables, Map theory, Lambek calculus with restricted contraction and expansion, The revised report on the syntactic theories of sequential control and state, Constructing type systems over an operational semantics, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Normal forms have partial types, 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, Infinite \(\lambda\)-calculus and types, Topology, domain theory and theoretical computer science, The kernel strategy and its use for the study of combinatory logic, 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, When is partial trace equivalence adequate?, Third order matching is decidable, \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule, Constructive domain theory as a branch of intuitionistic pointfree topology, Strong normalization for non-structural subtyping via saturated sets, The application of automated reasoning to questions in mathematics and logic, Interaction and program generators., Embedding of a free cartesian-closed category into the category of sets, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, A first order logic of effects, A confluent calculus for concurrent constraint programming, Developing developments, Higher-order subtyping, A linear logical framework, Reduction of finite and infinite derivations, On principal types of combinators, A theory of rules for enumerated classes of functions, Universal domains and the amalgamation property, Alonzo church:his life, his work and some of his miracles, Russell's 1903 - 1905 Anticipation of the Lambda Calculus, A normalization theorem for set theory, Theoretical Pearl Yet yet a counterexample for λ+SP, Total unfolding: theory and applications, Equivalence in functional languages with effects, SPACE AND TIME IN COMPUTATION AND DISCRETE PHYSICS, A \(\kappa\)-denotational semantics for map theory in ZFC+SI, A semantical proof of De Jongh's theorem, Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus, Typing and computational properties of lambda expressions, Self-similar sets as Tarski's fixed points, On the logic of unification, Towards a computation system based on set theory, Sequential evaluation strategies for parallel-or and related reduction systems, On the semantics of polymorphism, Equality between functionals in the presence of coproducts, Integration in Real PCF, On the \(\lambda Y\) calculus, Parametric parameter passing \(\lambda\)-calculus, Enumerators of lambda terms are reducing constructively, Levels of truth, NP-completeness of a combinator optimization problem, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Variations on mobile processes, SAC -- a functional array language for efficient multi-threaded execution, Improving the lazy Krivine machine, Strongly reducing variants of the Krivine abstract machine, Classical \(F_{\omega}\), orthogonality and symmetric candidates, Pure bigraphs: structure and dynamics, Diagonal fixed points in algebraic recursion theory, Unnamed Item, Unnamed Item, Unnamed Item, Meeting of the Association for Symbolic Logic, Stanford, California, 1985, Point-fixe sur un ensemble restreint, Proposal for a natural formalization of functional programming concepts, Functions as processes
