Bibliography

Major publications by the team in recent years

1A. Charguéraud, F. Pottier.

Functional Translation of a Calculus of Capabilities, in: Proceedings of the 13th International Conference on Functional Programming (ICFP'08), ACM Press, September 2008, p. 213–224.

http://doi.acm.org/10.1145/1411204.1411235
2K. Chaudhuri, D. Doligez, L. Lamport, S. Merz.

Verifying Safety Properties With the TLA+ Proof System, in: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Lecture Notes in Computer Science, Springer, 2010, vol. 6173, p. 142–148.

http://dx.doi.org/10.1007/978-3-642-14203-1_12
3D. Le Botlan, D. Rémy.

Recasting MLF, in: Information and Computation, 2009, vol. 207, n^o 6, p. 726–785.

http://dx.doi.org/10.1016/j.ic.2008.12.006
4X. Leroy.

A formally verified compiler back-end, in: Journal of Automated Reasoning, 2009, vol. 43, n^o 4, p. 363–446.

http://dx.doi.org/10.1007/s10817-009-9155-4
5X. Leroy.

Formal verification of a realistic compiler, in: Communications of the ACM, 2009, vol. 52, n^o 7, p. 107–115.

http://doi.acm.org/10.1145/1538788.1538814
6B. Montagu, D. Rémy.

Modeling Abstract Types in Modules with Open Existential Types, in: Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09), ACM Press, January 2009, p. 354-365.

http://doi.acm.org/10.1145/1480881.1480926
7F. Pottier.

Hiding local state in direct style: a higher-order anti-frame rule, in: Proceedings of the 23rd Annual IEEE Symposium on Logic In Computer Science (LICS'08), IEEE Computer Society Press, June 2008, p. 331-340.

http://dx.doi.org/10.1109/LICS.2008.16
8F. Pottier, D. Rémy.

The Essence of ML Type Inference, in: Advanced Topics in Types and Programming Languages, B. C. Pierce (editor), MIT Press, 2005, chap. 10, p. 389–489.
9N. Pouillard, F. Pottier.

A fresh look at programming with names and binders, in: Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), ACM Press, 2010, p. 217–228.

http://doi.acm.org/10.1145/1863543.1863575
10J.-B. Tristan, X. Leroy.

A simple, verified validator for software pipelining, in: Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL'10), ACM Press, 2010, p. 83–92.

http://doi.acm.org/10.1145/1706299.1706311

Publications of the year

Articles in International Peer-Reviewed Journal

11A. W. Appel, R. Dockins, X. Leroy.

A list-machine benchmark for mechanized metatheory, in: Journal of Automated Reasoning, 2011, Accepted for publication, to appear.

http://dx.doi.org/10.1007/s10817-011-9226-1
12R. Di Cosmo, D. Di Ruscio, P. Pelliccione, A. Pierantonio, S. Zacchiroli.

Supporting software evolution in component-based FOSS systems, in: Science of Computer Programming, 2011, vol. 76, n^o 12, p. 1144–1160.

http://dx.doi.org/10.1016/j.scico.2010.11.001
13D. Rémy, B. Yakobowski.

A Church-Style Intermediate Language for MLF, in: Theoretical Computer Science, 2011, Accepted for publication, to appear.

http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski:xmlf@tcs2011.pdf

Articles in Non Peer-Reviewed Journal

14X. Leroy.

Safety first! (technical perspective), in: Communications of the ACM, December 2011, vol. 54, n^o 12, p. 122–122.

http://doi.acm.org/10.1145/2043174.2043196

Invited Conferences

15X. Leroy.

Formally verifying a compiler: Why? How? How far?, in: Proceedings of CGO 2011, The 9th International Symposium on Code Generation and Optimization, IEEE, 2011, Abstract of invited talk.

http://dx.doi.org/10.1109/CGO.2011.5764668
16X. Leroy.

Verified squared: does critical software deserve verified tools?, in: Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), ACM Press, 2011, p. 1–2, Extended abstract of invited talk.

http://dx.doi.org/10.1145/1926385.1926387

International Conferences with Proceedings

