Output details
11 - Computer Science and Informatics
University of Nottingham
Chapter title
A type of partial recursive functions
Type
C - Chapter in book
Publisher of book
Springer
Book title
Theorem proving in higher order logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008
ISBN of book
9783540710653
Year of publication
2008
Number of additional authors
1
Additional information
<11> The representation of general recursive functions in a total type theory is a fundamental problem that has received much attention in recent years. In this article, we completely solved the problem by showing how the Bove/Capretta method, developed by the authors, can be formulated in the most general form, leading to a definition of types for all the computable functions between any two data sets. The Bove/Capretta method has been used successfully in many formal developments in type-theoretic based proof assistants, specifically in Coq, and has become a standard tool for modeling programs and formally proving their correctness.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
