Web interfaces for proof assistants

DOI10.1016/J.ENTCS.2006.09.021zbMATH Open1278.68266OpenAlexW2169030566WikidataQ108482197 ScholiaQ108482197MaRDI QIDQ2867935FDOQ2867935

Authors: 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

Recommendations

• A web interface for Isabelle: the next generation
• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 2154392
• Collaborative Interactive Theorem Proving with Clide
• Proviola: a tool for proof re-animation

zbMATH Keywords

interfaceCoqproof assistantwebasynchronous DOM modification

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Mathematical Knowledge Management
• \(\Omega\)\textsc{mega}: towards a mathematical assistant
• Types for Proofs and Programs
• Isabelle/HOL. A proof assistant for higher-order logic
• Knowledge representation and management in ACTIVEMATH
• Title not available (Why is that?)
• Advanced Functional Programming

Cited In (8)

• A user-friendly interface for a lightweight verification system
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Title not available (Why is that?)
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Crafting a Proof Assistant
• Proviola: a tool for proof re-animation
• A web interface for Isabelle: the next generation

Uses Software

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

This page was built for publication: Web interfaces for proof assistants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2867935)