17P. Abate, R. Di Cosmo.

Predicting upgrade failures using dependency analysis, in: Workshops Proceedings of the 27th International Conference on Data Engineering, ICDE 2011, IEEE Computer Society Press, 2011, p. 145–150.

http://dx.doi.org/10.1109/ICDEW.2011.5767626
18P. Abate, R. Di Cosmo, R. Treinen, S. Zacchiroli.

MPM: a modular package manager, in: Proceedings of the 14th International ACM Sigsoft Symposium on Component Based Software Engineering, CBSE 2011, ACM Press, 2011, p. 179–188.

http://doi.acm.org/10.1145/2000229.2000255
19R. Bedin França, S. Blazy, D. Favre-Felix, X. Leroy, M. Pantel, J. Souyris.

Formally verified optimizing compilation in ACG-based flight control software, in: Embedded Real Time Software and Systems (ERTS2 2012), 2012, To appear.

http://hal.inria.fr/hal-00653367/
20R. Bedin França, D. Favre-Felix, X. Leroy, M. Pantel, J. Souyris.

Towards Formally Verified Optimizing Compilation in Flight Control Software, in: Bringing Theory to Practice: Predictability and Performance in Embedded Systems (PPES 2011), OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2011, vol. 18, p. 59–68.

http://dx.doi.org/10.4230/OASIcs.PPES.2011.59
21J. Cretin, D. Rémy.

On the Power of Coercion Abstraction, in: Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL'12), ACM Press, 2012, To appear.

http://gallium.inria.fr/~jcretin/papers/conf.pdf
22R. Di Cosmo, O. Lhomme, C. Michel.

Aligning component upgrades, in: Proceedings Second Workshop on Logics for Component Configuration, Electronic Proceedings in Theoretical Computer Science, 2011, vol. 65, p. 1–11.

http://dx.doi.org/10.4204/EPTCS.65.1
23R. Di Cosmo, J. Vouillon.

On software component co-installability, in: 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13rd European Software Engineering Conference (ESEC-13), ACM Press, 2011, p. 256–266.

http://doi.acm.org/10.1145/2025113.2025149
24J.-H. Jourdan, F. Pottier, X. Leroy.

Validating LR $(1)$ Parsers, in: European Symposium on Programming (ESOP'12), Springer, 2012, To appear.

http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf
25A. Pilkiewicz, F. Pottier.

The essence of monotonic state, in: 6th Workshop on Types in Language Design and Implementation (TLDI 2011), ACM Press, 2011, p. 73–86.

http://dx.doi.org/10.1145/1929553.1929565
26F. Pottier.

A typed store-passing translation for general references, in: Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), ACM Press, 2011, p. 147–158.

http://dx.doi.org/10.1145/1926385.1926403
27N. Pouillard.

Nameless, Painless, in: Proceedings of the 16th International Conference on Functional Programming (ICFP 2011), ACM Press, 2011, p. 320–332.

http://doi.acm.org/10.1145/2034773.2034817
28T. Ramananandro, G. Dos Reis, X. Leroy.

Formal verification of object layout for C++ multiple inheritance, in: Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), ACM Press, 2011, p. 67–80.

http://dx.doi.org/10.1145/1926385.1926395
29T. Ramananandro, G. Dos Reis, X. Leroy.

A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management, in: Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL'12), ACM Press, 2012, To appear.

http://gallium.inria.fr/~xleroy/publi/cpp-construction.pdf
30D. N. Xu.

Hybrid contract checking via symbolic simplification, in: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'12), ACM Press, 2012, To appear.

http://gallium.inria.fr/~naxu/research/hcc.pdf
31B. Yorgey, S. Weirich, J. Cretin, José Pedro. Magalhães, S. Peyton Jones, D. Vytiniotis.

Giving Haskell a Promotion, in: The Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), ACM Press, 2012, To appear.

http://gallium.inria.fr/~jcretin/papers/fc-kind-poly.pdf

Conferences without Proceedings

32P. Cuoq, D. Doligez, J. Signoles.

Lightweight typed customizable unmarshaling, in: ACM SIGPLAN Workshop on ML, ACM Press, 2011.

