Sites Inria

Version française

CRISTAL Research team

CRISTAL team publications

2008

Journal articles

titre
The Multi-Dimensional Refinement Indicators Algorithm for Optimal Parameterization
auteur
Hend Ben Ameur, François Clément, Pierre Weis, Guy Chavent
article
Journal of Inverse and Ill-posed Problems, De Gruyter, 2008, 16 (2), pp.107-126. <10.1515/JIIP.2008.008>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00079668/file/rapport.pdf BibTex

2007

Journal articles

titre
Typer la désérialisation sans sérialiser les types
auteur
Grégoire Henry, Michel Mauny, Emmanuel Chailloux
article
Technique et Science Informatiques, Hermès-Lavoisier, 2007, 26 (9), pp.1067-1090
Accès au bibtex
BibTex

Conference papers

titre
On the implementation of construction functions for non-free concrete data types
auteur
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
article
16th European Symposium on Programming - ESOP'07, Mar 2007, Braga, Portugal. Springer, 4421, pp.95-109, 2007, Lecture Notes in Computer Science. <10.1007/978-3-540-71316-6_8>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00095110/file/main.pdf BibTex

Reports

titre
Separation Logic for Small-step Cminor (extended version)
auteur
Andrew W. Appel, Sandrine Blazy
article
[Research Report] RR-6138, INRIA. 2007, pp.34
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00134699/file/sequential-rr.pdf BibTex

2006

Conference papers

titre
Managing the Complexity of Large Free and Open Source Package-Based Software Distributions
auteur
Fabio Mancinelli, Jaap Boender, Roberto Di Cosmo, Jérôme Vouillon, Berke Durak, Xavier Leroy, Ralf Treinen
article
21st IEEE/ACM International Conference on Automated Software Engineering, Sep 2006, Tokyo, Japan. ACM, pp.199-208, 2006, <10.1109/ASE.2006.49>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00149566/file/ase.pdf BibTex
titre
Formal Verification of a C Compiler Front-end
auteur
Sandrine Blazy, Zaynah Dargaye, Xavier Leroy
article
Jayadev Misra, Tobias Nipkow and Emil Sekerinski. FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. Springer-Verlag, 4085 (4085), pp.460-475, 2006, Lecture Notes in Computer Science; FM 2006: Formal Methods. <10.1007/11813040_31>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00106401/file/fm06Blazy.pdf BibTex
titre
News from the EDOS project: improving the maintenance of free software distributions.
auteur
Roberto Di Cosmo, Jaap Boender, Berke Durak, Xavier Leroy, Fabio Mancinelli, Mario Morgado, David Pinheiro, Ralf Treinen, Paulo Trezentos, Jérôme Vouillon
article
Olivier Berger. Apr 2006, Porto Alegre, Brazil. Brazilian Computer Society, pp.199-207, 2006
Accès au bibtex
BibTex
titre
Maintaining large software distributions: new challenges from the FOSS era.
auteur
Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, Jérôme Vouillon
article
Apr 2006, Vienna, Austria. EASST, pp.7-20, 2006, EASST Newsletter, volume 12
Accès au bibtex
BibTex
titre
Towards efficient, typed LR parsers.
auteur
François Pottier, Yann Regis-Gianas
article
ACM Workshop on ML, Mar 2006, Portland, Oregon, United States. 2006
Accès au bibtex
BibTex
titre
Stratified type inference for generalized algebraic data types
auteur
François Pottier, Yann Regis-Gianas
article
POPL'06 - Proceedings of the 33rd ACM Symposium on Principles of Programming Languages, Jan 2006, Charleston, South Carolina, United States. pp.232--244, 2006, <http://dl.acm.org/citation.cfm?id=1111037.1111058&coll=DL&dl=ACM&CFID=56655396&CFTOKEN=73618070>
Accès au bibtex
BibTex
titre
Typer la dé-sérialisation sans sérialiser les types
auteur
Grégoire Henry, Michel Mauny, Emmanuel Chailloux
article
Jan 2006, Pauillac, France. INRIA, pp.133-146, 2006
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00145454/file/safe_unmarshalling.pdf BibTex

