FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Teaching Your Rooster to Crow in C

Author: Jason Gross

Paper Information

Title:Teaching Your Rooster to Crow in C
Authors:Jason Gross
Proceedings:Coq Abstracts
Editor: Nicolas Tabareau
Keywords:Coq, notation, pretty printing, DSL
Abstract:

ABSTRACT. Coq's notation system is both extremely powerful and confusingly ad-hoc. While powerful enough to pretty-print abstract syntax trees in most domain-specific languages, how to do so does not seem to be common knowledge. Typical questions arising from such an endeavor might include "How do I pick notation levels?", "Why are these notations clashing?", "Which things should be marked as symbols?", "How do I use boxes in `format`?", and "How do I get parentheses to show up (only) where I want them to?" This interactive presentation aims to serve as a guide to these questions and more, by demonstrating and explaining how to pretty-print subsets of C using only Coq's `Notation` mechanism.

Pages:2
Talk:Jul 08 17:00 (Session 42B)
Paper: