Ludovic Henrio

Home     |     Publications     |     Talks     |     Students     |     Projects      |     Formal proofs

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)

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:

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

Algorithms for Distributed Systems

Previous Works