The Coq mailing list

[gallais <guillaume.allais AT strath.ac.uk>]

Hi,

I'd like to point out that Interaction Structures are precisely
describing the kind of protocols where some commands are made
available by the fact that other ones were issued earlier on.

A quite simple example of such structures is given in Hancock
and Hyvernat's Programming Interfaces and Basic Topology [1]
on page 18 (4.2 Applications of interaction structures).

Cheers,

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.919

On 07/09/13 21:01, Djamila Baroudi wrote:
> hello;
> I defines a new type called "event" and I still have to define the
> relationship between these events like the sequence between two events,
> which means that event e2 can not happen unless the event e1 is checked.
>
>
>
> Inductive event:Type:=send(msg:string)
> | receive(msg:string)
>
> I try this but it's incorrect:
>
> Inductive activity:Type:=
> evenement(_:event).
> |sequence (e1 e2 : event) : bool := e1 && e2.
>
> can you help me please? n
> Thank you.