19 citations · 70 across the 9 of their papers we have counts for
10 papers
Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode
Klaus Miesenberger, Walther Neuper, Bernhard Stöger +1
The paper collects preparatory work for interdisciplinary collaboration between three partners, between (1) expertise in improving accessibility of studies for impaired individuals…
Interaction with Formal Mathematical Documents in Isabelle/PIDE
Makarius Wenzel
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testif…
Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents
Makarius Wenzel
Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores…
System description: Isabelle/jEdit in 2014
Makarius Wenzel
This is an updated system description for Isabelle/jEdit, according to the official release Isabelle2014 (August 2014). The following new PIDE concepts are explained: asynchronous…
READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
Makarius Wenzel
The LCF tradition of interactive theorem proving, which was started by Milner in the 1970-ies, appears to be tied to the classic READ-EVAL-PRINT-LOOP of sequential and synchronous…
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
Bruno Barras, Lourdes del Carmen González Huesca, Hugo Herbelin +4
This is an overview of the Paral-ITP project, which intents to make the proof assistants Isabelle and Coq fit for the multicore era.
PIDE as front-end technology for Coq
Makarius Wenzel
Isabelle/PIDE is the current Prover IDE technology for Isabelle. It has been developed in ML and Scala in the past 4-5 years for this particular proof assistant, but with an open m…
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
Christoph Lange, Marco B. Caminati, Manfred Kerber +4
Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new…
Isabelle/jEdit --- a Prover IDE within the PIDE framework
Makarius Wenzel
PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LC…
Isabelle/PIDE as Platform for Educational Tools
Makarius Wenzel, Burkhart Wolff
The Isabelle/PIDE platform addresses the question whether proof assistants of the LCF family are suitable as technological basis for educational tools. The traditionally strong log…