swMATH4901MaRDI QIDQ17052FDOQ17052
Author name not available (Why is that?)
Official website: http://proofgeneral.inf.ed.ac.uk/
Cited In (92)
- Cost-Effective Integration of MKM Semantic Services into Editing Environments
- Dependently Typed Programming Based on Automated Theorem Proving
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Enhancing theorem prover interfaces with program slice information
- Managing proof documents for asynchronous processing
- Interactive simplifier tracing and debugging in Isabelle
- User interaction with the Matita proof assistant
- Mini-workshop: Reflectionless operators: the Deift and Simon conjectures. Abstracts from the mini-workshop held October 22--28, 2017
- Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega
- Collaborative Interactive Theorem Proving with Clide
- A user interface for a mathematical system that allows ambiguous formulae
- Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers.
- Formal Proof: Reconciling Correctness and Understanding
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
- Formalizing cut elimination of coalgebraic logics in Coq
- ProofWidgets
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- An experiment concerning mathematical proofs on computers with French undergraduate students
- The Isabelle Framework
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
- Isabelle/HOL. A proof assistant for higher-order logic
- Types for Proofs and Programs
- Web interfaces for proof assistants
- Click'n prove: interactive proofs within set theory
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- ACL2s: ``the ACL2 sedan
- FEPG
- Isar
- IsaWin
- CliffMath
- CliffSymNil
- CliffOC
- TAS
- Genius
- Matita
- Saoithin
- Isabelle/jEdit
- PIDE
- Clide
- Isabelle/PIDE
- MathBrush
- Ott: Effective tool support for the working semanticist
- Coq/SSReflect
- Epigram
- jEdit
- Mella
- Proof General Kit
- CtCoq
- iJulienne
- Pcoq
- PhoX
- CLT
- Poly/ML
- Coqoon
- Hat
- SigmaKEE
- Towards verified handwritten calculational proofs (short paper)
- Elaborator reflection: extending Idris in Idris
- Isabelle as document-oriented proof assistant
- numericaluniversality
- LOUI
- XBarnacle
- CoqPIE
- PeaCoq
- SUMO
- SWT
- Bedrock
- DrACuLa
- Whelp
- Tinycals: step by step tacticals
- Recycling proof patterns in Coq: case studies
- Tactics for hierarchical proof
- Interactive theorem proving from the perspective of Isabelle/Isar
- From LCF to Isabelle/HOL
- Interaction with formal mathematical documents in Isabelle/PIDE
- A Framework for Interactive Proof
- The Theorema Environment for Interactive Proof Development
- jsCoq
- Crafting a Proof Assistant
- Isabelle/jEdit – A Prover IDE within the PIDE Framework
- Saoithín: a theorem prover for UTP
- Asynchronous processing of Coq documents: from the kernel up to the user interface
- The Matita interactive theorem prover
- A web interface for Isabelle: the next generation
- Hammer for Coq: automation for dependent type theory
- Stream differential equations: specification formats and solution methods
- Automation for interactive proof: first prototype
- Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
- TacticToe: learning to reason with HOL4 tactics
This page was built for software: Proof General
