Fix-point equations for well-founded recursion in type theory
In: TPHOLs 2000 : theorem proving in higher order logics (Portland OR, 14-18 August 2000)Lecture notes in computer science :1-16
Konferenz
- print, 16 ref
Zugriff:
Inductive type theories provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions. This work provides a fix-point equality theorem that represents the reduction rule and can be used without any knowledge of the proofs' structure. The first motivation is practical in nature. Without a fix-point equality, it is hard to collect information about a function. In a system like Coq, the fix-point equation is only a consequence of the encoding based on generalized inductive data-types. With our work to generate this equality automatically, it becomes simpler to reason about well-founded recursive functions in Coq.
Titel: |
Fix-point equations for well-founded recursion in type theory
|
---|---|
Autor/in / Beteiligte Person: | BALAA, A ; BERTOT, Y |
Link: | |
Quelle: | TPHOLs 2000 : theorem proving in higher order logics (Portland OR, 14-18 August 2000)Lecture notes in computer science :1-16 |
Veröffentlichung: | Berlin: Springer, 2000 |
Medientyp: | Konferenz |
Umfang: | print, 16 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|