The following pages link to Proof General (Q17052):
Displaying 50 items.
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers. (Q704168) (← links)
- Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega (Q841687) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Mini-workshop: Reflectionless operators: the Deift and Simon conjectures. Abstracts from the mini-workshop held October 22--28, 2017 (Q1731959) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- An experiment concerning mathematical proofs on computers with French undergraduate students (Q1884267) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Interaction with formal mathematical documents in Isabelle/PIDE (Q2287890) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- User interaction with the Matita proof assistant (Q2462635) (← links)
- CoqPIE: An IDE Aimed at Improving Proof Development Productivity (Q2829283) (← links)
- A Web Interface for Isabelle: The Next Generation (Q2843032) (← links)
- Formalizing Cut Elimination of Coalgebraic Logics in Coq (Q2851950) (← links)
- ACL2s: “The ACL2 Sedan” (Q2867932) (← links)
- Enhancing Theorem Prover Interfaces with Program Slice Information (Q2867933) (← links)
- Web Interfaces for Proof Assistants (Q2867935) (← links)
- Tinycals: Step by Step Tacticals (Q2867943) (← links)
- Collaborative Interactive Theorem Proving with Clide (Q2879270) (← links)
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (Q2879273) (← links)
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving (Q2881098) (← links)
- Cost-Effective Integration of MKM Semantic Services into Editing Environments (Q2907317) (← links)
- Isabelle/jEdit – A Prover IDE within the PIDE Framework (Q2907353) (← links)
- Dependently Typed Programming Based on Automated Theorem Proving (Q2908568) (← links)
- Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface (Q2945623) (← links)
- (Q2980965) (← links)
- Elaborator reflection: extending Idris in Idris (Q2985777) (← links)
- Saoithín: A Theorem Prover for UTP (Q3055742) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Click’n Prove: Interactive Proofs within Set Theory (Q3559759) (← links)
- Crafting a Proof Assistant (Q3612433) (← links)
- Formal Proof: Reconciling Correctness and Understanding (Q3637280) (← links)
- TacticToe: Learning to Reason with HOL4 Tactics (Q4645730) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) (Q5049030) (← links)
- Managing Proof Documents for Asynchronous Processing (Q5166497) (← links)
- A User Interface for a Mathematical System that Allows Ambiguous Formulae (Q5166498) (← links)
- Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit (Q5170238) (← links)
- Ott: Effective tool support for the working semanticist (Q5189646) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- The Matita Interactive Theorem Prover (Q5200015) (← links)
- Isabelle as Document-Oriented Proof Assistant (Q5200122) (← links)
- (Q5219926) (← links)
- The Theorema Environment for Interactive Proof Development (Q5387844) (← links)
- A Framework for Interactive Proof (Q5428268) (← links)
- Interactive Simplifier Tracing and Debugging in Isabelle (Q5495933) (← links)
