Proof General
From MaRDI portal
Software:17052
No author found.
Related Items (51)
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving ⋮ Unnamed Item ⋮ An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ 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) ⋮ Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega ⋮ Cost-Effective Integration of MKM Semantic Services into Editing Environments ⋮ Isabelle/jEdit – A Prover IDE within the PIDE Framework ⋮ Dependently Typed Programming Based on Automated Theorem Proving ⋮ Unnamed Item ⋮ A proof-centric approach to mathematical assistants ⋮ Supporting the formal verification of mathematical texts ⋮ Hammer for Coq: automation for dependent type theory ⋮ Types for Proofs and Programs ⋮ Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface ⋮ Tactics for hierarchical proof ⋮ Automation for interactive proof: first prototype ⋮ Elaborator reflection: extending Idris in Idris ⋮ The Theorema Environment for Interactive Proof Development ⋮ The Isabelle Framework ⋮ Recycling proof patterns in Coq: case studies ⋮ Mini-workshop: Reflectionless operators: the Deift and Simon conjectures. Abstracts from the mini-workshop held October 22--28, 2017 ⋮ User interaction with the Matita proof assistant ⋮ Click’n Prove: Interactive Proofs within Set Theory ⋮ TacticToe: Learning to Reason with HOL4 Tactics ⋮ 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 ⋮ Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers. ⋮ A Framework for Interactive Proof ⋮ Ott: Effective tool support for the working semanticist ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Saoithín: A Theorem Prover for UTP ⋮ From LCF to Isabelle/HOL ⋮ The Matita Interactive Theorem Prover ⋮ Isabelle as Document-Oriented Proof Assistant ⋮ Towards verified handwritten calculational proofs (short paper) ⋮ Crafting a Proof Assistant ⋮ Interaction with formal mathematical documents in Isabelle/PIDE ⋮ Formal Proof: Reconciling Correctness and Understanding ⋮ CoqPIE: An IDE Aimed at Improving Proof Development Productivity ⋮ Interactive Simplifier Tracing and Debugging in Isabelle ⋮ A Web Interface for Isabelle: The Next Generation ⋮ Formalizing Cut Elimination of Coalgebraic Logics in Coq ⋮ ACL2s: “The ACL2 Sedan” ⋮ Enhancing Theorem Prover Interfaces with Program Slice Information ⋮ Web Interfaces for Proof Assistants ⋮ Tinycals: Step by Step Tacticals ⋮ Isabelle/HOL. A proof assistant for higher-order logic ⋮ Collaborative Interactive Theorem Proving with Clide ⋮ Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
This page was built for software: Proof General
