Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs
Laurent Théry · Electronic Notes in Theoretical Computer Science · 2004
In this paper we propose a proof format to write formal proofs motivated by a formalisation of floating-point numbers.This proof format aims at being adequate for both proof presentation and mechanised proof checking.We also present a simple graphical interface to support this proof format.