To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Correct-by-Construction P… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Correct-by-Construction Pretty-Printing

Conference paper
Authors Nils Anders Danielsson
Published in Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-Typed Programming (DTP 2013)
ISBN 978-1-4503-2384-0
Publisher Association for Computing Machinery (ACM)
Publication year 2013
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Language en
Keywords dependent types, pretty-printing
Subject categories Theoretical computer science


A new approach to correct-by-construction pretty-printing is presented. 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.

It is 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. No guarantees are made about "prettiness".

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?