|
[6]
|
Romain Bardou.
Verification of Pointer Programs Using Regions and Permissions.
Thèse de doctorat, Université Paris-Sud, October 2011.
http://proval.lri.fr/publications/bardou11phd.pdf.
[ bib |
.pdf ]
|
|
[5]
|
Romain Bardou and Claude Marché.
Perle de preuve: les tableaux creux.
In Sylvain Conchon, editor, Vingt-deuxièmes Journées
Francophones des Langages Applicatifs, La Bresse, France, January 2011.
INRIA.
[ bib ]
|
|
[4]
|
Romain Bardou and Claude Marché.
Regions and permissions for verifying data invariants.
Research Report 7412, INRIA, 2010.
http://hal.inria.fr/inria-00525384/en/.
[ bib |
full paper on HAL ]
|
|
[3]
|
Romain Bardou, Jean-Christophe Filliâtre, Johannes Kanig, and Stéphane
Lescuyer.
Faire bonne figure avec Mlpost.
In Vingtièmes Journées Francophones des Langages
Applicatifs, Saint-Quentin sur Isère, January 2009. INRIA.
[ bib |
.pdf ]
Cet article présente Mlpost, une bibliothèque Ocaml de dessin
scientifique. Elle s'appuie sur Metapost, qui permet notamment
d'inclure des fragments LATEX dans les figures. Ocaml offre une
alternative séduisante aux langages de macros LATEX, aux langages
spécialisés ou même aux outils graphiques. En particulier,
l'utilisateur de Mlpost bénéficie de toute l'expressivité
d'Ocaml et de son typage statique. Enfin Mlpost propose un style
déclaratif qui diffère de celui, souvent impératif, des outils existants.
|
|
[2]
|
Romain Bardou.
Ownership, pointer arithmetic and memory separation.
In Formal Techniques for Java-like Programs (FTfJP'08), Paphos,
Cyprus, July 2008.
[ bib |
.pdf ]
|
|
[1]
|
Romain Bardou.
Invariants de classe et systèmes d'ownership.
Master's thesis, Master Parisien de Recherche en Informatique, 2007.
[ bib |
PDF |
.pdf ]
|