Publications

Draft - Published

Drafts and talks material

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory
Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa. Dec 2023. arXiv:2312.06103 [cs.LO]

Typed compositional quantum computation with lenses
Jacques Garrigue and Takafumi Saikawa. Draft paper, Coq code.

A type-theoretic account of quantum computation
Jacques Garrigue and Takafumi Saikawa, TyDE 2023, Seattle. Slides, Abstract, Coq code.

Environment-friendly monadic equational reasoning for OCaml
Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa, Coq Workshop 2023, Bialystok. Coq WS Slides, TPP Slides, NIER Slides, Abstract, Coq code.

Interpreting OCaml GADTs into Coq
Jacques Garrigue and Takafumi Saikawa. ML Workshop 2022, Ljubljana. Slides, Abstract, ML Code, Coq Code.
TPP 2022, Eiheiji. Slides.

Translation from OCaml to Coq and proof of programs
Kaoru Nakamura, Eito Maeda, Jacques Garrigue, Takafumi Saikawa.
Poster presented at JSSST 2022, Nagoya. Poster (in Japanese)
Poster presented at PPL 2023, Nagoya. Poster (in Japanese)

A Gallina generating backend to check OCaml's type inference correctness
Jacques Garrigue, Takafumi Saikawa.
TYPES 2022, Nantes. Abstract, Slides, Code.
PPL 2022. Poster.
TPP 2021, Kitami. Slides.

Formalizing quantum circuits with MathComp/Ssreflect
Takafumi Saikawa and Jacques Garrigue. TPP 2021, Kitami. Slides.
PPL 2022. Poster
PlanQC 2022. Poster

Formalizing OCaml GADT typing in Coq
Jacques Garrigue and Xuanrui Qi. ML Workshop, Aug 2021. A4 paper, Slides.

Towards a Coq specification for generalized algebraic datatypes in OCaml
Xuanrui Qi and Jacques Garrigue. CoqPL Workshop, Jan 2021. A4 paper.

Tracking injectivity and nominality beyond abstraction
Jacques Garrigue. ML Family Workshop 2020, New York. Abstract.

Proving tree algorithms for succinct data structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. JSSST Annual Meeting 2018, Osaka. Paper, Slides (Japanese), Proofs.

GADTs and exhaustiveness: looking for the impossible
Jacques Garrigue and Jacques Le Normand. ML Family Workshop 2015, Vancouver. Abstract, Slides.

Type-level module aliases: independent and equal
Jacques Garrigue and Leo White. ML Family Workshop 2014, Gothenburg. Abstract, Slides.

Formalization of Error-correcting Codes using SSReflect
Reynald Affeldt and Jacques Garrigue. Coq Workshop 2014, Vienna. Abstract.
Runtime types in OCaml
Jacques Garrigue and Grégoire Henry. OCaml Meeting 2013, Boston. Abstract.

On variance, injectivity, and abstraction
Jacques Garrigue. OCaml Meeting 2013, Boston. Abstract.

Relaxing the Value Restriction, a soundness proof for the OCaml type system in Coq
Thomas Leventis, internship report, September 2012. Coq scripts.

Tracing ambiguity in GADT type inference
Jacques Garrigue and Didier Rémy. ML Workshop 2012, Copenhagen. Abstract and Slides.

Adding GADTs to OCaml: a direct approach
Jacques Garrigue and Jacques Le Normand. ML Workshop 2011, Tokyo. Abstract and Slides.

Simpoulet: an attempt at proving environmental bisimulations in Coq
Jacques Garrigue and Pierre-Marie Pédrot. Presentation at TPP'10, Nagoya. Slides. Proofs.

First-class modules and composable signatures in Objective Caml 3.12
Alain Frisch and Jacques Garrigue. ML Workshop 2010, Baltimore, MD. Abstract. Slides.

Le sous-typage d'OCaml
Draft of 2008-06-13, in French: A4 PDF.
Coq scripts for some of the properties.

Unions de variants polymorphes abstraits
Romain Bardou. Rapport de stage (in French.) September 2006. A4 PDF
(This is a report by a student who did an internship with me, working on unions of private polymorphic variants.)
Also, slides of a talk at INRIA (2007-07-02): A4 PDF.

Published

