The Mathematical Foundation of the Proof Assistant Sparkle
Maarten de Mol, M.C.J.D. van Eekelen, Rinus Plasmeijer · 2007
This report presents the mathematical foundation of the proof assistant Sparkle, which is dedicated to the lazy functional language Clean. The mathematical foundation provides a formalization of the programming, logic and proof languages that are supported by Sparkle. Furthermore, it formalizes the reduction of programs and the semantics of properties, and provides proofs for the soundness of the de ned tactics. 1