Program extraction from nested definitions

Kenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

5 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationInteractive Theorem Proving
Subtitle of host publication4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
EditorsSandrine Blazy, Christine Paulin-Mohring, David Pichardie
Place of PublicationBerlin
Pages370-385
Number of pages16
DOIs
Publication statusPublished - 19 Jul 2013
Event4th International Conference on Interactive Theorem Proving, ITP 2013 - Rennes, France
Duration: 22 Jul 201326 Jul 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume7998
ISSN (Print)0302-9743

Conference

Conference4th International Conference on Interactive Theorem Proving, ITP 2013
CountryFrance
CityRennes
Period22/07/1326/07/13

Keywords

  • coinduction
  • computational contents
  • formalisation
  • Haskell programs
  • program extraction
  • proof assistant
  • uniformly continuous

Cite this

Miyamoto, K., Nordvall Forsberg, F., & Schwichtenberg, H. (2013). Program extraction from nested definitions. In S. Blazy, C. Paulin-Mohring, & D. Pichardie (Eds.), 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
Miyamoto, Kenji ; Nordvall Forsberg, Fredrik ; Schwichtenberg, Helmut. / Program extraction from nested definitions. Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. editor / Sandrine Blazy ; Christine Paulin-Mohring ; David Pichardie. Berlin, 2013. pp. 370-385 (Lecture Notes in Computer Science).
@inproceedings{893ff40f5282431484242469602a6632,
title = "Program extraction from nested definitions",
abstract = "Minlog is a proof assistant which automatically extracts computational content in an extension of G{\"o}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.",
keywords = "coinduction, computational contents, formalisation, Haskell programs, program extraction, proof assistant, uniformly continuous",
author = "Kenji Miyamoto and {Nordvall Forsberg}, Fredrik and Helmut Schwichtenberg",
year = "2013",
month = "7",
day = "19",
doi = "10.1007/978-3-642-39634-2_27",
language = "English",
isbn = "9783642396335",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "370--385",
editor = "Sandrine Blazy and Christine Paulin-Mohring and David Pichardie",
booktitle = "Interactive Theorem Proving",

}

Miyamoto, K, Nordvall Forsberg, F & Schwichtenberg, H 2013, Program extraction from nested definitions. in S Blazy, C Paulin-Mohring & D Pichardie (eds), 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.

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

Miyamoto K, Nordvall Forsberg F, Schwichtenberg H. Program extraction from nested definitions. In Blazy S, Paulin-Mohring C, Pichardie D, editors, Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Berlin. 2013. p. 370-385. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-39634-2_27