Coqoon - An IDE for Interactive Proof Development in Coq
Abstract
International audience
Related papers
- Martin-Löf à la Coq CPP 2024
- Capturing and Exploiting IDE Interactions Onward! 2014
- REPLica: REPL instrumentation for Coq analysis CPP 2020
- MoSeL: a general, extensible modal framework for interactive proofs in separation logic ICFP 2018
- Practical Tactics for Verifying C Programs in Coq CPP 2015
- Mtac: a monad for typed tactic programming in Coq ICFP 2013
- Dijkstra monads forever: termination-sensitive specifications for interaction trees POPL 2021
- Software development environments on the web: a research agenda Onward! 2012