Personnes présentes
- Marco David (student ENS Ulm, organiser)
- Thomas Serafini
- Xavier Pigé
- Pierre-Alexandre Bazin
- Timothé Ringeard
- Paul Wang
- Blaž Istenič Ur
- ... and about 8 other students
Presentators
- Burkhart Wolff
Summary:
I give a system-oriented talk for mathematicians and computer-scientist on system architecture, its links to theoretical foundations and the basic pragmatics of the Isabelle interactive proof system.
By the way, there is a list of formalisations of 100 somewhat arbitrarily chosen mathematical challenge proofs, together with a ranking of systems under which these formalisations have been undertaken: The "top 100" of mathematical theorems
Note that Isabelle's versatility of the Isabelle Platform (beyond an interactive theorem proving environment) has been applied for a number of projects such as HOL-TestGen, HOL-OCL, Isabelle/C, and Isabelle_DOF.