Feb 2013: This web page has moved THERE

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.

- 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