The Coq mailing list

[William DUCK <guillaume.fortaine AT wanadoo.fr>]

Bonjour,

Je m'intéresse actuellement au design des languages pour construire un 
système 
d'exploitation.

Mes recherches m'ont conduit à deux types de logiques :

Hybrid Logic :

http://hylo.loria.fr/

Separation Logic :

http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html

Pensez-vous que Coq et l'une de ces logiques puissent s'accorder ensemble ( 
j'ai vu que vous utilisiez le système Maude : cet outil peut-il m'être 
utile ? )

A la croisée des chemins entre l'informatique et les mathématiques ... :

http://domino.watson.ibm.com/library/CyberDig.nsf/papers/C6C779BBF1650FA4852570670054F3CA/$File/rc23694.pdf

http://www.cs.unm.edu/~fastos/06meeting/PROSE.pdf

http://www.research.ibm.com/K42/papers/osr06-virt.pdf

http://iir.csie.ncku.edu.tw/TFIT2005/Jouannaud.pdf

Cordialement,

                                        Guillaume FORTAINE