Vendredi 12 Décembre

Retour à la vue des calendrier
Vendredi 12 Décembre
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Asynchronous Interaction with Theorem Provers: ProofGeneral's Last March
Description: Carst Tankink This year ProofGeneral, the generic Emacs-interface for proof assistants, celebrates its 20th birthday. The tool is showing its age, however, by only allowing a user to work at a single point at the time, and having to re-evaluate an entire proof script in reaction to changes at the beginning. In this talk, I will discuss our recent efforts to changing this situation: based on a previous endeavour in Isabelle, we have adapted the Coq proof assistant to work with the jEdit text editor. This editor has no user-visible notion of "State": the entire proof is always available to the proof assistant, allowing it to react to changes in the document in a more intelligent manner: by scheduling proofs in parallel and by postponing computation that are of no direct interest to the author. I will not go into full technical details in this talk, but give a demo of the current prototype, and discuss the ramifications of such a model in the longer term.