The Typed Polymorphic Label-Selective lambda-Calculus. - Jacques Garrigue; Hassan Aït-Kaci (POPL, 1994)

The Transformation Calculus. - Jacques Garrigue (FSTTCS, 1995)

Label-Selective lambda-Calculus Syntax and Confluence. - Hassan Aït-Kaci; Jacques Garrigue (Theor. Comput. Sci., 1995)

Extending ML with Semi-Explicit Higher-Order Polymorphism. - Jacques Garrigue; Didier Rémy (TACS, 1997)

On the Runtime Complexity of Type-Directed Unboxing. - Yasuhiko Minamide; Jacques Garrigue (ICFP, 1998)

Semi-Explicit First-Class Polymorphism for ML. - Jacques Garrigue; Didier Rémy (Inf. Comput., 1999)

Simple Type Inference for Structural Polymorphism. - Jacques Garrigue (APLAS, 2001)

Relaxing the Value Restriction. - Jacques Garrigue (APLAS, 2002)

SOBA Framework: An Application Framework for Broadband Network Environment. - Nobuaki Yoshida; Yoshio Hayashi; Yutaka Tamagaki; Shoji Urashita; Makoto Kakuta; Masahiro Watanabe; Jacques Garrigue; Reiji Nakajima (SAINT, 2005)

Private Row Types: Abstracting the Unnamed. - Jacques Garrigue (APLAS, 2006)

Recursive modules for programming. - Keiko Nakata 001; Jacques Garrigue (ICFP, 2006)

A Certified Implementation of ML with Structural Polymorphism. - Jacques Garrigue (APLAS, 2010)

A syntactic type system for recursive modules. - Hyeonseung Im; Keiko Nakata 001; Jacques Garrigue; Sungwoo Park (OOPSLA, 2011)

Path resolution for nested recursive modules. - Jacques Garrigue; Keiko Nakata 001 (High. Order Symb. Comput., 2011)

Ambivalent Types for Principal Type Inference with GADTs. - Jacques Garrigue; Didier Rémy (APLAS, 2013)

Summer School on Coq (NII Shonan Meeting 2014-9). - Pierre Castéran; Jacques Garrigue; David Nowak (NII Shonan Meet. Rep., 2014)

Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. - Reynald Affeldt; Jacques Garrigue (ITP, 2015)

GADTs and Exhaustiveness: Looking for the Impossible. - Jacques Garrigue; Jacques Le Normand (ML Family/OCaml, 2015)

A certified implementation of ML with structural polymorphism and recursive types. - Jacques Garrigue (Math. Struct. Comput. Sci., 2015)

Formal Verification of the rank Algorithm for Succinct Data Structures. - Akira Tanaka; Reynald Affeldt; Jacques Garrigue (ICFEM, 2016)

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2016)

An Intuitionistic Set-theoretical Model of CCω. - Masahiro Sato; Jacques Garrigue (J. Inf. Process., 2016)

Examples of Formal Proofs about Data Compression. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2018)

Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. - Akira Tanaka; Reynald Affeldt; Jacques Garrigue (J. Inf. Process., 2018)

Proving Tree Algorithms for Succinct Data Structures. - Reynald Affeldt; Jacques Garrigue; Xuanrui Qi; Kazunari Tanaka (ITP, 2019)

Lightweight Linearly-typed Programming with Lenses and Monads. - Keigo Imai; Jacques Garrigue (J. Inf. Process., 2019)

Formal Adventures in Convex and Conical Spaces. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (CICM, 2020)

An Intuitionistic Set-theoretical Model of Fully Dependent CCω. - Masahiro Sato; Jacques Garrigue (CoRR, 2020)

A Library for Formalization of Linear Error-Correcting Codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Autom. Reason., 2020)

A trustful monad for axiomatic reasoning with probability and nondeterminism. - Reynald Affeldt; Jacques Garrigue; David Nowak; Takafumi Saikawa (J. Funct. Program., 2021)

An intuitionistic set-theoretical model of fully dependent CC. - Masahiro Sato; Jacques Garrigue (Math. Struct. Comput. Sci., 2023)

Typed Compositional Quantum Computation with Lenses. - Jacques Garrigue; Takafumi Saikawa (ITP, 2024)

QECC: Quantum Computation and Error-Correcting Codes. - Jacques Garrigue; Takafumi Saikawa (DROPS Artifacts, 2024)

An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. - Cheng-Hui Weng; Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (FORTE, 2025)

A practical formalization of monadic equational reasoning in dependent-type theory. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Funct. Program., 2025)