### 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

*Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings*(pp. 370-385). (Lecture Notes in Computer Science; Vol. 7998). Berlin. https://doi.org/10.1007/978-3-642-39634-2_27

}

*Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings.*Lecture Notes in Computer Science, vol. 7998, Berlin, pp. 370-385, 4th International Conference on Interactive Theorem Proving, ITP 2013, Rennes, France, 22/07/13. https://doi.org/10.1007/978-3-642-39634-2_27

**Program extraction from nested definitions.** / Miyamoto, Kenji; Nordvall Forsberg, Fredrik; Schwichtenberg, Helmut.

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 -