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
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, Extended term rewriting systems, Explicit effect subtyping, Levy Labels and Recursive Types, On the \(\lambda Y\) calculus, Parametric parameter passing \(\lambda\)-calculus, Enumerators of lambda terms are reducing constructively, Adding algebraic rewriting to the untyped lambda calculus (extended abstract), Some lambda calculi with categorical sums and products, Proving the genericity lemma by leftmost reduction is simple, The combinator M and the Mockingbird lattice, Universal domains and the amalgamation property, Levels of truth, NP-completeness of a combinator optimization problem, Using resolution for deciding solvable classes and building finite models, On λ-Definable Functions on Ordinals, Unnamed Item, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Embedding of a free cartesian-closed category into the category of sets, Functions as processes, Meeting of the Association for Symbolic Logic, Stanford, California, 1985, Wrapper semantics of an object-oriented programming language with state, 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 user's friendly syntax to define recursive functions as typed λ-terms, A short and flexible proof of strong normalization for the calculus of constructions, The Maude strategy language, A simple language supporting angelic nondeterminism and parallel composition, Correctness of procedure representations in higher-order assembly language, A deterministic rewrite system for the probabilistic λ-calculus, A linear logical framework, Many more predecessors: A representation workout, The conservation theorem for differential nets, SAC -- a functional array language for efficient multi-threaded execution, Point-fixe sur un ensemble restreint, Unnamed Item, Unnamed Item, Three faces of natural deduction, Proposal for a natural formalization of functional programming concepts, Variations on mobile processes, Psi-calculi in Isabelle, On Higher-Order Probabilistic Subrecursion, Strategic port graph rewriting: an interactive modelling framework, Improving the lazy Krivine machine, Strongly reducing variants of the Krivine abstract machine, Strategies, model checking and branching-time properties in Maude, Unnamed Item, Decidability of all minimal models, Optimized encodings of fragments of type theory in first order logic, A higher-order strategy for eliminating common subexpressions, The Typed Böhm Theorem, Hyperformulae, Parallel Deductions and Intersection Types, Alonzo church:his life, his work and some of his miracles, Classical \(F_{\omega}\), orthogonality and symmetric candidates, A \(\kappa\)-denotational semantics for map theory in ZFC+SI, Pure bigraphs: structure and dynamics, Formal SOS-Proofs for the Lambda-Calculus, The Functional Interpretation of Direct Computations, Equivalence in functional languages with effects, Introduction to Type Theory, Dependent vector types for data structuring in multirate Faust, Unnamed Item, SPACE AND TIME IN COMPUTATION AND DISCRETE PHYSICS, Translating between Language and Logic: What Is Easy and What Is Difficult, Unnamed Item, On Fixed Point Theory and Its Applications to Equilibrium Models, A theory of rules for enumerated classes of functions, Russell's 1903 - 1905 Anticipation of the Lambda Calculus, COCHIS: Stable and coherent implicits, 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, Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem, On the logic of unification, Towards a computation system based on set theory, Sequential evaluation strategies for parallel-or and related reduction systems, Evolving combinators, A normalization theorem for set theory, Dedekind completion as a method for constructing new Scott domains, On the semantics of polymorphism, Reduction of finite and infinite derivations, On principal types of combinators, Diagonal fixed points in algebraic recursion theory, Equality between functionals in the presence of coproducts, Integration in Real PCF, Theoretical Pearl Yet yet a counterexample for λ+SP, Total unfolding: theory and applications, On a Fully Abstract Model for a Quantum Linear Functional Language, Classical lambda calculus in modern dress, Computing in unpredictable environments: Semantics, reduction strategies, and program transformations
