Wiki Agenda Contact Version française

Publications 2004

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

Journals

[3] Claude Marché and Xavier Urbain. Modular and incremental proofs of AC-termination. Journal of Symbolic Computation, 38:873--897, 2004. [ bib | http ]
[2] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1--2):89--106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ]
[1] Xavier Urbain. Modular and incremental automated termination proofs. Journal of Automated Reasoning, 32:315--355, 2004. [ bib | .ps.gz ]

Conferences

[6] Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, Verona, Italy, August 2004. ACM Press. [ bib ]
[5] Jean-Christophe Filliâtre and Pierre Letouzey. Functors for Proofs and Programs. In Proceedings of The European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 370--384, Barcelona, Spain, April 2004. [ bib | PDF | .pdf ]
[4] Bart Jacobs, Claude Marché, and Nicole Rauch. Formal verification of a commercial smart card applet with multiple tools. In Algebraic Methodology and Software Technology, volume 3116 of Lecture Notes in Computer Science, Stirling, UK, July 2004. Springer. [ bib ]
[3] Évelyne Contejean. A certified AC matching algorithm. In Vincent van Oostrom, editor, 15th International Conference on Rewriting Techniques and Applications, volume 3091 of Lecture Notes in Computer Science, pages 70--84, Aachen, Germany, June 2004. Springer. [ bib | DOI | Abstract ]
[2] Pierre Corbineau. First-order reasoning in the Calculus of Inductive Constructions. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES 2003 : Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 162--177, Torino, Italy, April 2004. Springer. [ bib | .ps | .ps ]
[1] Jean-Christophe Filliâtre and Claude Marché. Multi-prover verification of C programs. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, 6th International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 15--29, Seattle, WA, USA, November 2004. Springer. [ bib | .ps.gz ]

PhD theses

[3] Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat, Université Paris-Sud, July 2004. [ bib | .ps.gz ]
[2] Jacek Chrzaszcz. Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University, Poland and Université de Paris-Sud, January 2004. [ bib ]
[1] Mihai Rotaru. Sur une théorie unificatrice des modèles de concurrence. PhD thesis, Cluj University, Romania and Université de Paris-Sud, January 2004. [ bib ]

Misc.

Reports

[5] Thierry Hubert. Certification des preuves de terminaison en Coq. Rapport de DEA, Université Paris 7, September 2004. http://www.lri.fr/~marche/hubert04rr.ps. [ bib | .ps ]
[4] Vikrant Chaudhary. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A case study. Technical report, IIT internship report, July 2004. [ bib ]
[3] The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.0, April 2004. http://coq.inria.fr. [ bib | http ]
[2] G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 8.0, April 2004. [ bib | http ]
[1] Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, 2004. [ bib | .ps.gz ]
Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

This page was generated by bibtex2html.