"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.