Integration der Logik HOL mit den Programmiersprachen ML und Haskell

• Applicant: Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 2005 to 2017
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 14516968

• Final Report Year: 2019

Final Report Abstract

Ziel des Projekts war, im dem interaktiven Beweisassistenten Isabelle/HOL eine integrierte Entwicklungs- und Verifikationsumgebung für die funktionalen Programmiersprachen ML und Haskell bereitzustellen. Kernstück dessen ist ein generisches Codegenerator-Framework, das in Isabelle/HOL erstellte Definitionen direkt nach ML und Haskell übersetzten kann. In der ersten Projektphase haben wir dafür die grundlegenden Bestandteile bereitgestellt; in der zweiten Projektphase haben wir das System ausgebaut und seine Anwendungsmöglichkeiten erweitert: Datentypverfeinerung mit Invarianten, unendliche Datenstrukturen; funktional-logische, monadische und parallele Programmierung. Für alle diese Erweiterungen gibt es ambitionierte Anwendungen. Abgerundet werden diese Beiträge durch umfangreiche Analysen der Konsistenz von HOL im Zusammenspiel mit überladenen Definitionen.

Publications

• Turning inductive into equational specifications. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs ’09: Proceedings of the 22th International Conference on Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pages 131-146. Springer, 2009
  Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann
  
• Code Generation via Higher-Order Rewrite Systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming, FLOPS 2010, volume 6009 of LNCS, pages 103-117. Springer, 2010
  Florian Haftmann and Tobias Nipkow
  
• A Compiled Implementation of Normalization by Evaluation. Journal of Functional Programming, 22(1):9-30, 2012
  Klaus Aehlig, Florian Haftmann, and Tobias Nipkow
  
• Data Refinement in Isabelle/HOL. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pages 100-115, Springer, 2013
  Florian Haftmann, Alexander Krauss, Ondřej Kunčar, and Tobias Nipkow
  
• Lifting and transfer: A modular design for quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, volume 8307 of LNCS, pages 131-146. Springer, 2013
  Brian Huffman and Ondřej Kunčar
  
• Recursive functions on lazy lists via domains and topologies. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of LNCS, pages 341-357. Springer, 2014
  Andreas Lochbihler and Johannes Hölzl
  
• A consistent foundation for Isabelle/HOL. In Chr. Urban and X. Zhang, editors, Interactive Theorem Proving, ITP 2015, volume 9236 of LNCS, pages 234-252. Springer, 2015
  Ondřej Kunčar and Andrei Popescu
  
• Correctness of Isabelle’s cyclicity checker: Implementability of overloading in proof assistants. In X. Leroy and A. Tiu, editors, Certified Programs and Proofs, CPP 2015, pages 85-94. ACM, 2015
  Ondřej Kunčar
  
• From types to sets by local type definitions in higher-order logic. In J. Blanchette and S. Merz, editors, Interactive Theorem Proving, ITP 2016, volume 9807 of LNCS, pages 200-218. Springer, 2016
  Ondřej Kunčar and Andrei Popescu
  
• Comprehending Isabelle/HOL’s consistency. In H. Yang, editor, Programming Languages and Systems, ESOP 2017, volume 10201 of LNCS, pages 724-749. Springer, 2017
  Ondřej Kunčar and Andrei Popescu
  
• Safety and conservativity of definitions in HOL and Isabelle/HOL. Proc. ACM Program. Lang, 2(POPL):24:1-24:26, 2018
  Ondřej Kunčar and Andrei Popescu
  
• From types to sets by local type definition in higherorder logic. J. Autom. Reasoning, 62(2):237-260, 2019
  Ondřej Kunčar and Andrei Popescu