| 2026 | ICGT | Parallel Transformations as Colimits. | Thierry Boy de la Tour |
| 2008 | CADE | Unification and Matching Modulo Leaf-Permutative Equational Presentations. | Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran |
| 2004 | CADE | Overlapping Leaf Permutative Equations. | Thierry Boy de la Tour, Mnacho Echenim |
| 2003 | LPAR | NP-Completeness Results for Deductive Problems on Stratified Terms. | Thierry Boy de la Tour, Mnacho Echenim |
| 2002 | CADE | A Note on Symmetry Heuristics in SEM. | Thierry Boy de la Tour |
| 2000 | AISC | Some Techniques of Isomorph-Free Search. | Thierry Boy de la Tour |
| 1996 | CADE | Ground Resolution with Group Computations on Semantic Symmetries. | Thierry Boy de la Tour |
| 1995 | IJCAI | On the Complexity of Extending Ground Resolution with Symmetry Rules. | Thierry Boy de la Tour, Stphane Demri |
| 1992 | LPAR | Building Proofs by Analogy via the Curry-Horward Isomorphism. | Thierry Boy de la Tour, Christoph Kreitz |
| 1990 | AIMSA | The Use of Renaming to Improve the Effeciency of Clausal Theorem Proving. | Thierry Boy de la Tour, Gilles Chaminade |
| 1990 | CADE | Minimizing the Number of Clauses by Renaming. | Thierry Boy de la Tour |
| 1988 | CADE | Some Tools for an Inference Laboratory (ATINF). | Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade |
| 1988 | ISSAC | A Formal Approach to some Usually Informal Techniques Used in Mathematical Reasoning. | Thierry Boy de la Tour, Ricardo Caferra |
| 1988 | STACS | Some Tools for an Inference Laboratory (ATINF). | Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade |
| 1987 | AAAI | Proof Analogy in Interactive Theorem Proving: A Method to Express and Use It via Second Order Pattern Matching. | Thierry Boy de la Tour, Ricardo Caferra |