Paral-ITP Publications

Papers

Isabelle/jEdit — a Prover IDE within the PIDE framework, by Makarius Wenzel. In J. Jeuring et-al, editors, Conference on Intelligent Computer Mathematics (CICM 2012). Springer LNAI 7362, 2012.

Designing a state transaction machine for Coq (with slides), by Bruno Barras and Enrico Tassi. Presented at the Coq Workshop 2012.

Paral-ITP Front-End Technologies (interim report), by Makarius Wenzel.

READ-EVAL-PRINT in Parallel and Asynchronous Proof-Checking (with slides), by Makarius Wenzel. Presented at User Interfaces for Theorem Provers (UITP 2012). Workshop postproceedings in EPTCS, 2013.

Shared-Memory Multiprocessing for Interactive Theorem Proving, by Makarius Wenzel. In S. Blazy, C. Paulin-Mohring, D. Pichardie, editors, Interactive Theorem Proving (ITP 2013). To appear in Springer LNCS. 2013.

PIDE as front-end technology for Coq, by Makarius Wenzel.

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems, by Bruno Barras, Hugo Herbelin, Lourdes del Carmen González Huesca, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff. In J. Carette et al, editors, Conference on Intelligent Computer Mathematics (CICM 2013), 2013. Springer LNCS 7961.

System description: Isabelle/jEdit in 2014 (with slides), by Makarius Wenzel. Presented at User Interfaces for Theorem Provers (UITP) Workshop, Vienna Summer of Logic, July 2014.

Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (with slides), by Makarius Wenzel. In G. Klein and R. Gamboa, editors, Interactive Theorem Proving (ITP 2014). 2014. Springer, LNCS 8558.

Isabelle/jEdit, by Makarius Wenzel. User manual for Isabelle2014 release, August 2014.

Paral-ITP Front-End Technologies (second interim report), by Makarius Wenzel, with contributions by Carst Tankink.

Coqoon - An IDE for Interactive Proof Development in Coq, by Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink. In TACAS 2016, LNCS.

Asynchronous processing of Coq documents: from the kernel up to the user interface, by Bruno Barras, Carst Tankink, Enrico Tassi. In ITP 2015, LNCS.

Tutorials

Isabelle/HOL tutorial at LRI, by Makarius Wenzel and Abdou Feliachi.

Isabelle tutorial at LIFO (Orleans), by Makarius Wenzel and Abdou Feliachi.

Isabelle short course at Edinburgh, by Makarius Wenzel, Gudmund Grov, Grant Passmore.

Isabelle tutorial at ENS Paris, by Makarius Wenzel and Timothy Bourke.

Talks

Talk at the LTP-LACMA-Meeting in Orleans, Burkhart Wolff.

Parallel and asynchronous interactive theorem proving in Isabelle — from READ-EVAL-PRINT to continuous processing of proof documents, by Makarius Wenzel. Presented at LRI, Orsay, September 2013.

Front-end Technologies for Formal-Methods Tools, by Makarius Wenzel. Presented at LRI, Orsay, November 2013.

Document-oriented Prover Interaction with Isabelle/PIDE, by Makarius Wenzel. Presented at Radboud University Nijmegen, December 2013.

Isabelle/jEdit for seasoned Isabelle users, by Makarius Wenzel. Presented at Isabelle Workshop, Vienna Summer of Logic, July 2014.

Ph.D. Theses

Incrementality and effect simulation in the Simply Typed Lambda Calculus, by Lourdes del Carmen González Huesca, 27 November 2015.

Posters

A poster presentation of the project from 2014.

The presentation at the ANR 2ème édition des Rencontres du numérique: Poster, Slides.