During the two weeks of 17..28-Jun-2019, I will be visiting Deducteam at LSV, Paris/Cachan. There will be two presentations about Isabelle technology for formal documents and libraries:
- Interaction with Formal Mathematical Documents in Isabelle/PIDE – Tuesday 18-Jun-2019, 11:00, Pavillon du Jardin, ENS Cachan.
- Isabelle technology for the Archive of Formal Proofs – Thursday 20-Jun-2019, 14:00, LSV library.
See also the official announcement of Deducteam.
Note: These talks will be repeated at the Conference on Intelligent Computer Mathematics (CICM 2019), Prague (CZ), 08..12-Jul-2019.
At the Conference for Intelligent Computer Mathematics (CICM 2019) in Prague (08..12-Jul-2019), I will give a keynote presentation on the track Mathematical Knowledge Management (MKM).
- Interaction with Formal Mathematical Documents in Isabelle/PIDE
- 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) testifies the success of such applications of formalized mathematics in Isabelle/HOL. More recently, the scope of PIDE has widened towards languages that are not connected to logic and proof in Isabelle, but taken from a broader repertoire of mathematics on the computer. The present paper provides a general overview of the PIDE project and its underlying document model, with built-in parallel evaluation and asynchronous interaction. There is also some discussion of original aims and approaches, successes and failures, later changes to the plan, and ideas for the future.
- Preprint from ArXiv