## "Winter 2014" DM meeting

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.

Document Model (DM)
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.