Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General
No abstract available.
Related papers
- The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver CAV 2026
- Interaction trees: representing recursive and impure programs in Coq POPL 2020
- Isolation and Analysis of Optimization Errors PLDI 1993
- Formalization of Karp-Miller tree construction on petri nets CPP 2017
- Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates CAV 2013
- Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq POPL 2023
- Design and Implementation of the UW Illustrated Compiler PLDI 1988
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic CPP 2024