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