|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|
, 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 .
|Editor||M. Aagaard and J. Harrison|