Room “Bleu 2” Fifth floor INRIA Paris-Rocquencourt Antenne: Place d’Italie, 19 February 2014, 16:00-18:00
Participants: Lourdes del Carmen Gonzalez Huesca, Yann Régis-Gianas, Burkhart Wolff.
Yann made an account of the research around incrementality. He explained the incremental approach intended to be used in the document model by means of an experiment of a typechecker for a simple typed lambda calculus. The discussion went through the way to represent the knowledge base, from a graph model using dependency graphs, as it is proposed by Makarius, to a simple store of verified terms. The reuse of information must be restricted, the constraints are syntax directed and they intuitively define a border in the space of research for a limited scope setting the reusable data. Yann emphasized the idea of a continuous description of change and this is the principal line of research with Lourdes: to develop a technique for incrementality that could be applied to the interactive proof developments of Coq.