Program extraction from nested definitions

Miyamoto, Kenji and Nordvall Forsberg, Fredrik and Schwichtenberg, Helmut; Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David, eds. (2013) Program extraction from nested definitions. In: Interactive Theorem Proving. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, FRA, pp. 370-385. ISBN 9783642396335 (https://doi.org/10.1007/978-3-642-39634-2_27)

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.

ORCID iDs

Nordvall Forsberg, Fredrik ORCID: https://orcid.org/0000-0001-6157-9288

• Share and Export
  

  RefWorksRIS (EndNote Online, Zotero, Ref manager, etc)RDF+XMLEndNoteASCII CitationOpenURL ContextObject in SpanMPEG-21 DIDLRIOXX2 XMLBibTeXAtomEP3 XMLDublin CoreRDF+N-TriplesMODSHTML CitationJSONData Cite XMLRDF+N3Multiline CSVOpenURL ContextObjectReferSimple MetadataMETS
• Item metadata

  Item type:	Book Section
  ID code:	53121
  Dates:	Date Event 19 July 2013 Published
  Subjects:	Science > Mathematics > Electronic computers. Computer science
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	28 May 2015 11:13
  Last modified:	11 Nov 2024 15:00
  Related URLs:	Publisher Event
  URI:	https://strathprints.strath.ac.uk/id/eprint/53121