Ludovic Henrio

Mechanised Formalisation in Isabelle/HOL

You will find here the source files for a few mechanised theories done in Isabelle/HOL. Some of the source files necessitate to run an old version of the Isabelle/HOL theorem prover, because unfortunately Isabelle does not necessarily ensure backward compatibility.

Object calculus Formalisation

Written with Florian Kammüller, a formalisation of multi-active objects (published in COORDINATION'13)

[03/2015] Multiactive objects: MultiASP: formalisation of the Semantics. Written for Isabelle 2014

Together with Florian Kammüller, Bianca Lutz and Henry Sudhof, we developped the following Isabelle theory for mechanizing the reasoning on (distributed) objects, here are several versions:

Sigma calculus with proof of confluence (published in FMOODS'07). These proofs have been performed with an old version of Isabelle: Isabelle 2005, that can be found there

ASP_fun with typing, i.e. a functional distributed object calculus, with a typing theory, the main features present in this file are (Necessitates Isabelle 2008, that can be found there):
- Each method now has a second parameter
- Definition of futures, active objects, requests, ...
- Properties of the calculus: well-formed configurations and absence of cycles
- typing comes with subject-reduction and progress
- Includes a proof that sigma-calculus (with the second parameter) is confluent
[10/2010] A formalisation with Locally nameless technique is available (in Isabelle 2009)

Component Model Formalisation

The objective of this formalisation is to provide a framework for reasoning on distributed component models, component configuration, components at runtime, and futures. Participants to this formalisation were: Muhammad Khan, Florian Kammüller, and Ludovic Henrio

[03/2010] Asynchronous Components and Futures GCM + Reconfigurations + Future update strategies and proofs. Necessitates Isabelle2009.

Algorithms for Distributed Systems

[06/2012] Broadcast for CAN Formalisation of a CAN network together with a broadcast algorithm. Necessitates Isabelle2011.
NEW! we proved existence of an optimal broadcast
Work realised with Francesco Bongiovanni

Previous Works

[03/2009] Formalisation of an asynchronous component model based on the GCM component model, published in FMCO 2008. Necessitates Isabelle 2008, that can be found there