Solange Coupet-Grimal



Conférences invitées (Invited talks)

Logique et cartes à puce, pdf. Journée "Mathématiques au féminin en Méditérannée", organisée par l'association Femmes et Mathématiques. Marseille, 8 Novembre 2003.

Un exemple de certification de logiciel. Colloque International Espace Mathématique Francophone. Tozeur, 19-23, Décembre 2003.


Publications



A Constructive Axiomatization of the Recursive Path Ordering, with William Delobel. 2006. Soumis.


An Effective Proof of the Well-Foundedness of the Multiset Path Ordering
, with William Delobel
. AAECC Journal
(Applicable Algebra in Engineering Communication and Computing
) Vol 17 No 6, pp 453-469, Dec 2006, Springer Berlin / Heidelberg. Contribution to the CoLoR Library.

Une preuve effective de la bonne fondation de l'ordre récursif multi-ensemble sur les chemins, avec William Delobel,  Les Journées Francophones des Langages Applicatifs,  JFLA 2006. Contribution à la bibliothèque  CoLoR. (Version préliminaire de l'article ci-dessus).

A Uniform and Certified Approach for Two Static Analyses with William Delobel,  post-proceedings of Types 2004, Filliatre and al Eds., © Springer LNCS 3839, pp 116-138, 2006. Also RR LIF  27-2005

Des Preuves et des Programmes, ps.gz, pdf, Habilitation à Diriger des Recherches, Université de Provence, Aix-Marseille I, Septembre 2004. Photo (Picture).

A Functional Scenario for Bytecode Verification of Space Bounds, (long version) with  Roberto Amadio, Silvano Dal Zilio, Line Jakubiec, the Annual Conference of the European Association for Computer Science Logic,  CSL'O4, J.Marcinkowski, A.Tarlecki Eds., LNCS 3210 pp 265-279. RR LIF 17-2004

Short Presentation: A Functional Scenario for Bytecode Verification of Space Bounds, with Roberto Amadio, Silvano Dal Zilio, Line Jakubiec, Space 2004, Second workshop on  Semantics, Program Analysis, and Computing Environments  for Memory Management. Venice, Italy.

Certifying circuits in Type Theory,  with Line Jakubiec. © Springer-Verlag.  Formal Aspects of Computing, Vol 16 No 4, pp 352 - 373, Nov 2004 .  Also   RR  LIF 03-2002 

Formal Verification of an Incremental Garbage Collector , with Catherine Nouvet,  The Journal of Logic and Computation, Vol 13 No  6, pp 815-833, 2003.

An Axiomatization of Linear Temporal Logic in The Calculus of Inductive Constructions,  The Journal of Logic and Computation, Vol 13 No 6, pp 801-813, 2003.

Hardware Verification using Co-Induction in Coq,  with Line Jakubiec, International Conference on Theorem Proving in Higher Order Logics, TPHOLS'99, LNCS 1690 Springer Verlag, Nice, France, 1999, pp  91-108.

Analysis of a guard condition in type theory, with Roberto Amadio, First Int. Conf Foundations of Software Science and Computation Structures, FoSSaCS'98,  M.Nivat Ed.,LNCS 1378. Springer Verlag, Lisbonne, Portugal, 1998, pp 48-62.

A Comparison of the Coq and HOL proof systems for Specifying Hardware, with Paul Curzon and Line Jakubiec, 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLS'97, Murray Hill, USA, 1997, Supplementary Proceedings pp 63-78.

Coq and Hardware Verification : a Case Study, with Line Jakubiec, International Conference on Theorem Proving in Higher Oreder Logics, TPHOLS'96, LNCS 1125, Springer Verlag, Turku, Finlande, 1996, pp 125-140.

A Formal System for Correct Hardware Design, with Michel Allemand & Jean-Luc Paillet, Proceedings of ATW'96 also published in Embedded System Applications, Kluver Academic Publishers, pp 45-69, 1996.

A System for Modelling and Proving Circuits, with Michel Allemand & Jean-Luc Paillet, ED & TC'96 (IEEE European Design and Test Conference and Exhibition) Paris, Mars 1996 (long version, short version, poster version).

Formath: A system for Modelling and Proving Circuits, with  Michel Allemand & Jean-Luc Paillet, CHARME'95 (Correct Hardware Design and Verification Methods) (long version, poster), Frankfurt, Octobre 1995.

On the use of advanced Logics Programming Features in Computational linguistics, with  Olivier Ridoux, The Journal of Logic Programming, 24 (1-2), 1995, pp 121-159  (abstract).

Représentation sémantique dans le traitement des langues naturelles en PrologJFLP'93, 2émes Journées Francophones de Programmation en Logique,  Telkea, Nîmes, 1993, pp 69- 90.

Prolog Infinite Trees and Automata, Theoretical Informatics and Applications, 25, n°5, 1991, pp 397-418.

Foncteur de Kleene et Programmation Logique, avec Georges Blanc et Noëlle Bleuzen-Guernalec, RR89-15, Laboratoire de Mathé matiques de Marseille URA 225.

Deux arguments pour les arbres infinis en Prolog, Thèse de spécialité, Université d'Aix-Marseille II, 29 Novembre 1988.

Coq Users Contributions

An axiomatization of Linear Temporal Logic
Equivalence notions on labelled transitions systems
Verification and synthesis of hardware linear arithmetic structures