2005

Conference papers

titre
Formal verification of a memory model for C-like imperative languages
auteur
Sandrine Blazy, Xavier Leroy
article
Kung-Kiu Lau, Richard Banach. ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. Springer, 3785 (3785), pp.280-299, 2005, Lecture Notes in Computer Science; Formal Methods and Software Engineering. <10.1007/11576280>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00077921/file/icfem05Blazy.pdf BibTex
titre
Simple, partial type-inference for System F based on type-containment
auteur
Didier Rémy
article
Proceedings of the tenth International Conference on Functional Programming, Sep 2005, Tallinn, Estonia, 2005
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000938/file/icfp.pdf BibTex
titre
Skeletal parallel programming with OCamlP3L 2.0
auteur
Roberto Di Cosmo, Zheng Li, Susanna Pelagatti, Pierre Weis
article
Proceedings of Third International Workshop on High-level Parallel Programming and Applications (HLPP 2005), Jul 2005, Warwick, United Kingdom. 2005
Accès au bibtex
BibTex
titre
Subtyping Recursive Types Modulo Associative Commutative Products
auteur
Roberto Di Cosmo, Didier Rémy, François Pottier
article
7th International Conference, TLCA 2005, Mar 2005, Nara, Japan. Springer Berlin / Heidelberg, pp.179-193, 2005, Lecture Notes in Computer Science. <10.1007/11417170_14>
Accès au bibtex
BibTex

Reports

titre
Automates modulaires
auteur
Benoit Razet
article
[Rapport de recherche] RR-5788, INRIA. 2005, pp.43
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070233/file/RR-5788.pdf BibTex
titre
Constraint-Based Type Inference for Guarded Algebraic Data Types
auteur
Vincent Simonet, François Pottier
article
[Research Report] RR-5462, INRIA. 2005, pp.65
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070544/file/RR-5462.pdf BibTex

2004

Reports

titre
Parallel Programming with the System Applications to Numerical Code Coupling
auteur
François Clément, Roberto Di cosmo, Zheng Li, Vincent Martin, Arnaud Vodicka, Pierre Weis
article
[Research Report] RR-5131, INRIA. 2004
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071452/file/RR-5131.pdf BibTex

Theses

titre
MLF: An extension of ML with first-class polymorphism and implicit instantiation
auteur
Didier Le Botlan
article
Other [cs.OH]. Ecole Polytechnique X, 2004. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-00007132/file/tel-00007132.pdf BibTex

2003

Journal articles

titre
Java bytecode verification: algorithms and formalizations
auteur
Xavier Leroy
article
Journal of Automated Reasoning, Springer Verlag, 2003, 30 (3-4), pp.235--269. <10.1023/A:1025055424017>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499939/file/bytecode-verification-JAR.pdf BibTex

Conference papers

titre
Computer Security from a Programming Language and Static Analysis Perspective
auteur
Xavier Leroy
article
ESOP 2003: Programming Languages and Systems, 12th European Symposium on Programming, Apr 2003, Warsaw, Poland. pp.1 - 9, 2003, <10.1007/3-540-36575-3_1>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499938/file/language-security-etaps03.pdf BibTex
titre
Compilation of extended recursion in call-by-value functional languages
auteur
Tom Hirschowitz, Xavier Leroy, J. B. Wells
article
PPDP '03, 2003, Uppsala, Sweden. ACM, pp.160--171, 2003, <10.1145/888251.888267>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310121/file/compil-recursion.pdf BibTex

Reports

