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.