Publication:5686017

From MaRDI portal


zbMath0269.02005MaRDI QIDQ5686017

Jonathan P. Seldin, J. Roger Hindley, Bruce Lercher

Publication date: 1972



03-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations

03D99: Computability and recursion theory

03B40: Combinatory logic and lambda calculus


Related Items

Reductions of Residuals are Finite, Standard and Normal Reductions, Expressibility of functionals in D. Scott's LCF language, Expressive power of typed and type-free programming languages, Reduction graphs in the lambda calculus, The absence and the presence of fixed point combinators, Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, Functions on universal algebras, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, A notation for lambda terms. A generalization of environments, Computation on graph-like expressions, Invertible terms in the lambda calculus, Characterizing complexity classes by general recursive definitions in higher types, Capturing strong reduction in director string calculus, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, Least fixed points revisited, Functionals computable in series and in parallel, A global representation of the recursive functions in the \(\lambda\)- calculus, A discrimination algorithm inside \(\lambda -\beta\)-calculus, On analysing relevance constructively, The typed lambda-calculus is not elementary recursive, A calculus for reasoning about software composition, On the semantics of polymorphism, The completeness theorem for typing lambda-terms, Normal forms in combinatory logic, Higher-order unification via combinators, A new type assignment for λ-terms, One method of defining the semantics of programming language constructs in terms of lambda calculus. II, Unnamed Item, Definition of the semantics of programming language constructs in terms of ?-calculus. I, Unnamed Item, Definierbare Funktionen imλ-Kalkül mit Typen