Web Interfaces for Proof Assistants

DOI10.1016/j.entcs.2006.09.021zbMath1278.68266OpenAlexW2169030566WikidataQ108482197 ScholiaQ108482197MaRDI QIDQ2867935

Cezary Kaliszyk

Publication date: 20 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.09.021

zbMATH Keywords

interfacewebproof assistantCoqasynchronous DOM modification

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Related Items

A User-friendly Interface for a Lightweight Verification System, Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit, HOL(y)Hammer: online ATP service for HOL Light, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• Coq
• Isabelle/HOL
• Proof General
• C-CoRN
• OMDoc
• Proof General Kit
• Epigram
• Pcoq
• Whelp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Knowledge representation and management in ACTIVEMATH
• Ωmega: Towards a mathematical assistant
• Mathematical Knowledge Management
• Advanced Functional Programming
• Types for Proofs and Programs