Publication

Structural Formal Development with Quotient Types in Isabelle/HOL

Maksym Bortin, Christoph Lüth

In: 10th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2010). International Conference on Artificial Intelligence and Symbolic Computation (AISC-2010) 10th located at Intelligent Computer Mathematics 2010 (CICM 2010) July 5-10 Paris France Pages 34-48 Lecture Notes in Computer Science (LNCS) 6167 Springer 2010.

Abstract

General purpose theorem provers provide sophisticated proof methods, but lack some of the advanced structuring mechanisms found in specification languages. This paper builds on previous work extending the theorem prover Isabelle with such mechanisms. A way to build the quotient type over a given base type and an equivalence relation on it, and a generalised notion of folding over quotiented types is given as a formalised high-level step called a design tactic. The core of this paper are four axiomatic theories capturing the design tactic. The applicability is demonstrated by derivations of implementations for finite multisets and finite sets from lists in Isabelle.

Projekte

aisc2010.pdf (pdf, 397 KB)

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz