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.
Abstract:
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.
