Publications
Draft - Published
- 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.
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.
- 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
2022.10.28