Re: [isabelle] [moca] A formalisation of the spi calculus in Coq




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/







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.