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
• A Web Interface for Isabelle: The Next Generation
• Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
• Collaborative Interactive Theorem Proving with Clide
• Cost-Effective Integration of MKM Semantic Services into Editing Environments
• Dependently Typed Programming Based on Automated Theorem Proving
• Saoithín: A Theorem Prover for UTP
• CoqPIE: An IDE Aimed at Improving Proof Development Productivity
• 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
• Title not available (Why is that?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• An experiment concerning mathematical proofs on computers with French undergraduate students
• Isabelle as Document-Oriented Proof Assistant
• 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
• Formalizing Cut Elimination of Coalgebraic Logics in Coq
• Web interfaces for proof assistants
• TacticToe: Learning to Reason with HOL4 Tactics
• ACL2s: ``the ACL2 sedan
• Title not available (Why is that?)
• Ott: Effective tool support for the working semanticist
• The Matita Interactive Theorem Prover
• Towards verified handwritten calculational proofs (short paper)
• Elaborator reflection: extending Idris in Idris
• Tinycals: step by step tacticals
• Managing Proof Documents for Asynchronous Processing
• Recycling proof patterns in Coq: case studies
• Tactics for hierarchical proof
• Interactive Simplifier Tracing and Debugging in Isabelle
• 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
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Crafting a Proof Assistant
• A User Interface for a Mathematical System that Allows Ambiguous Formulae
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
• Click’n Prove: Interactive Proofs within Set Theory
• Hammer for Coq: automation for dependent type theory
• Enhancing theorem prover interfaces with program slice information
• Automation for interactive proof: first prototype

This page was built for software: Proof General