Integration der Logik HOL mit den Programmiersprachen ML und Haskell

• Antragsteller: Professor Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2005 bis 2017
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 14516968

• Erstellungsjahr: 2019

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

• 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