Séminaire Marelle : Interfacing with Coq

On Monday 28/09/2009, at 14h, in room Byron Blanc.

Speaker: Thomas Hutchinson.

Title: Interfacing with Coq – Encoding Coq’s tactic language in XML.

I will present my work on encoding the tactic language in XML. There will be a demonstration of Coq starting an external program which returns a piece of ltac. Implementation details will be discussed. Comments are requested for the direction of future work. This is a preparation for the demo I am to give at the Journées des ARC, ADT et AEx, 29/09/2009 – 01/10/2009, in Bordeaux.