POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:00 - 16:22 at Kelvin Lecture - Session 4

At the heart of most formal developments are inductive definitions, ranging from simple data structures to complex operational semantics of programming languages. We are developing InducTeX, a MetaCoq plugin for typesetting Coq inductives as inference rules with TeX.

The tool provides a convenient way of documenting and communicating inductive definitions, even to those who are not proficient in Coq. Furthermore, it saves authors from duplicating their Coq inference rules in TeX and having to keep them in sync with the corresponding Coq definitions.