LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on January 27 2016

Audience

  • Frédéric Boulanger
  • Chantal Keller
  • Safouan Taha
  • Frédéric Tuong
  • Yakoub Nemouchi
  • Romain Aissat
  • Benoît Valiron
  • Burkhart Wolff
  • Lina Ye
  • Thibaut Balabonski

Isabelle Kernel

Burkhart

Burkhart tells Benoit he got his notations wrong in the previous meeting's notes.

Classes

Class system introduced in Isabelle. It has loosely been formalized: see Makarius Wenzels paper at ITP'99. Actually, this is merely a description of how it axiomatically works, without concrete semantic foundation.

Isabelle formalized in Isabelle

Bu shows his formalization of the core ML of Isabelle in Isabelle. The goal: showing that the extension of the kernel to "promises" is sound. This is not completely clear as promises may contains schematic variables, while they are usually forbidden in hypotheses.

The formalization goes up to the definition of the type inference algorithm W. But unlike the original version, because the language allows type annotations, the proof of correctness is in effect non-trivial (and yet unfinished), and the notion of "most-general type" is not completely trivial to state (and to prove).

On this construction Bu constructed a model of the Isabelle kernel.

Note on {$\beta$} equivalence

The kernel heavily depends on {$\beta$}-equivalence. However, it is not considered as computation, as it could be seen in Coq.

Previous meeting -- Next meeting