Prolog infinite trees and automata. - Solange Coupet-Grimal (RAIRO Theor. Informatics Appl., 1991)

Représentation sémantique des langues naturelles en Prolog. - Solange Coupet-Grimal (JFPL, 1993)

On the Use of Advanced Logic Programming Languages in Computational Linguistics. - Solange Coupet-Grimal; Olivier Ridoux (J. Log. Program., 1995)

A System for Modelling and Proving Circuits. - Michel Allemand; Solange Coupet-Grimal; Line Jakubiec; Jean-Luc Paillet (ED&TC, 1996)

Coq and Hardware Verification: A Case Study. - Solange Coupet-Grimal; Line Jakubiec (TPHOLs, 1996)

Analysis of a Guard Condition in Type Theory (Extended Abstract). - Roberto M. Amadio; Solange Coupet-Grimal (FoSSaCS, 1998)

Hardware Verification Using Co-induction in COQ. - Solange Coupet-Grimal; Line Jakubiec (TPHOLs, 1999)

An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions. - Solange Coupet-Grimal (J. Log. Comput., 2003)

Formal Verification of an Incremental Garbage Collector. - Solange Coupet-Grimal; Catherine Nouvet (J. Log. Comput., 2003)

A Functional Scenario for Bytecode Verification of Resource Bounds. - Roberto M. Amadio; Solange Coupet-Grimal; Silvano Dal-Zilio; Line Jakubiec (CSL, 2004)

A Uniform and Certified Approach for Two Static Analyses. - Solange Coupet-Grimal; William Delobel (TYPES, 2004)

Certifying circuits in Type Theory. - Solange Coupet-Grimal; Line Jakubiec (Formal Aspects Comput., 2004)

An effective proof of the well-foundedness of the multiset path ordering. - Solange Coupet-Grimal; William Delobel (Appl. Algebra Eng. Commun. Comput., 2006)