InducTeX: A MetaCoq Plugin for Typesetting Inductive Definitions

InducTeX: A MetaCoq Plugin for Typesetting Inductive Definitions

Explore a MetaCoq plugin called InducTeX, designed to typeset Coq inductive definitions as inference rules using TeX. Learn how this tool facilitates the documentation and communication of inductive definitions, making them accessible even to those unfamiliar with Coq. Discover the plugin's ability to automatically generate TeX representations of inference rules, eliminating the need for manual duplication and synchronization between Coq definitions and their TeX counterparts. Gain insights into how InducTeX can streamline the process of working with inductive definitions, from simple data structures to complex operational semantics of programming languages, in this 22-minute conference talk presented by Jacco Krijnen at CoqPL'24.