Abstract
| Original language | English |
|---|---|
| Title of host publication | Interactive Theorem Proving |
| Subtitle of host publication | 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings |
| Editors | Sandrine Blazy, Christine Paulin-Mohring, David Pichardie |
| Place of Publication | Berlin |
| Pages | 370-385 |
| Number of pages | 16 |
| DOIs | |
| Publication status | Published - 19 Jul 2013 |
| Event | 4th International Conference on Interactive Theorem Proving, ITP 2013 - Rennes, France Duration: 22 Jul 2013 → 26 Jul 2013 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Berlin Heidelberg |
| Volume | 7998 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 4th International Conference on Interactive Theorem Proving, ITP 2013 |
|---|---|
| Country | France |
| City | Rennes |
| Period | 22/07/13 → 26/07/13 |
Keywords
- coinduction
- computational contents
- formalisation
- Haskell programs
- program extraction
- proof assistant
- uniformly continuous
Cite this
}
Program extraction from nested definitions. / Miyamoto, Kenji; Nordvall Forsberg, Fredrik; Schwichtenberg, Helmut.
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. ed. / Sandrine Blazy; Christine Paulin-Mohring; David Pichardie. Berlin, 2013. p. 370-385 (Lecture Notes in Computer Science; Vol. 7998).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book
TY - GEN
T1 - Program extraction from nested definitions
AU - Miyamoto, Kenji
AU - Nordvall Forsberg, Fredrik
AU - Schwichtenberg, Helmut
PY - 2013/7/19
Y1 - 2013/7/19
N2 - Minlog is a proof assistant which automatically extracts computational content in an extension of Gödel’s T from formalized proofs. We report on extending Minlog to deal with predicates defined using a particular combination of induction and coinduction, via so-called nested definitions. In order to increase the efficiency of the extracted programs, we have also implemented a feature to translate terms into Haskell programs. To illustrate our theory and implementation, a formalisation of a theory of uniformly continuous functions due to Berger is presented.
AB - Minlog is a proof assistant which automatically extracts computational content in an extension of Gödel’s T from formalized proofs. We report on extending Minlog to deal with predicates defined using a particular combination of induction and coinduction, via so-called nested definitions. In order to increase the efficiency of the extracted programs, we have also implemented a feature to translate terms into Haskell programs. To illustrate our theory and implementation, a formalisation of a theory of uniformly continuous functions due to Berger is presented.
KW - coinduction
KW - computational contents
KW - formalisation
KW - Haskell programs
KW - program extraction
KW - proof assistant
KW - uniformly continuous
UR - http://link.springer.com/
UR - http://itp2013.inria.fr/
U2 - 10.1007/978-3-642-39634-2_27
DO - 10.1007/978-3-642-39634-2_27
M3 - Conference contribution book
SN - 9783642396335
T3 - Lecture Notes in Computer Science
SP - 370
EP - 385
BT - Interactive Theorem Proving
A2 - Blazy, Sandrine
A2 - Paulin-Mohring, Christine
A2 - Pichardie, David
CY - Berlin
ER -