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
T2 - 4th International Conference on Interactive Theorem Proving, ITP 2013
Y2 - 22 July 2013 through 26 July 2013
ER -