The Coq mailing list

[Samuel Colin <scolin-lists AT hivernal.org>]

> Hai WAN wrote:
> > Dear all,
> >
Greetings,

> > Is there any existing implementation of duration calculus in Coq? I
> > searched using Google and only found one paper. The implementation
> > mentioned in the paper is not available.
> >
Well, now it is, it took me some time from the moment I saw your post on
the Coq-club list to fill in the webpage and add licensing information to
the files. Here you are:

http://hivernal.org/static/about/phd-thesis.en.html

Be aware that this is the work of a beginner in Coq (version 8.0) with a
somewhat exotic logic, though.

> > Can anyone help? Thanks in advance.
>
Hope this helps. Do not hesitate to ask me if you have any more question
about this.

Dixit Yves Bertot 
<Yves.Bertot AT sophia.inria.fr>
 : 
>>
>>
> What paper are you talking about?
> 
I guess that would be me, AFAIK no other person attempted an implementation
of duration calculus in Coq (at least when I looked for it a few years
ago, maybe the situation is better now in this regard).

-- 
Samuel Colin
E-mail: 
scolin AT hivernal.org
Informations: http://hivernal.org/static/about/