Publications

Drafts and talks material

A Certified Interpreter for ML with Structural Polymorphism

Extended abstract. A4 PDF.

Coq scripts for the proofs, allowing extraction of a certified algorithm.
(Updated 2009-08-29)

Type inference for structural polymorphism

Slides from a presentation at TPP08 (Sendai, 2008-11-26): A4 PDF.

Coq scripts for the proofs, allowing extraction of a certified algorithm.

Proving OCaml's type system?

Slides from a presentation at INRIA (Rocquencourt, 2008-06-13): A4 PDF.

Coq scripts for structural polymorphism extended with Kind GC (updated 2008-06-20). See also material below.

Le sous-typage d'OCaml

Draft of 2008-06-13, in French: A4 PDF.
Coq scripts for some of the properties.

A formal proof of soundness for structural polymorphism

Coq scripts proving the soundness described in Simple type inference for structural polymorphism, based on Arthur Charguéraud et al. Engineering Formal Metatheory.

Slides from a presentation at TPP07 (Tsukuba, 2007-11-22): A4 PDF.

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

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

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 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

Programming with polymorphic variants..

Jacques Garrigue. In ML Workshop, September 1998. Letter postscript

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

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