---
title: TwelfPPR
---

Prettyprinter for [Twelf](http://twelf.org/wiki/Main_Page)
===
[Available on Github](https://github.com/Athas/twelfppr)

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](https://github.com/Athas/twelfppr).

As far as I know, `twelfppr` should be able to handle the full Twelf
language.