Prettyprinter for Twelf
Twelf is a language used for describing and proving properties about
logical systems. As part of a university project, I wrote a program
able to translate parts of Twelf signatures into LaTeX, formatting
definitions as either grammars or natural-deduction-tree-style
inference rules. Proofs are not printed in any useful form, nor is
more than second-order higher abstract syntax supported. While still
in need of some final touchups and some documentation, twelfppr
is
already somewhat useful. You can check out the code on the Github
page.
As far as I know, twelfppr
should be able to handle the full Twelf
language.