| 2025 | FORTE | An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. | Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2024 | ITP | Typed Compositional Quantum Computation with Lenses. | Jacques Garrigue, Takafumi Saikawa |
| 2019 | ITP | Proving Tree Algorithms for Succinct Data Structures. | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka |
| 2018 | ISITA | Examples of Formal Proofs about Data Compression. | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2016 | ICFEM | Formal Verification of the rank Algorithm for Succinct Data Structures. | Akira Tanaka, Reynald Affeldt, Jacques Garrigue |
| 2016 | ISITA | Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2015 | ITP | Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. | Reynald Affeldt, Jacques Garrigue |
| 2013 | APLAS | Ambivalent Types for Principal Type Inference with GADTs. | Jacques Garrigue, Didier Rmy |
| 2011 | OOPSLA | A syntactic type system for recursive modules. | Hyeonseung Im, Keiko Nakata, Jacques Garrigue, Sungwoo Park |
| 2010 | APLAS | A Certified Implementation of ML with Structural Polymorphism. | Jacques Garrigue |
| 2006 | APLAS | Private Row Types: Abstracting the Unnamed. | Jacques Garrigue |
| 2006 | ICFP | Recursive modules for programming. | Keiko Nakata, Jacques Garrigue |
| 2004 | FLOPS | Relaxing the Value Restriction. | Jacques Garrigue |
| 2002 | APLAS | Relaxing the Value Restriction. | Jacques Garrigue |
| 2001 | APLAS | Simple Type Inference for Structural Polymorphism. | Jacques Garrigue |
| 1998 | ICFP | On the Runtime Complexity of Type-Directed Unboxing. | Yasuhiko Minamide, Jacques Garrigue |
| 1994 | POPL | The Typed Polymorphic Label-Selective lambda-Calculus. | Jacques Garrigue, Hassan At-Kaci |