Proof General
Proof General: A generic tool for proof development. This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a proof development. Proof General provides a powerful user-interface with relatively little effort, alleviating the need for a proof assistant to provide its own GUI, and providing a uniform appearance for diverse proof assistants. par Proof General has a growing user base and is currently used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others is on the way. Here we give a brief overview of what Proof General does and the philosophy behind it; technical details are available elsewhere. The program and user documentation are available on the web at http://www.dcs.ed.ac.uk/home/proofgen.
Keywords for this software
References in zbMATH (referenced in 53 articles , 1 standard article )
Showing results 1 to 20 of 53.
Sorted by year (- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
- Damanik, David (ed.); Gesztesy, Fritz (ed.); Yuditskii, Peter (ed.): Mini-workshop: Reflectionless operators: the Deift and Simon conjectures. Abstracts from the mini-workshop held October 22--28, 2017 (2017)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
- Hansen, Helle Hvid; Kupke, Clemens; Rutten, Jan: Stream differential equations: specification formats and solution methods (2017)
- Christiansen, David; Brady, Edwin: Elaborator reflection: extending Idris in Idris (2016)
- Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity (rough diamond) (2016)
- Barras, Bruno; Tankink, Carst; Tassi, Enrico: Asynchronous processing of Coq documents: from the kernel up to the user interface (2015)
- Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
- Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
- Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
- Ring, Martin; Lüth, Christoph: Collaborative interactive theorem proving with Clide (2014)
- Wenzel, Makarius: Asynchronous user interaction and tool integration in Isabelle/PIDE (2014)
- Lüth, Christoph; Ring, Martin: A web interface for Isabelle: the next generation (2013)
- Tews, Hendrik: Formalizing cut elimination of coalgebraic logics in Coq (2013)
- Armstrong, Alasdair; Foster, Simon; Struth, Georg: Dependently typed programming based on automated theorem proving (2012)
- Gast, Holger: Engineering the prover interface (2012) ioport
- Jucovschi, Constantin: Cost-effective integration of MKM semantic services into editing environments (2012)
Further publications can be found at: http://proofgeneral.inf.ed.ac.uk/pubs