Proof General

swMATH4901MaRDI QIDQ17052FDOQ17052

Author name not available (Why is that?)

Cited In (51)

• 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
• Cost-Effective Integration of MKM Semantic Services into Editing Environments
• Dependently Typed Programming Based on Automated Theorem Proving
• 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
• 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
• Ott: Effective tool support for the working semanticist
• Towards verified handwritten calculational proofs (short paper)
• Elaborator reflection: extending Idris in Idris
• Isabelle as document-oriented proof assistant
• 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
• 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
• The Theorema Environment for Interactive Proof Development
• 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
• Enhancing theorem prover interfaces with program slice information
• 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)
• Managing proof documents for asynchronous processing
• TacticToe: learning to reason with HOL4 tactics
• Interactive simplifier tracing and debugging in Isabelle

This page was built for software: Proof General