Computability in higher types, P\(\omega\) and the completeness of type assignment

DOI10.1016/0304-3975(86)90030-7zbMath0625.03027OpenAlexW2032004219MaRDI QIDQ579245

Jianyong Qiao, Sumit K. Garg

Publication date: 1986

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(86)90030-7

zbMATH Keywords

continuous functionsapplicative structurecompleteness theorem for type checkingeffectively given domainformal type assignment to terms of \(\lambda \)-calculusKleene-Kreisel countable functionalsrecursive functionalsrecursive operators at higher types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65)

Related Items (2)

Constructive natural deduction and its ‘ω-set’ interpretation ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory

Uses Software

• ML

Cites Work

• 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
• On combinatory algebras and their expansions
• 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
• \(\mathbb{T}^\omega\) as a universal domain
• Effectively given domains
• Recursion on the countable functionals
• The lambda calculus, its syntax and semantics
• \(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
• Computability concepts for programming language semantics
• A theory of type polymorphism in programming
• The completeness theorem for typing lambda-terms
• Computable functionals of finite types
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Filter spaces and continuous functionals
• Effective operations on partial recursive functions
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A filter lambda model and the completeness of type assignment
• Recursion theoretic operators and morphisms on numbered sets
• Effectively given domains and lambda-calculus models
• The hereditary partial effective functionals and recursion theory in higher types
• Lambda‐Calculus Models and Extensionality
• Data Types as Lattices
• What is a model of the lambda calculus?
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: Computability in higher types, P\(\omega\) and the completeness of type assignment