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 -