Maarten de Mol, M.C.J.D. van Eekelen, and Rinus Plasmeijer. Confluent Term-Graph Reduction for Computer-Aided Formal Reasoning. Technical report: ICIS-R07012, May, Radboud University Nijmegen, 2007.
Sparkle is the dedicated proof assistant for the lazy functional programming language Clean, which is based on term-graph rewriting. Because equational reasoning is an important proof technique, Sparkle needs to offer support for formally proving e1 = e2 in as many situations as possible. The base proof of equality is by means of reduction: if e1 reduces to e2, then also e1 = e2. Therefore, the underlying reduction system of Sparkle needs to be geared towards flexibility, allowing reduction to take place as often as possible. In this paper, we will define a flexible term-graph reduction system for a simplified lazy functional language. Our system leaves the choice of redex free and uses single-step reduction. It is therefore more suited for formal reasoning than the well-established standard reduction systems for lazy functional languages, which usually fix a single redex and/or realize multi-step reduction only. We will show that our system is correct with respect to the standard systems, by proving that it is confluent and allows standard lazy functional evaluation as a possible reduction path. Our reduction system is used in the foundation of Sparkle. Because it is based on a simplified functional language, it can be applied to any other functional language based on term-graph rewriting as well.
Maarten de Mol, M.C.J.D. van Eekelen, and Rinus Plasmeijer. The Mathematical Foundation of the Proof Assistant Sparkle. Technical report: ICIS-R07025, November, Radboud University Nijmegen, 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 defined tactics.