Proof General: A generic tool for proof development
From MaRDI portal
Recommendations
- A Framework for Interactive Proof
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The foundation of a generic theorem prover
- Web interfaces for proof assistants
- TPS: A hybrid automatic-interactive system for developing proofs
Cited in
(52)- The RISC ProofNavigator: a proving assistant for program verification in the classroom
- An overview of the Tecton proof system
- Hammer for Coq: automation for dependent type theory
- A formal proof generator from semi-formal proof documents
- Proof General
- An experiment concerning mathematical proofs on computers with French undergraduate students
- A generic graphic framework for combining inference tools and editing proofs and formulae
- From LCF to Isabelle/HOL
- Automation for interactive proof: first prototype
- User interaction with the Matita proof assistant
- System description: GAPT 2.0
- Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
- Enhancing theorem prover interfaces with program slice information
- Web interfaces for proof assistants
- Tool support for proof engineering
- Tinycals: step by step tacticals
- Asynchronous processing of Coq documents: from the kernel up to the user interface
- ProofScript: proof scripting for the masses
- The Isabelle Framework
- Click'n prove: interactive proofs within set theory
- Proviola: a tool for proof re-animation
- Crafting a Proof Assistant
- Formal Proof: Reconciling Correctness and Understanding
- Functional design and implementation of graphical user interfaces for theorem provers
- scientific article; zbMATH DE number 500942 (Why is no real title available?)
- Proof by pointing
- CtCoq: a system presentation
- scientific article; zbMATH DE number 2154392 (Why is no real title available?)
- Recycling proof patterns in Coq: case studies
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)
- Panoptes: an exploration tool for formal proofs
- Managing proof documents for asynchronous processing
- A user interface for a mathematical system that allows ambiguous formulae
- Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- The Matita interactive theorem prover
- Isabelle as document-oriented proof assistant
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- Jape: a calculator for animating proof-on-paper
- A Framework for Interactive Proof
- Interactive simplifier tracing and debugging in Isabelle
- Mathematical Knowledge Management
- Traf: a graphical proof tree viewer cooperating with Coq through Proof General
- Tactics for hierarchical proof
- The HOL-CSP Refinement Toolkit
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- ProofViz: an interactive visual proof explorer
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
This page was built for publication: Proof General: A generic tool for proof development
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729065)