Internal Reports

33J. Cretin, D. Rémy.

On the Power of Coercion Abstraction, INRIA, December 2011, n^o RR-7587.

http://hal.inria.fr/inria-00582570/en/
34D. N. Xu.

Hybrid Contract Checking via Symbolic Simplification, INRIA, November 2011, n^o RR-7794.

http://hal.inria.fr/hal-00644156/en

Other Publications

35S. Dailler.

Preuve mécanisée de correction et de complexité pour un algorithme impératif, University Paris Diderot, August 2011, Report on Master's internship.
36J.-H. Jourdan.

Validation d'analyseurs syntaxiques LR(1): Vers un analyseur syntaxique certifié pour le compilateur CompCert, ENS Paris, August 2011, Report on Master's internship.
37F. Pottier.

Syntactic soundness proof of a type-and-capability system with hidden state, July 2011, Submitted for publication.

http://gallium.inria.fr/~fpottier/publis/fpottier-ssphs.pdf
38V. Robert.

Conception, mise en oeuvre et vérification d'une analyse d'alias pour CompCert, un compilateur C formellement vérifié, ENSEIRB, December 2011, Report on Master's internship.
39J. Schwinghammer, L. Birkedal, F. Pottier, B. Reus, K. Støvring, H. Yang.

A step-indexed Kripke Model of Hidden State, December 2011, Submitted for publication.

http://gallium.inria.fr/~fpottier/publis/sikmhs.pdf

References in notes

40L. O. Andersen.

Program Analysis and Specialization for the C Programming Language, DIKU, University of Copenhagen, 1994.
41V. Benzaken, G. Castagna, A. Frisch.

CDuce: an XML-centric general-purpose language, in: Int. Conf. on Functional programming (ICFP'03), ACM Press, 2003, p. 51–63.
42A. Frisch.

OCaml + XDuce, in: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, ACM Press, September 2006, p. 192–200.

http://doi.acm.org/10.1145/1159803.1159829
43J. Garrigue, J. Le Normand.

Adding GADTs to OCaml: the direct approach, in: ACM SIGPLAN Workshop on ML, ACM Press, 2011.
44H. Hosoya, B. C. Pierce.

XDuce: A Statically Typed XML Processing Language, in: ACM Transactions on Internet Technology, May 2003, vol. 3, n^o 2, p. 117–148.
45L. Lamport.

How to write a proof, in: American Mathematical Monthly, August 1993, vol. 102, n^o 7, p. 600–608.

http://research.microsoft.com/users/lamport/pubs/lamport-how-to-write.pdf
46X. Leroy, D. Doligez, J. Garrigue, D. Rémy, J. Vouillon.

The Objective Caml system, documentation and user's manual – release 3.12, INRIA, August 2010.

http://caml.inria.fr/pub/docs/manual-ocaml/
47X. Leroy.

Java bytecode verification: algorithms and formalizations, in: Journal of Automated Reasoning, 2003, vol. 30, n^o 3–4, p. 235–269.

http://gallium.inria.fr/~xleroy/publi/bytecode-verification-JAR.pdf
48B. Montagu.

Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts, École Polytechnique, December 2010, English title: Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types.

http://tel.archives-ouvertes.fr/tel-00550331/
49B. C. Pierce.

Types and Programming Languages, MIT Press, 2002.
50F. Pottier.

Simplifying subtyping constraints: a theory, in: Information and Computation, 2001, vol. 170, n^o 2, p. 153–183.
51F. Pottier, V. Simonet.

Information Flow Inference for ML, in: ACM Transactions on Programming Languages and Systems, January 2003, vol. 25, n^o 1, p. 117–158.

http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-toplas.ps.gz
52V. Prevosto, D. Doligez.

Algorithms and Proofs Inheritance in the FOC Language, in: Journal of Automated Reasoning, 2002, vol. 29, n^o 3–4, p. 337-363.
53D. Rémy, J. Vouillon.

Objective ML: A simple object-oriented extension to ML, in: 24th ACM Conference on Principles of Programming Languages, ACM Press, 1997, p. 40–53.

Previous |

Home