Computational foundations of basic recursive function theory
The authors present a variant of indexing-free theory of computing, in which computations ``can be treated as objects and typed. The family of base types consists of three types: the nonnegative integers, a one- element type unit and a two-element type Boolean. One of the generating rules is very strong: it is the fixed point rule. The axiomatic rules of the theory are constructive. The authors show parallels between recursive function theory over natural numbers and this new theory, particularly concerning unsolvability results. A variant of Rice's theorem is proved. A ``dovetailing constructor is defined to make possible parallel computing. The notions of reducibility, completeness, acceptability (a generalization of recursive enumerability) are introduced. The authors show that Markov's principle implies a generalization of Post's theorem concerning r.e. sets with r.e. complement. The theory is deeply connected with Nuprl [\textit{R. Constable} et al., Implementing, mathematics with the Nuprl proof development system, Prentice-Hall, Englewood Cliffs, NJ (1986)].
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Algebraically Generalized Recursive Function Theory
- Constructive mathematics and computer programming
- Data Types as Lattices
- Domain interpretations of Martin-Löf's partial type theory
- Edinburgh LCF. A mechanized logic of computation
- scientific article; zbMATH DE number 3900718 (Why is no real title available?)
- scientific article; zbMATH DE number 3928956 (Why is no real title available?)
- scientific article; zbMATH DE number 3966062 (Why is no real title available?)
- scientific article; zbMATH DE number 4074542 (Why is no real title available?)
- scientific article; zbMATH DE number 4091484 (Why is no real title available?)
- scientific article; zbMATH DE number 3655923 (Why is no real title available?)
- scientific article; zbMATH DE number 3685474 (Why is no real title available?)
- scientific article; zbMATH DE number 3520384 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- scientific article; zbMATH DE number 3418623 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- LCF considered as a programming language
- Recursive Functionals and Quantifiers of Finite Types I
- Shorter Notes: A Note on the Failure of the Relativized Enumeration Theorem in Recursive Function Theory
- Uniformly Reflexive Structures: On the Nature of Godelizations and Relative Computability
- Constructing type systems over an operational semantics
- Meaning explanations at higher dimension
- Formalizing abstract computability: Turing categories in Coq
- Some Reflections on the Foundations of Ordinary Recursion Theory and a New Proposal
- scientific article; zbMATH DE number 702378 (Why is no real title available?)
- Validating Brouwer's continuity principle for numbers using named exceptions
- Multi-type recursive functions
- Recursive Functions and Constructive Mathematics
- Notions of computation and monads
This page was built for publication: Computational foundations of basic recursive function theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1314348)
