On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
From MaRDI portal
Publication:1120558
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
surveybibliographyproof theorycategory theorysemantics\(\lambda\)-calculushigher type recursion theory
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
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
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
