[isabelle] Sigma-calculus in Isabelle/HOL


I'd like to announce recent work with Ludovic Henrio on the formalization of Abadi's and Cardelli's Theory of Objects in Isabelle/HOL. We formalized the untyped
sigma calculus and proved confluence.

A Technical report is available here https://hal.inria.fr/inria-00121816 .
We would appreciate comments and experience reports from people who have performed
similar experiments.

Florian Kammueller
Dr. Florian Kammüller, wissenschaftlicher Assistent
Institut für Softwaretechnik und Theoretische Informatik
TU-Berlin, Franklinstr 28/29, 10587 Berlin
Tel +49-30-314 24330

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.