An Intuitionistic Set-theoretical Model of Fully Dependent CCω.
Masahiro Sato and Jacques Garrigue. Mathematical Structures in Computer Science (2023), 1–32. Author's version, DOI.

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. Journal of Functional Programming, 31:e17, July 2021. Author's version.

Formal Adventures in Convex and Conical Spaces
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. CICM 2020, Bertinoro, Italy. Paper, Slides.

Reasoning with Conditional Probabilities and Joint Distributions in Coq
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Computer Software 37(3)79-95, July 2020. Presented at the JSSST Workshop on Programming and Programming Languages, Hanamaki, March 2019. Journal version, PPL version.

A Library for Formalization of Linear Error-Correcting Codes
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Journal of Automated Reasoning 64(6)1123-1164, January 2020. Author's version, DOI.

Proving tree algorithms for succinct data structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. ITP 2019, Portland, OR. Paper, Slides, Proofs.

Lightweight linearly-typed programming with lenses and monads
Keigo Imai and Jacques Garrigue. Journal of Information Processing 27:431-444, 2019. A4 PDF, DOI.

Examples of Formal Proofs about Data Compression
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. International Symposium on Information Theory and Its Applications (ISITA 2018), Singapore, October 2018. A4 PDF.

Safe Low-level Code Generation in Coq Using Monomorphization and Monadification
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. Journal of Information Processing 26:54-72, 2018. A4 PDF, DOI.

Des unités dans le typeur.
Jacques Garrigue and Dara Ly. In JFLA 2017. A4 PDF.

GADTs and Exhaustiveness: Looking for the Impossible.
Jacques Garrigue and Jacques Le Normand. In Proceeding of the ML Family / OCaml Workshops 2015, EPTCS 241. EPTCS link, A4 PDF.

Formal Verification of the rank Algorithm for Succinct Data Structures.
Akira Tanaka, Reynald Affeldt, and Jacques Garrigue. In 18th International Conference on Formal Engineering Methods (ICFEM 2016), Tokyo, Japan, November 2016, Springer-Verlag LNCS 10009, pages 243-260. A4 PDF, DOI, Code.

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.
Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. In International Symposium on Information Theory and Its Applications (ISITA 2016), Monterey, California, October 2016, pages 537-541. A4 PDF, Scripts.

An Intuitionistic Set-theoretical Model of CCω.
Masahiro Sato and Jacques Garrigue. Journal of Information Processing 24(4):711-720, 2016. JIP link, A4 PDF.

Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory.
Reynald Affeldt and Jacques Garrigue. In 6th Conference on Interactive Theorem Proving (ITP 2015), Nanjing, China, August 2015, Springer-Verlag LNCS 9236, pages 17-33. A4 PDF. © Springer, Springer Link.

A Certified Implementation of ML with Structural Polymorphism and Recursive Types.
Jacques Garrigue. Mathematical Structures in Computer Science, November 2014, pages 1-25. A4 PDF, Publisher PDF.
Abstract and Coq scripts (updated 2019-11-15).

Ambivalent types for principal type inference with GADTs.
Jacques Garrigue and Didier Rémy. In 11th Asian Symposium on Programming Languages and Systems, Melbourne, December 2013. Springer-Verlag LNCS 8301, pages 257-272. Abstract and long version. Author PDF. Slides.

Path resolution for recursive nested modules.
Jacques Garrigue and Keiko Nakata. Higher-Order and Symbolic Computation (2012) 24:207-237.
DOI 10.1007/s10990-012-9083-6. SpringerLink. Author PDF. Coq scripts.

A Syntactic Type System for Recursive Modules.
Hyonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Portland, Oregon, October 2011. Letter PDF.

A Certified Implementation of ML with Structural Polymorphism.
Jacques Garrigue. In 8th Asian Symposium on Programming Languages and Systems, Shanghai, November 2010. Springer-Verlag LNCS 6461, pages 360-375. A4 PDF.
Abstract and Coq scripts.

Path resolution for recursive nested modules is undecidable.
Keiko Nakata and Jacques Garrigue. In 9th International Workshop on Termination, Paris, June 2007. A4 postscript, A4 PDF.

Private rows: abstracting the unnamed.
Jacques Garrigue. In 4th Asian Symposium on Programming Languages and Systems, Sydney, November 2006. Springer-Verlag LNCS 4279. A4 PDF, IFIP 2005 slides (PDF)

