Correct-by-Construction Pretty-Printing

Correct-by-Construction Pretty-Printing
Talk given at meeting #70 of IFIP WG2.1, Schloss Reisensburg, 2013-07-04. (Slightly edited.) [pdf]

Abstract

I will present a new approach to correct-by-construction pretty-printing. The basic methodology is the one of classical (not necessarily correct) pretty-printing: users convert values to pretty-printer documents, and a general rendering algorithm turns documents into strings. The main novelty is that dependent types are used to ensure that, for each value, the constructed document is correct with respect to the value and a given grammar. Other parts of the development use well-established technology: the pretty-printer document interface is basically that of Wadler (2003), but with more precise types, and a single additional primitive combinator; and Wadler's rendering algorithm is used.

I have proved that if a given value is pretty-printed, and the resulting string parsed (with respect to the same, unambiguous grammar), then the original value is obtained. I make no guarantees about "prettiness".