PIDE
Isabelle/jEdit -- a prover IDE within the PIDE framework. PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala [2]. The overall aim is to connect LCF-style provers like Isabelle [5, {S}6] (or Coq [5, {S}4] or HOL [5, {S}1]) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
Sorted by year (- Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
- Wenzel, Makarius: Interaction with formal mathematical documents in Isabelle/PIDE (2019)
- Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
- Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
- Hupel, Lars; Kuncak, Viktor: Translating Scala programs to Isabelle/HOL. System description (2016)
- Nakasho, Kazuhisa; Shidama, Yasunari: Documentation generator focusing on symbols for the HTML-ized Mizar library (2015)
- Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)
- Hupel, Lars: Interactive simplifier tracing and debugging in Isabelle (2014)
- Wenzel, Makarius: Asynchronous user interaction and tool integration in Isabelle/PIDE (2014)
- Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart: Pervasive parallelism in highly-trustable interactive theorem proving systems (2013)
- Wenzel, Makarius: Isabelle/jEdit -- a prover IDE within the PIDE framework (2012)