Computability in higher types, P and the completeness of type assignment

DOI10.1016/0304-3975(86)90030-7zbMATH Open0625.03027OpenAlexW2032004219MaRDI QIDQ579245FDOQ579245

Authors: 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

Recommendations

• scientific article; zbMATH DE number 3933051
• scientific article; zbMATH DE number 4087654
• Completeness of type assignment in continuous lambda models
• The hereditary partial effective functionals and recursion theory in higher types
• A filter lambda model and the completeness of type assignment

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)

Cites Work

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

Cited In (9)

• Interpreting higher computations as types with totality
• The computational power of \({\mathcal M}^\omega\)
• Completeness of type assignment in continuous lambda models
• Title not available (Why is that?)
• Title not available (Why is that?)
• Higher types, finite domains and resource-bounded Turing machines
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Title not available (Why is that?)
• Constructive natural deduction and its ‘ω-set’ interpretation

Uses Software

• ML

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q579245)