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.

*[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

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.

- [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

- [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