Recursive Modules for Programming.
Keiko Nakata and Jacques Garrigue. In 11th ACM SIGPLAN International Conference on Functional Programming, Portland, Oregon, September 2006. Letter PDF

Recursive Object-Oriented Modules.
Keiko Nakata, Akira Ito, and Jacques Garrigue. In 12th International Workshop on Foundations of Object-Oriented Languages, Long Beach, California, January 2005. Letter postscript, Letter PDF

Typing deep pattern-matching in presence of polymorphic variants.
Jacques Garrigue. In JSSST Workshop on Programming and Programming Languages, Gamagori, Japan, March 2004. A4 postscript, A4 PDF

Relaxing the value restriction.
Jacques Garrigue. In International Symposium on Functional and Logic Programming, Nara, April 2004. Springer-Verlag LNCS 2998. (extended version: RIMS Preprint 1444) A4 postscript, A4 PDF

Simple Type Inference for Structural Polymorphism .
Jacques Garrigue. Presented at the 9th Workshop on Foundations of Object-Oriented Languages, Portland, Oregon, January 2002. Revised on 2002/12/11. A4 postscript, Letter postscript, A4 PDF, Letter PDF,

Labeled and optional arguments for Objective Caml.
Jacques Garrigue. In JSSST Workshop on Programming and Programming Languages, Kameoka, Japan, March 2001. Revised on 2000/04/13. A4 PDF, A4 postscript, DVI

Code reuse through polymorphic variants.
Jacques Garrigue. In Workshop on Foundations of Software Engineering. Sasaguri, Japan, November 2000.
Abstract and code samples. A4 postscript A4 PDF

Programming with polymorphic variants.
Jacques Garrigue. In ML Workshop, September 1998. Letter postscript, A4 PDF, Letter PDF

Extending ML with semi-explicit higher order polymorphism.
Jacques Garrigue and Didier Rémy. In Proceedings of the International Symposium on Theoretical Aspects of Computer Software. Sendai, Japan. September 1997. Springer-Verlag LNCS 1281. A4 postscript
Journal version in Information and Computation 155, december 1999, pages 134-171. A4 postscript, Letter PDF

A label-selective lambda-calculus with optional arguments and its compilation method.
Jun P. Furuse and Jacques Garrigue. RIMS Preprint 1041, Research Institute for Mathematical Sciences, Kyoto University, October 1995. Abstract

The transformation calculus.
Jacques Garrigue. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science. Bangalore, India, December 1995. Spring-Verlag LNCS 1026. Abstract

The transformation calculus (revised version).
Jacques Garrigue. RIMS Preprint 1042, Research Institute for Mathematical Sciences, Kyoto University, October 1995. Abstract

Dynamic binding and lexical binding in a transformation calculus.
Jacques Garrigue. In Proc. of the Fuji International Workshop on Functional and Logic Programming. World Scientific, Singapore, 1995. Abstract

Label-selective lambda-calculus: syntax and confluence.
Hassan Aït-Kaci and Jacques Garrigue. Theoretical Computer Science 151 (1995) 353-383. Abstract

Label-Selective Lambda-Calculi and Transformation Calculi.
Jacques Garrigue. PhD thesis, University of Tokyo, Department of Information Science, March 1995. Abstract

The typed polymorphic label-selective lambda-calculus.
Jacques Garrigue and Hassan Aït-Kaci. In Proc. of the 21st ACM Symposium on Principles of Programming Languages, pages 35-47, 1994. Abstract

Transformation calculus and its typing.
Jacques Garrigue. In Proc. of the workshop on Type Theory and its Applications to Computer Systems, pages 34-45. Kyoto University RIMS Lecture Notes 851, July 1993. Abstract

Introducing stateful objects in a transformation calculus.
Jacques Garrigue. In Proc. of the JSSST Workshop on Object-Oriented Computing, Tokyo, March 1993. Iwanami Shoten. Abstract

Label-selective lambda-calculus: Syntax and confluence.
Hassan Aït-Kaci and Jacques Garrigue. In Proc. of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 24-40, Bombay, India, 1993. Springer-Verlag LNCS 761. Abstract
Links to the online papers are included in the abstracts.
JG 2024.03.11