A Vernacular for Coherent Logic

Sana Stojanovic, Julien Narboux, Marc Bezem +1

We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rule…