Wiki Agenda Contact English version

Publications 2005

Retour

Livres / Revues / Conférences / Thèses / Divers / Rapports

Livres et chapitres de livres

Revues

[3] Sava Krstić and Sylvain Conchon. Canonization for disjoint unions of theories. Information and Computation, 199(1-2):87--106, May 2005. [ bib ]
[2] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95:446--453, 2005. [ bib ]
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs
[1] Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain. Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning, 34(4):325--363, 2005. [ bib | DOI | Abstract ]

Conférences

[16] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ]
[15] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ]
[14] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05) [15]. [ bib ]
[13] Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ]
[12] Nicolas Oury. Extensionality in the Calculus of Constructions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 278--293. Springer, August 2005. [ bib ]
[11] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179--194. Springer, August 2005. [ bib | .ps ]
[10] Louis Mandel and Marc Pouzet. ReactiveML, a Reactive Extension to ML. In ACM International Conference on Principles and Practice of Declarative Programming (PPDP), pages 82--93, Lisboa, July 2005. [ bib | PDF | .pdf ]
[9] Évelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In Robert Nieuwenhuis, editor, 20th International Conference on Automated Deduction (CADE-20), volume 3632 of Lecture Notes in Artificial Intelligence, pages 7--22, Tallinn, Estonia, July 2005. Springer. [ bib | DOI | Abstract ]
[8] June Andronick, Boutheina Chetali, and Christine Paulin-Mohring. Formal verification of security properties of smart card embedded source code. In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, International Symposium of Formal Methods Europe (FM'05), volume 3582 of Lecture Notes in Computer Science, Newcastle,UK, July 2005. Springer. [ bib ]
[7] Louis Mandel and Farid Benbadis. Simulation of mobile ad hoc network protocols in ReactiveML. In Proceedings of Synchronous Languages, Applications, and Programming (SLAP'05), Edinburgh, Scotland, April 2005. Elsevier Science Publishers. [ bib | PDF | .pdf ]
[6] Julien Signoles. Une approche fonctionnelle du modèle vue-contrôleur. In Seizièmes Journées Francophones des Langages Applicatifs, pages 63--78. INRIA, March 2005. [ bib ]
[5] Louis Mandel and Marc Pouzet. ReactiveML, un langage pour la programmation réactive en ML. In Seizièmes Journées Francophones des Langages Applicatifs, pages 1--16. INRIA, March 2005. [ bib | .ps ]
[4] Pierre Corbineau. Skip lists et arbres binaires de recherche probabilistes. In Seizièmes Journées Francophones des Langages Applicatifs, pages 99--112. INRIA, March 2005. [ bib ]
[3] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Seizièmes Journées Francophones des Langages Applicatifs, pages 79--94. INRIA, March 2005. [ bib | .ps.gz ]
[2] Sylvie Boldo and Jean-Michel Muller. Some functions computable with a fused-mac. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th Symposium on Computer Arithmetic, pages 52--58, Cape Cod, USA, 2005. [ bib | .pdf ]
[1] G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In R. Gorrieri, F. Martinelli, P. Ryan, and S. Schneider, editors, Proceedings of FAST'05, volume 3866 of Lecture Notes in Computer Science, pages 112--126. Springer, 2005. [ bib ]

Thèses

[2] Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ]
[1] Pierre Corbineau. Démonstration Automatique en Théorie des Types. Thèse de doctorat, Université Paris-Sud, September 2005. [ bib ]

Divers

[2] Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors. Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers, volume 3839 of Lecture Notes in Computer Science. Springer, 2005. [ bib ]
[1] Évelyne Contejean. Coccinelle, 2005. http://www.lri.fr/~contejea/Coccinelle/coccinelle.html. [ bib | www: ]

Rapports

[3] Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Research Report DSIC II/01/05, Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Spain, February 2005. [ bib ]
[2] Matthieu Sozeau. Coercion par prédicats en Coq. Master's thesis, Université Paris 7, 2005. In French. [ bib | .pdf ]
[1] Nicolas Ayache. Coopération d'outils de preuve interactifs et automatiques. Master's thesis, Université Paris 7, 2005. [ bib ]
Retour

Livres / Revues / Conférences / Thèses / Divers / Rapports

This page was generated by bibtex2html.