On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory

DOI10.1016/0168-0072(88)90017-6zbMath0673.03009OpenAlexW1527344590MaRDI QIDQ1120558

No author found.

Publication date: 1988

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(88)90017-6

zbMATH Keywords

surveybibliographyproof theorycategory theorysemantics\(\lambda\)-calculushigher type recursion theory

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Functionals in proof theory (03F10) Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65)

Related Items (3)

A category-theoretic characterization of functional completeness ⋮ A note on Russell's paradox in locally Cartesian closed categories ⋮ A modest model of records, inheritance, and bounded quantification

Uses Software

• ML
• Nuprl
• Automath

Cites Work

• Computability in higher types, P\(\omega\) and the completeness of type assignment
• Linear logic
• Completeness of type assignment in continuous lambda models
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• Harvey Friedman's research on the foundations of mathematics
• Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The system \({\mathcal F}\) of variable types, fifteen years later
• Realizability and recursive set theory
• Pebble, a kernel language for modules and abstract data types
• Categories of partial maps
• \(\mathbb{T}^\omega\) as a universal domain
• Intuitionist type theory and the free topos
• Sequential algorithms on concrete data structures
• A theory of type polymorphism in programming
• Fixed-point constructions in order-enriched categories
• Intuitionistic propositional logic is polynomial-space complete
• Semantics-directed generation of a Prolog compiler
• Edinburgh LCF. A mechanized logic of computation
• Writing programs that construct proofs
• The L. E. J. Brouwer Centenary Symposium. Proceedings of the Conference held in Noordwijkerhout, 8--13 June, 1981
• A set of postulates for the foundation of logic. II
• Randomized geometric algorithms and pseudorandom generators
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Combinators, \(\lambda\)-terms and proof theory
• \(\lambda\)-definability and recursiveness
• A weak absolute consistency proof for some systems of illative combinatory logic
• A new type assignment for λ-terms
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Locally cartesian closed categories and type theory
• Models of the lambda calculus
• A filter lambda model and the completeness of type assignment
• Recursion theoretic operators and morphisms on numbered sets
• The Type Theory of PL/CV3
• Pre-adjunctions and lambda-algebraic theories
• Effectively given domains and lambda-calculus models
• The hereditary partial effective functionals and recursion theory in higher types
• Categorical combinators
• Tripos theory
• Lambda‐Calculus Models and Extensionality
• Completeness, invariance and λ-definability
• The Category-Theoretic Solution of Recursive Domain Equations
• Constructive natural deduction and its ‘ω-set’ interpretation
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• Data Types as Lattices
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Can programming be liberated from the von Neumann style?
• A sequent calculus formulation of type assignment with equality rules for the λβ-calculus
• The „Dialectica”︁ Interpretation and Categories
• Functional completeness of cartesian categories
• Deductive systems and categories
• The Principal Type-Scheme of an Object in Combinatory Logic
• Resolution in type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory