|
 
|
[BOI04] Proof Reuse with Extended Inductive Types
Conférence Internationale avec comité de lecture : TPHOLs 2004, January 2004, Vol. 3223, pp.50-65, Series LNCS,
motcle:
Résumé:
Proof assistants based on type theory such as Coq or Lego, put
emphasis on inductive specifications and proofs by featuring
expressive inductive types. It is
frequent to modify an existing specification or proof by adding or
modifying constructors in inductive types. In the context of language design,
adding constructors is a common practice to make progress step-by-step.
In this article, we propose a
mechanism to extend and parameter inductive types, and a
proof reuse mechanism founded on proof terms reuse.
BibTeX
| @inproceedings { | |||
| BOI04, | |||
| title | = | "{Proof Reuse with Extended Inductive Types}", | |
| author | = | " O. Boite ", | |
| booktitle | = | "{TPHOLs 2004}", | |
| year | = | 2004, | |
| month | = | "January", | |
| series | = | "LNCS", | |
| volume | = | 3223, | |
| pages | = | "50-65", | |
| } | |||