titre
The Flow Caml System: Documentation and user's manual
auteur
Vincent Simonet
article
RT-0282, INRIA. 2003, pp.155
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069896/file/RT-0282.pdf BibTex
titre
Couplage de codes numériques, parallélisme et langages de haut niveau
auteur
François Clément, Arnaud Vodicka, Roberto Di cosmo, Pierre Weis
article
[Rapport de recherche] RR-4825, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071761/file/RR-4825.pdf BibTex
titre
On the implementation of recursion in call-by-value functional languages
auteur
Tom Hirschowitz, Xavier Leroy, J. B. Wells
article
[Research Report] RR-4728, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071858/file/RR-4728.pdf BibTex

2002

Journal articles

titre
Bytecode verification on Java smart cards
auteur
Xavier Leroy
article
Software: Practice and Experience, Wiley, 2002, 32 (4), pp.319-340. <10.1002/spe.438>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499944/file/oncard-verifier-spe.pdf BibTex

Conference papers

titre
A Compiled Implementation of Strong Reduction
auteur
Benjamin Grégoire, Xavier Leroy
article
ICFP '02: seventh ACM SIGPLAN international conference on Functional programming , Oct 2002, Pittsburgh, United States. ACM, pp.235-246, <10.1145/581478.581501>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499941/file/strong-reduction.pdf BibTex

Reports

titre
A reduction semantics for call-by-value mixin modules
auteur
Tom Hirschowitz, Xavier Leroy, Joe B. Wells
article
[Research Report] RR-4682, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071903/file/RR-4682.pdf BibTex

2001

Conference papers

