Sciweavers

Share
AISC
2010
Springer

Structured Formal Development with Quotient Types in Isabelle/HOL

9 years 16 days ago
Structured Formal Development with Quotient Types in Isabelle/HOL
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.
Maksym Bortin, Christoph Lüth
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2010
Where AISC
Authors Maksym Bortin, Christoph Lüth
Comments (0)
books