scientific article

Publication date: 1984

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

recursive functions inductive definitions Reduction type free lambda calculus lambda model Böhm tree Lambda terms

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Combinatory logic and lambda calculus (03B40)

Related Items

Classical logic, storage operators and second-order lambda-calculus, Games characterizing Levy-Longo trees, The differential lambda-calculus, On the implementation of abstract data types by programming language constructs, Strong normalization in type systems: A model theoretical approach, The Inf function in the system \(F\), Needed reduction and spine strategies for the lambda calculus, Formalizing non-termination of recursive programs, A unified approach to type theory through a refined \(\lambda\)-calculus, Equational programming in \(\lambda\)-calculus via SL-systems. Part 1, Equational programming in \(\lambda\)-calculus via SL-systems. Part 2, Totality in applicative theories, Every countable poset is embeddable in the poset of unsolvable terms, A synchronous \(\pi\)-calculus, Partial combinatory algebra and generalized numberings, Term-Generic Logic, The Lambda Calculus: Practice and Principle, Semantics of the second order lambda calculus, Higher-order subtyping and its decidability, Combinatory weak reduction in lambda calculus, Hypergraph Basic Categorial Grammars, C-system of a module over a \(Jf\)-relative monad, A note on preservation of strong normalisation in the \(\lambda \)-calculus, A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations, Implementing term rewrite languages in DACTL, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, Theories with self-application and computational complexity., Recursion over realizability structures, On strong normalization and type inference in the intersection type discipline, Partial inductive definitions, Normal forms for a class of formulas, Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus, A multiset semantics for the pi-calculus with replication, Constructive \(\lambda\)-models, Strictness analysis via abstract interpretation for recursively defined types, Characterizing complexity classes by higher type primitive recursive definitions, Extension of combinatory logic to a theory of combinatory representation, On the adequacy of representing higher order intuitionistic logic as a pure type system, Intersection types for combinatory logic, Parallel reductions in \(\lambda\)-calculus, A proof-theoretic characterization of the basic feasible functionals, Unnamed Item, Unnamed Item, On sets of solutions to combinator equations, A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus, Constant time parallel computations in \(\lambda\)-calculus, Shallow confluence of conditional term rewriting systems, On perfect ideals of seminearrings, A note on inconsistencies caused by fixpoints in a cartesian closed category, About systems of equations, X-separability, and left-invertibility in the \(\lambda\)-calculus, Stability and computability in coherent domains, Telescopic mappings in typed lambda calculus, Fixed point theorems for precomplete numberings, Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus, Supra-logic: using transfinite type theory with type variables for paraconsistency, Higher-order unification revisited: Complete sets of transformations, Realizability models for BLL-like languages, Type Inference using Constraint Handling Rules, On the semantics of the call-by-name CPS transform, Ordinals and ordinal functions representable in the simply typed lambda calculus, Term-generic logic, Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus, Higher order unification via explicit substitutions, A structural approach to reversible computation, Kripke-style models for typed lambda calculus, A fully abstract denotational semantics for the \(\pi\)-calculus, An equivalence between lambda- terms, Why ramify?, Abstract abstract reduction