| Modelling General Recursion in Type Theory (2004) | |||||||||||||||
Abstract | |||||||||||||||
| this paper is also included. A tutorial on the method can also be found in Bove 2003. Since our method separates the computational part from the logical part of a de nition, formalising partial functions becomes possible (Bove & Capretta 2001, Bove 2003). Proving that a certain function is total amounts to proving that the corresponding special-purpose accessibility predicate (or domain predicate) is satis ed by every input | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||