titre
On-card Bytecode Verification for Java Card
auteur
Xavier Leroy
article
Isabelle Attali; Thomas Jensen. Smart card programming and security, proceedings E-Smart 2001, Sep 2001, Cannes, France. Springer, 2149, pp.150-164, LNCS. <10.1007/3-540-45418-7_13>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499956/file/oncard-verifier-esmart.pdf BibTex
titre
Java bytecode verification: an overview
auteur
Xavier Leroy
article
Gérard Berry; Hubert Comon; Alain Finkel. Computer Aided Verification, CAV 2001, Jul 2001, Paris, France. Springer, 2102, pp.265-285, LNCS. <10.1007/3-540-44585-4_26>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499955/file/survey-bytecode-verification.pdf BibTex
titre
JOIN(X): Constraint-Based Type Inference for the Join-Calculus
auteur
Sylvain Conchon, François Pottier
article
David Sands. Proceedings of the 10th European Symposium on Programming (ESOP'01), Apr 2001, Genova, Springer Verlag, 2028, pp.221--236, 2001, Lecture notes in computer science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000029/file/conchon-fpottier-esop01.pdf BibTex
titre
Finding secure curves with the Satoh-FGH algorithm and an early-abort strategy
auteur
Mireille Fouquet, Pierrick Gaudry, Robert Harley
article
Birgit Pfitzman. Eurocrypt, 2001, Innsbruck, Austria. Springer Verlag, 2045, pp.14-29, 2000, LNCS; Advances in Cryptology - EUROCRYPT 2001. <10.1007/3-540-44987-6_2>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00514426/file/euro01.pdf BibTex

Reports

titre
A Semi-Syntactic Soundness Proof for HM(X)
auteur
François Pottier
article
[Research Report] RR-4150, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072475/file/RR-4150.pdf BibTex

2000

Journal articles

titre
An extension of Satoh's algorithm and its implementation
auteur
Mireille Fouquet, Pierrick Gaudry, Robert Harley
article
Journal of the Ramanujan Mathematical Society, Ramanujan Mathematical Society, 2000, 15, pp.281-318
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00512791/file/satoh.pdf BibTex
titre
Type-based analysis of uncaught exceptions
auteur
Xavier Leroy, François Pessaux
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2000, 22 (2), pp.340-377. <10.1145/349214.349230>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499948/file/exceptions-toplas.pdf BibTex
titre
A modular module system
auteur
Xavier Leroy
article
Journal of Functional Programming, Cambridge University Press (CUP), 2000, 10 (3), pp.269-303. <10.1017/S0956796800003683>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499946/file/modular-modules-jfp.pdf BibTex

Conference papers

titre
Counting points on hyperelliptic curves over finite fields
auteur
Pierrick Gaudry, Robert Harley
article
Wieb Bosma. ANTS-IV, 2000, Leiden, Netherlands. Springer Verlag, 1838, pp.313-332, 2000, LNCS; Algorithmic Number Theory. <10.1007/10722028_18>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00512403/file/antsIV.pdf BibTex

1999

Conference papers

titre
Type-based analysis of uncaught exceptions
auteur
François Pessaux, Xavier Leroy
article
POPL 1999: 26th symposium Principles of Programming Languages, Jan 1999, San Antonio, United States. ACM, pp.276 - 290, 1999, <10.1145/292540.292565>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499959/file/exceptions-popl.pdf BibTex

Book sections

titre
Security properties of typed applets
auteur
Xavier Leroy, François Rouaix
article
Jan Vitek; Christian D. Jensen Secure Internet Programming - Security issues for Mobile and Distributed Objects, 1603, Springer, pp.147-182, 1999, LNCS, 978-3-540-66130-6. <10.1007/3-540-48749-2_7>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499957/file/sip-typed-applets.pdf BibTex

1998

Conference papers

titre
Parallel Functional Programming with Skeletons: the OCamlP3L experiment
auteur
Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, Susanna Pelagatti
article
ACM Workshop on ML and its applications, Sep 1998, Baltimore, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499962/file/ocamlp3l-mlws.pdf BibTex
titre
An overview of Types in Compilation
auteur
Xavier Leroy
article
TIC 1998: workshop Types in Compilation, Mar 1998, Kyoto, Japan. Springer, 1473, pp.1-8, LNCS. <10.1007/BFb0055509>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499960/file/intro-tic98.pdf BibTex
titre
Security properties of typed applets
auteur
Xavier Leroy, François Rouaix
article
POPL 1998: 25th symposium Principles of Programming Languages, Jan 1998, San Diego, United States. ACM, pp.391-403, <10.1145/268946.268979>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499963/file/typed-applets.pdf BibTex

Reports

titre
Type Inference in the Presence of Subtyping: from Theory to Practice
auteur
François Pottier
article
[Research Report] RR-3483, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073205/file/RR-3483.pdf BibTex
titre
Type-Based Analysis of Uncaught Exceptions
auteur
Xavier Leroy, François Pessaux
article
[Research Report] RR-3541, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073144/file/RR-3541.pdf BibTex

1997

Conference papers

titre
Application of formal methods to the development of a software maintenance tool
auteur
Sandrine Blazy, Philippe Facon
article
IEEE CS Press. ASE'97: The 12th IEEE Conference on Automated Software Engineering., Nov 1997, Lake Tahoe, Nevada, USA, pp.162-171, 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00078882/file/BlazyASE97.pdf BibTex
titre
The effectiveness of type-based unboxing
auteur
Xavier Leroy
article
TIC 1997: Workshop Types in Compilation, Jun 1997, Amsterdam, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499964/file/unboxing-tic97.pdf BibTex

Reports

titre
On the Finiteness of Resources in Distributed Computing
auteur
Luc Moreau, Christian Queinnec
article
[Research Report] RR-3147, INRIA. 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073542/file/RR-3147.pdf BibTex

1996

Journal articles

titre
A syntactic theory of type generativity and sharing
auteur
Xavier Leroy
article
Journal of Functional Programming, Cambridge University Press (CUP), 1996, 6 (5), pp.667 - 698. <10.1017/S0956796800001933>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499965/file/syntactic-generativity.pdf BibTex

Conference papers

titre
An automatic interprocedural analysis for the understanding of scientific application programs
auteur
Sandrine Blazy, Philippe Facon
article
Springer Verlag. Dagstuhl seminar on partial evaluation, Feb 1996, Saarbrucken, Germany. 1110, pp.1-16, Lecture Notes in Computer Science; Partial evaluation. <10.1007/3-540-61580-6>
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165927/file/fulltext.pdf BibTex

Reports

titre
A New Presentation of the Intersection Type Discipline through Principal Typings of Normal Forms
auteur
Emilie Sayag, Michel Mauny
article
[Research Report] RR-2998, INRIA. 1996
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073698/file/RR-2998.pdf BibTex
titre
A Modular Module System
auteur
Xavier Leroy
article
[Research Report] RR-2866, INRIA. 1996
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073825/file/RR-2866.pdf BibTex

1995

Conference papers

titre
Applicative functors and fully transparent higher-order modules
auteur
Xavier Leroy
article
POPL 1995: 22nd symposium Principles of Programming Languages, Jan 1995, San Francisco, United States. ACM, pp.142 - 153, 1995, <10.1145/199448.199476>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499966/file/applicative-functors.pdf BibTex

Reports

titre
Une analyse syntaxique d'ASN.1 : 1990 en Caml Light
auteur
Christian Rinderknecht
article
RT-0171, INRIA. 1995, pp.228
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069999/file/RT-0171.pdf BibTex
titre
Implémentation d'un système de modules évolué en Caml-Light
auteur
François Pottier
article
[Rapport de recherche] RR-2449, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074226/file/RR-2449.pdf BibTex
titre
A syntactic theory of type generativity and sharing
auteur
Xavier Leroy
article
[Research Report] RR-2545, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074133/file/RR-2545.pdf BibTex
titre
Le système Caml Special Light: modules et compilation efficace en Caml
auteur
Xavier Leroy
article
[Rapport de recherche] RR-2721, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073972/file/RR-2721.pdf BibTex

1994

Conference papers

titre
Llamado de procedimientos a distancia y abstracción de tipos
auteur
Maria-Virginia Aponte, Xavier Leroy
article
20th CLEI PANEL latino-american computer science conference, Aug 1994, Mexico, México. pp.1281-1292
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499967/file/rpc-abstract-types.pdf BibTex

Reports

titre
1+1=1 : an optimizing Caml compiler
auteur
Manuel Serrano, Pierre Weis
article
[Research Report] RR-2301, INRIA. 1994
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074372/file/RR-2301.pdf BibTex
titre
An Implementation of Caml-Light with existential types
auteur
Michel Mauny, Francois Pottier
article
[Research Report] RR-2183, INRIA. 1994
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074488/file/RR-2183.pdf BibTex

1993

Journal articles

titre
Dynamics in ML
auteur
Xavier Leroy, Michel Mauny
article
Journal of Functional Programming, Cambridge University Press (CUP), 1993, 3 (4), pp.431-463. <10.1017/S0956796800000848>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499972/file/dynamics-in-ML.pdf BibTex

Conference papers

titre
Polymorphism by name for references and continuations
auteur
Xavier Leroy
article
POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. ACM, pp.220-231, 1993, <10.1145/158511.158632>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499970/file/polymorphism-by-name.pdf BibTex
titre
A concurrent, generational garbage collector for a multithreaded implementation of ML
auteur
Damien Doligez, Xavier Leroy
article
POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. pp.113-123, 1993, <10.1145/158511.158611>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499969/file/concurrent-gc.pdf BibTex

Reports

titre
Programmation du systeme Unix en Caml Light
auteur
Xavier Leroy
article
RT-0147, INRIA. 1993, pp.91
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070021/file/RT-0147.pdf BibTex

1992

Reports

titre
The CAML numbers reference manual
auteur
V. Menissier-Morain
article
RT-0141, INRIA. 1992, pp.157
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070027/file/RT-0141.pdf BibTex

1991

Reports

titre
Functional programming using CAML
auteur
Michel Mauny
article
[Research Report] RT-0129, INRIA. 1991, pp.119
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070039/file/RT-0129.pdf BibTex

1990

Reports

titre
The ZINC experiment : an economical implementation of the ML language
auteur
Xavier Leroy
article
RT-0117, INRIA. 1990, pp.100
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070049/file/RT-0117.pdf BibTex