On Thursday 29/01/2015, at 10h30, in room Byron Blanc,
Speaker: Carst Tankink
Title: Proofs as documents: asynchronous interaction for Coq
Abstract:Since the beginning of interactive theorem proving, the actual interaction has been a simple back-and-forth between the user and the prover, with the user providing a command the prover eagerly executes, giving feedback the user then uses to compose a new command. I will present a document-oriented model for Coq proofs (based on Wenzel’s PIDE architectures for Isabelle) that asynchronously updates the proof and processes the results from the prover. This model allows faster (parallel) processing of complete proof scripts, supports a simpler interaction model for readers of formal proofs, and gives a cleaner API for writing third party tools working on top of the proof assistant’s results. I will demonstrate the model and the interactions it allows using the jEdit plugin for Coq.
