Details:
| Title | Fix-Point Equations for Well-Founded Recursion in Type Theory | | Author(s) | Antonia Balaa, Yves Bertot | | Type | Book, Chapter in Book, Conference Proceeding | | Abstract | This paper is mostly described by Coquand, Pfenning, and Paulin-Mohring in [14, 4, 11]. General use of well-founded recursion in Martin-L#f's intuitionistic type theory was studied by Paulson in
[12], who shows that reduction rules can be obtained for each of several means to construct well-founded relations from previously known well-founded relations.
By comparison with Paulson's work, our technique is to obtain reduction rules that are specic to each recursive function. The introduction of well-founded recursion using an accessibility principle as used in this paper was described by Nordstr#m in [9]. |
| Language | English | | Volume | 1689 | | Pages | 1-16 | | Publisher | Springer-Verlag | | Address | Berlin | | Year | 2000 | | Editor | M. Aagaard and J. Harrison | | Edition | 0 | | Translation |
No | | Refereed |
No |
|
