Recent publications of project Cristal

2006

[1] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, Workshop TYPES 2004, volume 3839 of Lecture Notes in Computer Science, pages 66-81. Springer-Verlag, 2006.
[ .pdf ]
[2] Emmanuel Chailloux and Michel Mauny. Programmation fonctionnelle. In Encyclopédie des systèmes d'information. Éditions Vuibert, 2006. To appear.
[3] Alain Frisch. OCaml + XDuce. In Programming Language Technologies for XML (PLAN-X) 2006, January 2006.
[4] Grégoire Henry, Michel Mauny, and Emmanuel Chailloux. Typer la dé-sérialisation sans sérialiser les types. In Journées francophones des langages applicatifs. INRIA, January 2006. Accepted for publication, to appear.
[5] Xavier Leroy. Coinductive big-step operational semantics. In European Symposium on Programming (ESOP'06). Springer-Verlag, 2006. Accepted for publication, to appear.
[ .pdf ]
[6] Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM symposium on Principles of Programming Languages, pages 42-54. ACM Press, 2006.
[ .pdf ]
[7] François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. In 33rd ACM symposium on Principles of Programming Languages, pages 232-244. ACM Press, January 2006.
[ .pdf ]

2005

[1] Serge Abiteboul, Ciarán Bryce, Roberto Di Cosmo, Klaus R. Dittrich, Stéfane Fermigier, Stéphane Laurière, Frédéric Lepied, Xavier Leroy, Tova Milo, Eleonora Panto, Radu Pop, Assaf Sagi, Yotam Shtossel, Florent Villard, and Boris Vrdoljak. Edos: Environment for the development and distribution of open source software. In First International Conference on Open Source Systems (OSS 2005), 2005.
[ .pdf ]
[2] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory. Draft, circulated on the poplmark mailing list, 2005.
[3] Sandrine Blazy and Xavier Leroy. Formal verification of a memory model for C-like imperative languages. In International Conference on Formal Engineering Methods (ICFEM 2005), volume 3785 of Lecture Notes in Computer Science, pages 280-299. Springer-Verlag, 2005.
[ http ]
[4] Daniel Bonniot. Typage modulaire des multi-méthodes. PhD thesis, École des Mines de Paris, November 2005.
[5] Giuseppe Castagna, Dario Colazzo, and Alain Frisch. Error mining for regular expression patterns. In 9th Italian Conference on Theoretical Computer Science, pages 160-172, October 2005.
[6] Giuseppe Castagna and Alain Frisch. A gentle introduction to semantic subtyping. In International Conference on Principles and Practice of Declarative Programming, pages 198-199. ACM Press, July 2005. Abstract of invited lecture.
[7] Zaynah Dargaye. Éléments de preuve pour un compilateur certifié de C. Master's thesis, Université Paris 7, 2005.
[8] David Delahaye, Mathieu Jaume, and Virgile Prevosto. Coq, un outil pour l'enseignement. Technique et Science Informatique, 24(9):1139-1160, 2005.
[9] Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping recursive types modulo associative commutative products. In Seventh International Conference on Typed Lambda Calculi and Applications (TLCA'05), volume 3461 of Lecture Notes in Computer Science, pages 179-193, Nara, Japan, April 2005. Springer Verlag.
[ .pdf ]
[10] Philippe Flajolet and Gérard Huet. Mathématiques et informatique. In J.-C. Yoccoz, editor, Les mathématiques dans le monde contemporain. Rapport sur la science et la technologie n°20, Académie des sciences, 2005.
[11] Tom Hirschowitz and Xavier Leroy. Mixin modules in a call-by-value setting. ACM Transactions on Programming Languages and Systems, 27(5):857-881, 2005.
[ .pdf ]
[12] Haruo Hosoya, Alain Frisch, and Giuseppe Castagna. Parametric polymorphism for XML. In 32nd ACM symposium on Principles of Programming Languages, pages 50-62. ACM Press, January 2005.
[ .ps.gz ]
[13] Gérard Huet. A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger. J. Functional Programming, 15(4):573-614, 2005.
[ .pdf ]
[14] Gérard Huet. Internet challenges for informatics research. Progress in Informatics, 1(2), 2005.
[15] Gérard Huet. The Zen Computational Linguistics Toolkit, Version 2.0, 2005.
[ http ]
[16] Gérard Huet and Benoît Razet. The reactive engine for modular transducers. Submitted for publication, 2005.
[17] Xavier Leroy. A locally nameless solution to the POPLmark challenge. October 2005.
[ http ]
[18] Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, documentation and user's manual - release 3.09. INRIA, October 2005.
[ http ]
[19] François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389-489. MIT Press, 2005.
[20] François Pottier. An overview of Cαml. In ACM Workshop on ML, Electronic Notes in Theoretical Computer Science, pages 27-51, September 2005.
[ .pdf ]
[21] François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, May 2005. To appear.
[ .pdf ]
[22] François Pottier and Yann Régis-Gianas. Towards efficient, typed LR parsers. In ACM Workshop on ML, Electronic Notes in Theoretical Computer Science, pages 149-173, September 2005.
[ .pdf ]
[23] François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. ACM Transactions on Programming Languages and Systems, 27(2), March 2005.
[ .ps.gz ]
[24] Benoît Razet. Automates modulaires. Master's thesis, Université Paris 7, 2005.
[25] Didier Rémy. Simple, partial type-inference for system F based on type-containment. In Proceedings of the tenth International Conference on Functional Programming. ACM Press, September 2005.
[ http | .pdf ]
[26] Didier Rémy and Boris Yakobowski. MLF with graphs. In Proceedings 3rd APPSEM II Worshop, sept 2005.
[27] Vincent Simonet and François Pottier. Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA, January 2005.
[ .html ]

2004

[1] Vincent Balat, Roberto Di Cosmo, and Marcelo Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In 31st ACM symposium on Principles of Programming Languages, pages 64-76. ACM Press, January 2004.
[2] Richard Bonichon. TaMeD: A tableau method for deduction modulo. In Automated Reasoning: Second International Joint Conference, IJCAR 2004, volume 3097 of Lecture Notes in Computer Science, pages 445-459. Springer-Verlag, 2004.
[3] François Clément, Roberto Di Cosmo, Zheng Li, Vincent Martin, Arnaud Vodicka, and Pierre Weis. Parallel programming with the OCamlP3L system: Applications to numerical code coupling. Research report 5131, INRIA, 2004.
[ .html ]
[4] Alexandre Frey. Approche algébrique du typage d'un langage à la ML avec objets, sous-typage et multi-méthodes. PhD thesis, École des Mines de Paris, June 2004.
[5] Alain Frisch. Regular tree language recognition with static information. In 3rd IFIP International Conference on Theoretical Computer Science. Kluwer Academic Publishers, August 2004.
[6] Alain Frisch. Théorie, conception et réalisation d'un langage de programmation fonctionnel adapté à XML. PhD thesis, University Paris 7, December 2004.
[7] Alain Frisch and Luca Cardelli. Greedy regular expression matching. In 31st International Colloquium on Automata, Languages and Programming, pages 618-629. Springer-Verlag, July 2004.
[8] Nadji Gauthier and François Pottier. Numbering matters: First-order canonical forms for second-order recursive types. In Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP'04), pages 150-161. ACM Press, September 2004.
[ .pdf ]
[9] David Haguenauer. Pré-compilation d'un sous-ensemble du langage C. Master's dissertation (mémoire de stage de DEA), Université Paris 6, September 2004.
[10] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Call-by-value mixin modules: Reduction semantics, side effects, types. In European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 64-78. Springer-Verlag, 2004.
[ .ps.gz ]
[11] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Compilation of extended recursion in call-by-value functional languages. submitted and resubmitted after revision to Higher-Order and Symbolic Computation, November 2004.
[12] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Extended recursive definitions in call-by-value languages, with applications to mixin modules and recursive modules. In Electronic proceedings of the second APPSEM II Workshop, April 2004.
[13] Gérard Huet. Automata mista. In N. Dershowitz, editor, Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772 of Lecture Notes in Computer Science, pages 359-372. Springer-Verlag, 2004.
[ .pdf ]
[14] Gérard Huet. Design of a lexical database for sanskrit. In Workshop on Enhancing and Using Electronic Dictionaries, COLING 2004. International Conference on Computational Linguistics, 2004.
[ .pdf ]
[15] Gérard Huet. Lexicon-directed segmentation and tagging of Sanskrit. In XIIth World Sanskrit Conference, Linguistics volume. Motilal Banarsidass, Delhi, 2004.
[16] Didier Le Botlan. MLF: Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, École Polytechnique, May 2004.
[ .html ]
[17] François Pottier. Types et contraintes. Mémoire d'habilitation à diriger des recherches, Université Paris 7, December 2004.
[ .pdf ]
[18] François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization. In 31st ACM symposium on Principles of Programming Languages, pages 89-98. ACM Press, January 2004.
[ .pdf ]
[19] Vincent Simonet. Inférence de flots d'information pour ML: formalisation et implantation. PhD thesis, Université Paris 7, March 2004.
[ .pdf ]
[20] Basile Starynkevitch. OCamlJIT: a faster just-in-time OCaml implementation. In First MetaOCaml Workshop. ACM Press, 2004.
[ .ps ]
[21] J. B. Wells and Boris Yakobowski. Graph-based proof counting and enumeration with applications for program fragment synthesis. In Sandro Etalle, editor, International Symposium on Logic-based Program Synthesis and Transformation 2004 (LOPSTR 2004), volume 3049 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
[ .pdf ]
[22] Boris Yakobowski. Étude sémantique d'un langage intermédiaire de type static single assignment. Master's dissertation (mémoire de stage de DEA), ENS Cachan, September 2004.
[ .pdf ]

2003

[1] Daniel Bonniot. Using kinds to type partially-polymorphic methods. Electronic Notes in Theoretical Computer Science, 75, 2003.
[2] Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. Implementing multi-stage languages using ASTs, gensym, and reflection. In Generative Programming and Component Engineering (GPCE'03), 2003.
[ .pdf ]
[3] F. Clément, V. Martin, A. Vodicka, R. Di Cosmo, and P. Weis. Domain decomposition for flow simulation around a waste disposal site: direct computation versus code coupling using OCamlP3l. In International Conference on Supercomputing in Nuclear Applications (SNA'2003), September 2003.
[4] Roberto Di Cosmo. Legal tools to protect software: Choosing the right one. Upgrade, 4(3):21-23, June 2003.
[ .pdf ]
[5] Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonovski. Proof nets and explicit substitutions. Mathematical Structures in Computer Science, 13(3):409-450, 2003.
[6] Roberto Di Cosmo and Susanna Pelagatti. A calculus for dense array distributions. Parallel Processing Letters, 3(13), 2003.
[7] Jean-Christophe Filliâtre and François Pottier. Producing all ideals of a forest, functionally. Journal of Functional Programming, 13(5):945-956, September 2003.
[ .ps.gz ]
[8] Jun Furuse. Extensional polymorphism by flow graph dispatching. In Atsushi Ohori, editor, Programming Languages and Systems, first Asian Symposium, APLAS 2003, number 2895 in Lecture Notes in Computer Science, pages 376-393. Springer-Verlag, November 2003.
[ .ps.gz ]
[9] Benjamin Grégoire. Compilation de termes de preuves. PhD thesis, University Paris 7, December 2003.
[10] Tom Hirschowitz. Modules mixins, modules et récursion étendue en appel par valeur. PhD thesis, University Paris 7, December 2003.
[11] Tom Hirschowitz. Rigid mixin modules. Technical Report RR2003-46, ENS Lyon, 2003.
[ .ps.gz ]
[12] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Compilation of extended recursion in call-by-value functional languages. In International Conference on Principles and Practice of Declarative Programming, pages 160-171. ACM Press, 2003.
[ .pdf ]
[13] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. On the implementation of recursion in call-by-value functional languages. Technical Report 4728, INRIA, 2003.
[ .html ]
[14] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. A reduction semantics for call-by-value mixin modules. Technical Report 4682, INRIA, 2003.
[ .html ]
[15] Gérard Huet. Linear contexts and the sharing functor: Techniques for symbolic computation. In Fairouz Kamareddine, editor, Thirty Five Years of Automating Mathematics. Kluwer, 2003.
[ .pdf ]
[16] Gérard Huet. Towards computational processing of Sanskrit. In International Conference on Natural Language Processing (ICON), 2003.
[17] Gérard Huet. Zen and the art of symbolic computing: Light and fast applicative algorithms for computational linguistics. In Practical Aspects of Declarative Languages (PADL) symposium, 2003.
[ .pdf ]
[18] Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of System F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 27-38. ACM Press, August 2003.
[ .pdf ]
[19] Xavier Leroy. Computer security from a programming language and static analysis perspective. In P. Degano, editor, Programming Languages and Systems: 12th European Symposium on Programming, ESOP 2003, volume 2618 of Lecture Notes in Computer Science, pages 1-9. Springer-Verlag, 2003. Extended abstract of invited lecture.
[20] Xavier Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, 30(3-4):235-269, 2003.
[ .pdf ]
[21] François Pottier. A constraint-based presentation and generalization of rows. In Eighteenth Annual IEEE Symposium on Logic In Computer Science (LICS'03), pages 331-340, Ottawa, Canada, June 2003.
[ .ps.gz ]
[22] François Pottier and Vincent Simonet. Information flow inference for ML. ACM Transactions on Programming Languages and Systems, 25(1):117-158, January 2003.
[ .ps.gz ]
[23] Vincent Simonet. An extension of HM(X) with bounded existential and universal data-types. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), pages 39-50, Uppsala, Sweden, August 2003. ACM Press.
[24] Vincent Simonet. Flow Caml in a nutshell. In Graham Hutton, editor, Proceedings of the first APPSEM-II workshop, pages 152-165, Nottingham, United Kingdom, March 2003.
[25] Vincent Simonet. The Flow Caml System: documentation and user's manual. Technical Report 0282, INRIA, July 2003.
[26] Vincent Simonet. Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. In Atsushi Ohori, editor, Programming Languages and Systems, first Asian Symposium, APLAS 2003, number 2895 in Lecture Notes in Computer Science, pages 283-302. Springer-Verlag, November 2003.

2002

[1] Daniel Bonniot. Type-checking multi-methods in ML (a modular approach). In Ninth International Workshop on Foundations of Object-Oriented Languages, FOOL 9, 2002.
[2] Daniel Bonniot. Using kinds to type partially polymorphic multi-methods. In Workshop on Types in Programming (TIP'02), 2002.
[3] Pascal Cuoq. Ajout de synchronisme dans les langages fonctionnels fortement typés. PhD thesis, University Paris 6, October 2002.
[4] Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In Symposium on Logic in Computer Science (LICS 2002). IEEE, 2002.
[5] Jun Furuse. Extensional polymorphism: theory and applications. PhD thesis, University Paris 7, December 2002.
[6] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In International Conference on Functional Programming 2002, pages 235-246. ACM Press, 2002.
[ .pdf ]
[7] Robert Harley. Algorithmique avancée sur les courbes elliptiques. PhD thesis, University Paris 7, December 2002.
[8] Tom Hirschowitz and Xavier Leroy. Mixin modules in a call-by-value setting. In D. Le Métayer, editor, Programming Languages and Systems - ESOP'2002, volume 2305 of Lecture Notes in Computer Science, pages 6-20. Springer-Verlag, 2002.
[ .pdf ]
[9] Gérard Huet. Data structures for trees and tree contexts, and a uniform sharing functor, as design issues for symbolic computation systems. In Workshop on Thirty Five Years of Automath, 2002.
[10] Gérard Huet. Higher order unification 30 years later. In V. Carreño, C. Muñoz, and S. Tahar, editors, Proceedings, 15th International Conference TPHOL, volume 2410 of Lecture Notes in Computer Science, pages 3-12. Springer-Verlag, 2002.
[11] Gérard Huet. Sri Yantra geometry. Theoretical Computer Science, 281:609-628, 2002.
[12] Gérard Huet. The Zen computational linguistics toolkit. In ESSLLI 2002 Lectures, 2002.
[13] Xavier Leroy. Bytecode verification for Java smart card. Software Practice & Experience, 32:319-340, 2002.
[ .pdf ]
[14] François Pottier. A simple view of type-secure information flow in the π-calculus. In Proceedings of the 15th IEEE Computer Security Foundations Workshop, pages 320-330, June 2002.
[15] François Pottier and Vincent Simonet. Information flow inference for ML. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02), pages 319-330, January 2002.
[16] Didier Rémy. Using, Understanding, and Unraveling the OCaml Language. In Gilles Barthe, editor, Applied Semantics. Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 413-537. Springer-Verlag, 2002.
[17] Vincent Simonet. Fine-grained information flow analysis for a λ-calculus with sum types. In Proceedings of the 15th IEEE Computer Security Foundations Workshop, pages 223-237, June 2002.
[18] Christian Skalka and François Pottier. Syntactic type soundness for HM(X). In Proceedings of the 2002 Workshop on Types in Programming (TIP'02), June 2002.

2001

[1] Sylvain Conchon and François Pottier. JOIN(X): Constraint-based type inference for the join-calculus. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in Computer Science, pages 221-236. Springer-Verlag, 2001.
[2] Pascal Cuoq and Marc Pouzet. Modular causality in a synchronous stream language. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in Computer Science, pages 30-45. Springer-Verlag, 2001.
[3] Daniel de Rauglaudre. Camlp4 - Reference Manual version 3.03. INRIA, November 2001.
[4] Daniel de Rauglaudre. Camlp4 - Tutorial version 3.03. INRIA, November 2001.
[5] Mireille Fouquet, Pierrick Gaudry, and Robert Harley. Finding secure curves with the Satoh-FGH algorithm and an early-abort strategy. In Birgit Pfitzmann, editor, Advances in Cryptology - Eurocrypt 2001, volume 2045 of Lecture Notes in Computer Science, pages 14-29. Springer-Verlag, May 2001.
[6] Maxence Guesdon. OCamldoc documentation and user's manual - release 3.03. INRIA, December 2001.
[7] Gérard Huet. Computational tools for sanskrit. In Workshop on Computational Linguistics in South Asian Languages, 2001.
[8] Gérard Huet. From an informal textual lexicon to a well-structured lexical database: An experiment in data reverse engineering. In IEEE Working Conference on Reverse Engineering (WCRE'2001), pages 127-135, 2001.
[9] Xavier Leroy. Java bytecode verification: an overview. In Computer Aided Verification, CAV 2001, volume 2102 of Lecture Notes in Computer Science, pages 265-285. Springer-Verlag, 2001.
[10] Xavier Leroy. On-card bytecode verification for Java card. In I. Attali and T. Jensen, editors, Smart card programming and security, proceedings E-Smart 2001, volume 2140 of Lecture Notes in Computer Science, pages 150-164. Springer-Verlag, 2001.
[11] François Pottier. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA, March 2001.
[12] François Pottier. Simplifying subtyping constraints: a theory. Information & Computation, 170(2):153-183, 2001.
[13] François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. In David Sands, editor, Proceedings of the 10th European Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in Computer Science, pages 30-45. Springer-Verlag, April 2001.
[14] Jérôme Vouillon. An object calculus with views. In Proceedings 28th ACM symposium Principles of Programming Languages (POPL'01). ACM Press, June 2001.

2000

[1] Emmanuel Chailloux, Pascal Manoury, and Bruno Pagano. Développement d'applications avec Objective Caml. O'Reilly, 2000.
[2] Mireille Fouquet, Pierrick Gaudry, and Robert Harley. An extension of Satoh's algorithm and its implementation. Journal of the Ramanujan Mathematical Society, 15:281-318, 2000.
[3] Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Inheritance in the join calculus. In Foundations of Software Technology and Theoretical Computer Science - FSTTCS 2000, volume 1974 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
[4] Jun Furuse and Pierre Weis. Entrées-sorties de valeurs en Caml. In Journées francophones des langages applicatifs (JFLA 2000). INRIA, January 2000.
[5] Tom Hirschowitz. Modules mixins : typage et implantation. DEA dissertation (master's thesis), University Paris 7, 2000.
[6] Gérard Huet. Structure of a sanskrit dictionary. In 11th International Sanskrit Conference, 2000.
[7] Richard Kieburtz. Coalgebraic techniques for reactive functional programming. In Journées francophones des langages applicatifs. INRIA, 2000. Invited talk.
[8] Xavier Leroy. A modular module system. Journal of Functional Programming, 10(3):269-303, 2000.
[ .ps.gz ]
[9] François Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems, 22(2):340-377, 2000.
[ .ps.gz ]
[10] François Pottier. A 3-part type inference engine. In Proceedings of the 2000 European Symposium on Programming (ESOP'00), volume 1782 of Lecture Notes in Computer Science, pages 320-335. Springer-Verlag, March 2000.
[11] François Pottier. wallace: an efficient implementation of type inference with subtyping, February 2000.
[12] François Pottier. A versatile constraint-based type inference system. Nordic Journal of Computing, 7(4):312-347, 2000.
[13] François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pages 46-57, 2000.
[14] Didier Rémy. Re-exploring multiple inheritance. In Seventh International Workshop on Foundations of Object-Oriented Languages (FOOL 7), 2000. Invited talk.
[15] Jérôme Vouillon. Conception et réalisation d'une extension du langage ML avec des objets. PhD thesis, University Paris 7, 2000.
[16] Yong Xiao, Zena Ariola, and Michel Mauny. From syntactic theories to interpreters: A specification language and its compilation. In Nachum Derschowitz and Claude Kirchner, editors, First International Workshop on Rule-Based Programming (RULE 2000), September 2000.

1999

[1] Jacques Garrigue and Didier Rémy. Extending ML with semi-explicit higher-order polymorphism. Information & Computation, 155(1/2):134-169, 1999.
[2] Benjamin Grégoire. Certification en coq de propriétés de sécurité issues du typage. DEA dissertation (master's thesis), University Paris 7, 1999.
[3] Xavier Leroy and François Rouaix. Security properties of typed applets. In J. Vitek and C. Jensen, editors, Secure Internet Programming - Security issues for Mobile and Distributed Objects, volume 1603 of Lecture Notes in Computer Science, pages 147-182. Springer-Verlag, 1999.
[ .ps.gz ]
[4] François Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. In 26th symposium Principles of Programming Languages, pages 276-290. ACM Press, 1999.
[5] François Pessaux. Détection statique d'exceptions non rattrapées en Objective Caml. PhD thesis, University Paris 6, 1999.
[6] Pierre Weis and Xavier Leroy. Le langage Caml. Dunod, second edition edition, July 1999.