The Coq mailing list

[Marino Miculan <miculan AT dimi.uniud.it>]

On 02/nov/07, at 14:40, Sébastien Briais wrote:

> Dear all,
>
> I am happy to announce the first public release of
> my formalisation of the spi calculus [3] in the Coq
> proof assistant [1].

I guess this is a good occasion for advertising also our  
formalization of the spi-calculus in Isabelle/Nominal, which we have  
done about one year ago.
See at
   http://www.cs.swan.ac.uk/~csteme/SpiInIsabelle/SpiInIsabelle.html

It contains
- the definition of the spi calculus
- the definitions of several LTS and their properties
- the definitions of frame and frame bisimulation
- the definitions and properties of hedges
- the definition of late hedged bisimulation
- the proof of a "perfect encryption" equation in frame bisimulation
- the proof of a "perfect encryption" equation in hedged bisimulation
- the proof of "impossibility of certain inputs", both in framed and  
in hedged bisimulations

Notably, the usage of Nominal package simplifies the handling of  
binders and names, without using de Bruijn indexes.

All the best
- Temesghen Kahsai and Marino Miculan

--
Marino Miculan - Dept Math Compu Sci, University of Udine
miculan AT dimi.uniud.it
      http://www.dimi.uniud.it/miculan/