Publications in 2015

Conference papers:
[1] Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In POPL'15 - 42nd ACM Symposium on Principles of Programming Languages. ACM Press, 2015. To appear. [ bib | HAL archive | Local copy | At publisher's ]
[2] François Pottier. Depth-first search and strong connectivity in Coq. In JFLA 2015 - Journées Francophones des Langages Applicatifs, 2015. To appear. [ bib ]
[3] Gabriel Scherer. Normalization by realizability also evaluates. In JFLA 2015 - Journées Francophones des Langages Applicatifs, 2015. To appear. [ bib ]

Publications in 2014

PhD and habilitation theses:
[1] Julien Cretin. Erasable coercions: a unified approach to type systems. PhD thesis, Université Paris Diderot (Paris 7), January 2014. [ bib | HAL archive | Local copy ]
[2] Jonathan Protzenko. Mezzo, a typed language for safe effectful concurrent programs. PhD thesis, Université Paris Diderot (Paris 7), September 2014. [ bib | Local copy ]
Journal articles:
[1] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: modelling, simulation, testing, and data-mining for weak memory. ACM Transactions on Programming Languages and Systems, 36(2):article no 7, 2014. [ bib | HAL archive | Local copy | At publisher's ]
[2] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning, 2014. To appear. [ bib | Local copy ]
[3] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. Journal of Automated Reasoning, 53(3):271-304, 2014. [ bib | At publisher's ]
[4] Pierre-Évariste Dagand and Conor McBride. Transporting functions across ornaments. Journal of Functional Programming, 24(2-3):316-383, 2014. [ bib | HAL archive | At publisher's ]
Conference papers:
[1] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Theory and practice of chunked sequences. In European Symposium on Algorithmes, ESA 2014, volume 8737 of Lecture Notes in Computer Science, pages 25-36. Springer, 2014. [ bib | At publisher's ]
[2] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: modelling, simulation, testing, and data-mining for weak memory. In PLDI 2014: ACM SIGPLAN Conference on Programming Language Design and Implementation, page 7. ACM Press, 2014. Presentation of TOPLAS paper. [ bib | HAL archive | At publisher's ]
[3] Thibaut Balabonski, Francois Pottier, and Jonathan Protzenko. Type soundness and race freedom for Mezzo. In FLOPS 2014: Functional and Logic Programming, volume 8475 of Lecture Notes in Computer Science, pages 253-269. Springer, 2014. [ bib | HAL archive | Local copy | At publisher's ]
[4] Thomas Braibant, Jonathan Protzenko, and Gabriel Scherer. Well-typed generic smart-fuzzing for APIs. In ML'14 - ACM SIGPLAN ML Family Workshop, 2014. [ bib | Local copy ]
[5] Julien Cretin and Didier Rémy. System F with coercion constraints. In CSL-LICS 2014: Computer Science Logic / Logic In Computer Science, page article no 34. ACM, 2014. [ bib | At publisher's ]
[6] Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz. Coalescing: Syntactic abstraction for reasoning in first-order modal logics. In ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics, 2014. [ bib | HAL archive ]
[7] Robbert Krebbers, Xavier Leroy, and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP 2014: Interactive Theorem Proving, number 8558 in Lecture Notes in Computer Science, pages 543-548. Springer, 2014. [ bib | HAL archive | At publisher's ]
[8] Gregory Malecha, Adam Chlipala, and Thomas Braibant. Compositional computational reflection. In ITP 2014: Interactive Theorem Proving, number 8558 in Lecture Notes in Computer Science, pages 374-389. Springer, 2014. [ bib | At publisher's ]
[9] François Pottier. Hindley-Milner elaboration in applicative style. In ICFP 2014: Proceedings of the 19th International Conference on Functional Programming, pages 203-212. ACM, 2014. [ bib | HAL archive | Local copy | At publisher's ]
[10] Thomas Williams, Pierre Évariste Dagand, and Didier Rémy. Ornaments in practice. In WGP'14 - 10th ACM SIGPLAN Workshop on Generic Programming, 2014. [ bib | HAL archive | Local copy | At publisher's ]
Book chapters:
[1] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model. In Andrew W. Appel, editor, Program Logics for Certified Compilers, pages 237-271. Cambridge University Press, March 2014. [ bib | HAL archive ]
Others:
[1] Julien Cretin and Didier Rémy. System F with coercion constraints. Research Report RR-8456, INRIA, January 2014. [ bib | HAL archive ]

Publications in 2013

Journal articles:
[1] François Pottier. Syntactic soundness proof of a type-and-capability system with hidden state. Journal of Functional Programming, 23(1):38-144, 2013. [ bib | HAL archive | Local copy | At publisher's ]
[2] Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, and Hongseok Yang. A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1):1-54, 2013. [ bib | HAL archive | Local copy | At publisher's ]
Conference papers:
[1] Thibaut Balabonski. Weak optimality, and the meaning of sharing. In Proceedings of the 18th International Conference on Functional Programming (ICFP 2013), pages 263-274. ACM Press, 2013. [ bib | HAL archive | Local copy | At publisher's ]
[2] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 107-115. IEEE Computer Society Press, 2013. [ bib | HAL archive | At publisher's ]
[3] Thomas Braibant and Adam Chlipala. Formal verification of hardware synthesis. In CAV 2013, 25th International Conference on Computer Aided Verification, volume 8044 of Lecture Notes in Computer Science, pages 213-228. Springer, 2013. [ bib | HAL archive | Local copy | At publisher's ]
[4] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. In Interactive Theorem Proving, ITP 2013, volume 7998 of Lecture Notes in Computer Science, pages 477-483. Springer, 2013. [ bib | HAL archive | At publisher's ]
[5] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof certification in Zenon modulo: When Achilles uses deduction modulo to outrun the tortoise with shorter steps. In IWIL 2013, 10th International Workshop on the Implementation of Logics. EasyChair, 2013. [ bib | HAL archive ]
[6] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles outruns the tortoise using deduction modulo. In LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 8312 of Lecture Notes in Computer Science, pages 274-290. Springer, 2013. [ bib | HAL archive ]
[7] Jacques Garrigue and Didier Rémy. Ambivalent types for principal type inference with GADTs. In Chung-chien Shan, editor, 11th Asian Symposium on Programming Languages and Systems, APLAS 2013, volume 8301 of Lecture Notes in Computer Science, pages 257-272, Melbourne, VIC, Australia, December 2013. Springer. [ bib | HAL archive ]
[8] François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. In Proceedings of the 18th International Conference on Functional Programming (ICFP 2013), pages 173-184. ACM Press, 2013. [ bib | HAL archive | Local copy | At publisher's ]
[9] Gabriel Scherer and Jan Hoffmann. Tracking data-flow with open closure types. In LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 8312 of Lecture Notes in Computer Science, pages 710-726. Springer, 2013. [ bib | HAL archive ]
[10] Gabriel Scherer and Didier Rémy. GADTs meet subtyping. In European Symposium on Programming, ESOP 2013, volume 7792 of Lecture Notes in Computer Science, pages 554-573. Springer, 2013. [ bib | HAL archive | At publisher's ]
Others:
[1] Umut Acar, Arthur Charguéraud, Stefan Muller, and Mike Rainey. Atomic read-modify-write operations are unnecessary for shared-memory work stealing. September 2013. [ bib | HAL archive ]
[2] Xavier Leroy. The CompCert C verified compiler, documentation and user's manual. INRIA, October 2013. [ bib | Local copy ]
[3] Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, documentation and user's manual - release 4.01. INRIA, September 2013. [ bib | Local copy ]
[4] Gabriel Scherer and Jan Hoffmann. Tracking data-flow with open closure types. Research Report RR-8345, Inria, August 2013. [ bib | HAL archive ]

Publications in 2012

PhD and habilitation theses:
[1] Nicolas Pouillard. Une approche unifiante pour programmer sûrement avec de la syntaxe du premier ordre contenant des lieurs / Namely, Painless: A unifying approach to safe programming with first-order syntax with binders. PhD thesis, Université Paris Diderot (Paris 7), January 2012. [ bib | HAL archive | Local copy ]
[2] Tahina Ramananandro. Machine-checked Formal Semantics and Verified Compilation for C++ Objects. PhD thesis, Université Paris Diderot (Paris 7), January 2012. [ bib | HAL archive | Local copy ]
Journal articles:
[1] Andrew W. Appel, Robert Dockins, and Xavier Leroy. A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning, 49(3):453-491, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[2] Gregor Gössler, Dana N. Xu, and Alain Girault. Probabilistic contracts for component-based design. Formal Methods in System Design, 41(2):211-231, 2012. [ bib | HAL archive | At publisher's ]
[3] Luc Maranget, Jade Alglave, Susmit Sarkar, and Peter Sewell. Fences in weak memory models (extended version). Formal Methods in System Design, 40(2):170-205, 2012. [ bib | HAL archive | At publisher's ]
[4] Nicolas Pouillard and François Pottier. A unified treatment of syntax with binders. Journal of Functional Programming, 22(4-5):614-704, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[5] Didier Rémy and Boris Yakobowski. A Church-style intermediate language for MLF. Theoretical Computer Science, 435(1):77-105, 2012. [ bib | Local copy | At publisher's ]
Conference papers:
[1] Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In Embedded Real Time Software and Systems (ERTS2 2012). AAAF, SEE, 2012. [ bib | HAL archive ]
[2] Thomas Braibant and Adam Chlipala. Formal verification of hardware synthesis. In The Coq Workshop, 2012. [ bib | Local copy ]
[3] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA + proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods - 18th International Symposium, volume 7436 of Lecture Notes in Computer Science, pages 147-154. Springer, 2012. [ bib | HAL archive | At publisher's ]
[4] Julien Cretin and Didier Rémy. On the power of coercion abstraction. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL'12), pages 361-372. ACM Press, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[5] Damien Doligez, Mathieu Jaume, and Renaud Rioboo. Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment. In Proceedings of the 7th Workshop on Programming Languages and Analysis for Security (PLAS'12), pages 9:1-9:12. ACM Press, 2012. [ bib | HAL archive | At publisher's ]
[6] Jacques Garrigue and Didier Rémy. Tracing ambiguity in GADT type inference. In ACM SIGPLAN Workshop on ML, 2012. [ bib | Local copy ]
[7] Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. Validating LR(1) parsers. In H. Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, volume 7211 of Lecture Notes in Computer Science, pages 397-416. Springer, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[8] Xavier Leroy. Mechanized semantics for compiler verification. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of Lecture Notes in Computer Science, pages 386-388. Springer, 2012. Abstract of invited talk. [ bib | HAL archive | Local copy | At publisher's ]
[9] Jonathan Protzenko and François Pottier. Programming with permissions: the Mezzo language. In ACM SIGPLAN Workshop on ML, 2012. [ bib | Local copy ]
[10] Tahina Ramananandro, Gabriel Dos Reis, and Xavier 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), pages 521-532. ACM Press, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[11] Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs - Second International Conference, CPP 2012, volume 7679 of Lecture Notes in Computer Science, pages 11-26. Springer, 2012. [ bib | HAL archive | Local copy | At publisher's ]
[12] Gabriel Scherer and Didier Rémy. GADTs meet subtyping. In ACM SIGPLAN Workshop on ML, 2012. [ bib | Local copy ]
[13] Dana N. Xu. Hybrid contract checking via symbolic simplification. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'12), pages 107-116. ACM Press, 2012. [ bib | Local copy | At publisher's ]
[14] Brent Yorgey, Stephanie Weirich, Julien Cretin, José Pedro Magalhães, Simon Peyton Jones, and Dimitrios Vytiniotis. Giving Haskell a promotion. In The Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'12), pages 67-78. ACM Press, 2012. [ bib | Local copy | At publisher's ]
Others:
[1] Gregor Gössler, Dana N. Xu, and Alain Girault. Probabilistic contracts for component-based design. Research Report RR-7328, INRIA, July 2012. [ bib | Local copy ]
[2] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. [ bib | Local copy ]
[3] François Pottier and Jonathan Protzenko. An introduction to Mezzo. Unpublished draft, September 2012. [ bib | Local copy ]
[4] Gabriel Scherer and Didier Rémy. GADT meet subtyping. Research report RR-8114, INRIA, October 2012. [ bib | Local copy ]

Publications in 2011

Journal articles:
[1] Roberto Di Cosmo, Davide Di Ruscio, Patrizio Pelliccione, Alfonso Pierantonio, and Stefano Zacchiroli. Supporting software evolution in component-based FOSS systems. Science of Computer Programming, 76(12):1144-1160, 2011. [ bib | At publisher's ]
Conference papers:
[1] Pietro Abate and Roberto Di Cosmo. Predicting upgrade failures using dependency analysis. In Workshops Proceedings of the 27th International Conference on Data Engineering, ICDE 2011, pages 145-150. IEEE Computer Society Press, 2011. [ bib | Local copy ]
[2] Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli. MPM: a modular package manager. In Proceedings of the 14th International ACM Sigsoft Symposium on Component Based Software Engineering, CBSE 2011, pages 179-188. ACM Press, 2011. [ bib | At publisher's ]
[3] Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. Towards formally verified optimizing compilation in flight control software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems (PPES 2011), volume 18 of OpenAccess Series in Informatics (OASIcs), pages 59-68. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2011. [ bib | HAL archive | At publisher's ]
[4] Pascal Cuoq, Damien Doligez, and Julien Signoles. Lightweight typed customizable unmarshaling. In ACM SIGPLAN Workshop on ML. ACM Press, 2011. [ bib ]
[5] Roberto Di Cosmo, Olivier Lhomme, and Claude Michel. Aligning component upgrades. In Proceedings Second Workshop on Logics for Component Configuration, volume 65 of Electronic Proceedings in Theoretical Computer Science, pages 1-11, 2011. [ bib | At publisher's ]
[6] Roberto Di Cosmo and Jérôme 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), pages 256-266. ACM Press, 2011. [ bib | At publisher's ]
[7] Xavier 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. [ bib | At publisher's ]
[8] Xavier Leroy. Verified squared: does critical software deserve verified tools? In Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), pages 1-2. ACM Press, 2011. Extended abstract of invited talk. [ bib | HAL archive | Local copy | At publisher's ]
[9] Alexandre Pilkiewicz and François Pottier. The essence of monotonic state. In 6th Workshop on Types in Language Design and Implementation (TLDI 2011), pages 73-86. ACM Press, 2011. [ bib | HAL archive | Local copy | At publisher's ]
[10] François Pottier. A typed store-passing translation for general references. In Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), pages 147-158. ACM Press, 2011. [ bib | HAL archive | Local copy | At publisher's ]
[11] Nicolas Pouillard. Nameless, painless. In Proceedings of the 16th International Conference on Functional Programming (ICFP 2011), pages 320-332. ACM Press, 2011. [ bib | Local copy | At publisher's ]
[12] Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy. Formal verification of object layout for C++ multiple inheritance. In Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL'11), pages 67-80. ACM Press, 2011. [ bib | HAL archive | Local copy | At publisher's ]
Others:
[1] Julien Cretin and Didier Rémy. On the Power of Coercion Abstraction. Research Report RR-7587, INRIA, December 2011. [ bib | Local copy | Pdf ]
[2] Sylvain Dailler. Preuve mécanisée de correction et de complexité pour un algorithme impératif. Master's thesis, University Paris Diderot, August 2011. Report on Master's internship. [ bib ]
[3] Jacques-Henri Jourdan. Validation d'analyseurs syntaxiques LR(1): Vers un analyseur syntaxique certifié pour le compilateur CompCert. Master's thesis, ENS Paris, August 2011. Report on Master's internship. [ bib ]
[4] Xavier Leroy. Safety first! (technical perspective). Communications of the ACM, 54(12):122-122, December 2011. [ bib | At publisher's ]
[5] Valentin Robert. Conception, mise en oeuvre et vérification d'une analyse d'alias pour CompCert, un compilateur C formellement vérifié. Master's thesis, ENSEIRB, December 2011. Report on Master's internship. [ bib ]
[6] Dana N. Xu. Hybrid contract checking via symbolic simplification. Research Report RR-7794, INRIA, November 2011. [ bib | Local copy ]

Publications in 2010

PhD and habilitation theses:
[1] Arthur Charguéraud. Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris Diderot (Paris 7), December 2010. [ bib | Local copy ]
[2] Benoît Montagu. Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts. PhD thesis, École Polytechnique, December 2010. English title: Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types. [ bib | Local copy ]
Journal articles:
[1] Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta. On isomorphisms of intersection types. ACM Transactions on Computational Logic, 11(4):Article No. 25, 2010. [ bib | At publisher's ]
Conference papers:
[1] Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and Benjamin C. Pierce. Matching lenses: Alignment and view update. In Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), pages 193-204. ACM Press, 2010. [ bib | At publisher's ]
[2] Arthur Charguéraud. Program verification through characteristic formulae. In Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), pages 321-332. ACM Press, 2010. [ bib | Local copy | At publisher's ]
[3] Arthur Charguéraud. The optimal fixed point combinator. In Interactive Theorem Proving (ITP 2010), volume 6172 of Lecture Notes in Computer Science, pages 195-210. Springer, 2010. [ bib | Local copy | At publisher's ]
[4] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. Verifying safety properties with the TLA+ proof system. In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, volume 6173 of Lecture Notes in Computer Science, pages 142-148. Springer, 2010. [ bib | At publisher's ]
[5] Roberto Di Cosmo and Jaap Boender. Using strong conflicts to detect quality issues in component-based complex systems. In ISEC '10: Proceedings of the 3rd India software engineering conference, pages 163-172. ACM Press, 2010. [ bib | At publisher's ]
[6] Roberto Di Cosmo and Stefano Zacchiroli. Feature diagrams as package dependencies. In Software Product Lines: Going Beyond - 14th International Conference, SPLC 2010, volume 6287 of Lecture Notes in Computer Science, pages 476-480. Springer, 2010. [ bib | At publisher's ]
[7] Benoît Montagu. Experience report: Mechanizing Core F-zip using the locally nameless approach (extended abstract). In 5th ACM SIGPLAN Workshop on Mechanizing Metatheory, 2010. [ bib | At publisher's ]
[8] Benoît Montagu and Didier Rémy. Types abstraits et types existentiels ouverts. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, pages 147-148, Université de Pau, March 2010. [ bib | At publisher's ]
[9] Nicolas Pouillard and François Pottier. A fresh look at programming with names and binders. In Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), pages 217-228. ACM Press, 2010. [ bib | Local copy | At publisher's ]
[10] Didier Rémy and Boris Yakobowski. A Church-style intermediate language for MLF. In Functional and Logic Programming, 10th International Symposium, FLOPS 2010, volume 6009 of Lecture Notes in Computer Science, pages 24-39. Springer, 2010. [ bib | Local copy | At publisher's ]
[11] Silvain Rideau and Xavier Leroy. Validating register allocation and spilling. In Compiler Construction (CC 2010), volume 6011 of Lecture Notes in Computer Science, pages 224-243. Springer, 2010. [ bib | Local copy | At publisher's ]
[12] Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, and Bernhard Reus. A semantic foundation for hidden state. In Foundations of Software Science and Computation Structures (FoSSaCS 2010), volume 6014 of Lecture Notes in Computer Science, pages 2-17. Springer, 2010. [ bib | Local copy | At publisher's ]
[13] Jean-Baptiste Tristan and Xavier Leroy. A simple, verified validator for software pipelining. In Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL'10), pages 83-92. ACM Press, 2010. [ bib | Local copy | At publisher's ]
[14] Dana N. Xu, Gregor Gössler, and Alain Girault. Probabilistic contracts for component-based design. In Automated Technology for Verification and Analysis (ATVA 2010), volume 6252 of Lecture Notes in Computer Science, pages 325-340. Springer, 2010. [ bib | Local copy | At publisher's ]
Book chapters:
[1] Xavier Leroy. Mechanized semantics. In Logics and languages for reliability and security, volume 25 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 195-224. IOS Press, 2010. [ bib | Local copy | At publisher's ]
Others:
[1] Julien Cretin. A generalization of F-eta with abstraction over retyping functions. Master's thesis, École Polytechnique, December 2010. [ bib | Local copy ]
[2] Xavier Leroy. Comment faire confiance à un compilateur? La Recherche, 440, April 2010. Les cahiers de l'INRIA. [ bib | Local copy | At publisher's ]
[3] Gabriel Scherer. Extending MLF with higher-order types. Master's thesis, École Normale Supérieure, Paris, August 2010. [ bib | Local copy ]
[4] Dana N. Xu, Gregor Gössler, and Alain Girault. Probabilistic Contracts for Component-based Design. Research Report RR-7328, INRIA, July 2010. [ bib | Local copy ]

Publications in 2009

PhD and habilitation theses:
[1] Zaynah Dargaye. Vérification formelle d'un compilateur optimisant pour langages fonctionnels. PhD thesis, University Paris Diderot (Paris 7), July 2009. English title: Formal verification of an optimizing compiler for functional languages. [ bib | Local copy ]
[2] Jean-Baptiste Tristan. Formal verification of translation validators. PhD thesis, University Paris Diderot (Paris 7), November 2009. [ bib | Local copy ]
Journal articles:
[1] Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009. [ bib | Local copy | At publisher's ]
[2] Zaynah Dargaye and Xavier Leroy. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation, 22(3):199-231, 2009. [ bib | Local copy | At publisher's ]
[3] Tom Hirschowitz, Xavier Leroy, and J. B. Wells. Compilation of extended recursion in call-by-value functional languages. Higher-Order and Symbolic Computation, 22(1):3-66, 2009. [ bib | Local copy | At publisher's ]
[4] Didier Le Botlan and Didier Rémy. Recasting MLF. Information and Computation, 207(6):726-785, 2009. [ bib | DOI | Local copy | At publisher's ]
[5] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. [ bib | Local copy | At publisher's ]
[6] Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. [ bib | Local copy | At publisher's ]
[7] Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. [ bib | Local copy | At publisher's ]
Conference papers:
[1] Pietro Abate, Jaap Boender, Roberto Di Cosmo, and Stefano Zacchiroli. Strong dependencies between software components. In 3rd International Symposium on Empirical Sofware Engineering and Measurement, ESEM 2009, pages 89-99. IEEE Computer Society Press, October 2009. [ bib | At publisher's ]
[2] Sandrine Blazy and Benoît Robillard. Live-range unsplitting for faster optimal coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), pages 70-79. ACM Press, 2009. [ bib | Local copy | At publisher's ]
[3] Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, and Gilles Muller. A foundation for flow-based program matching using temporal logic and model checking. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL'09), pages 114-126. ACM Press, January 2009. [ bib | At publisher's ]
[4] Benoît Montagu and Didier 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), pages 354-365. ACM Press, January 2009. [ bib | Local copy | At publisher's ]
[5] Jean-Baptiste Tristan and Xavier Leroy. Verified validation of Lazy Code Motion. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09), pages 316-326. ACM Press, 2009. [ bib | Local copy | At publisher's ]
Others:
[1] Roberto Di Cosmo. La science du logiciel libre. La Recherche, 436, December 2009. Les cahiers de l'INRIA. [ bib | Local copy ]
[2] Roberto Di Cosmo. Offrons aux jeunes les clés du pouvoir et de la liberté. Science et Avenir, 751:42-45, September 2009. [ bib | At publisher's ]
[3] Paolo Herms. Partial Type Inference with Higher-Order Types. Master's thesis, University of Pisa, July 2009. [ bib | Local copy ]

Publications in 2008

PhD and habilitation theses:
[1] Sandrine Blazy. Sémantiques formelles. Habilitation à diriger les recherches, Université Évry Val d'Essone, October 2008. English title: Formalized semantics. [ bib | Local copy ]
[2] Boris Yakobowski. Graphical types and constraints: second-order polymorphism and inference. PhD thesis, University Paris Diderot (Paris 7), December 2008. [ bib | Local copy ]
Journal articles:
[1] Blandine Doligez, Anne Berthouly, Damien Doligez, Marion Tanner, Verena Saladin, Danielle Bonfils, and Heinz Richner. Spatial scale of local breeding habitat quality and adjustment of breeding decisions in a wild tit population. Ecology, 89(5):1436-1444, 2008. [ bib | At publisher's ]
[2] Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1-31, 2008. [ bib | Local copy | At publisher's ]
[3] Laurence Rideau, Bernard Paul Serpette, and Xavier Leroy. Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, 40(4):307-326, 2008. [ bib | Local copy | At publisher's ]
Conference papers:
[1] Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 3-15. ACM Press, January 2008. [ bib | Local copy | At publisher's ]
[2] Philippe Ayrault, Matthieu Carlier, David Delahaye, Catherine Dubois, Damien Doligez, Lionel Habib, Thérèse Hardin, Mathieu Jaume, Charles Morisset, François Pessaux, Renaud Rioboo, and Pierre Weis. Trusted software within Focal. In Pascal Chour, Yves Correc, Olivier Heen, and Ludovic Mé, editors, Computer & Electronics Security Applications Rendez-vous (C&SAR 2008), pages 142-158, December 2008. [ bib | Local copy ]
[3] Sandrine Blazy, Benoît Robillard, and Éric Soutif. Coloration avec préférences: complexité, inégalités valides et vérification formelle. In ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, February 2008. [ bib | Local copy ]
[4] Sandrine Blazy, Benoît Robillard, and Éric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. In Journées Francophones des Langages Applicatifs (JFLA'08), pages 31-46, Étretat, France, January 2008. INRIA. [ bib | Local copy | At publisher's ]
[5] Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In Proceedings of the 13th International Conference on Functional Programming (ICFP'08), pages 213-224. ACM Press, September 2008. [ bib | Local copy | At publisher's ]
[6] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. A TLA+ proof system. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors, Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, November 2008. [ bib | Local copy ]
[7] Pascal Cuoq and Damien Doligez. Hashconsing in an incrementally garbage-collected system: A story of weak pointers and hashconsing in OCaml 3.10.2. In 2008 ACM SIGPLAN Workshop on ML, pages 13-22. ACM Press, September 2008. [ bib | At publisher's ]
[8] J. Nathan Foster, Alexandre Pilkiewicz, and Benjamin C. Pierce. Quotient lenses. In Proceedings of the 13th International Conference on Functional Programming (ICFP'08), pages 383-396. ACM Press, September 2008. [ bib | Local copy | At publisher's ]
[9] François 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), pages 331-340. IEEE Computer Society Press, June 2008. [ bib | Local copy | At publisher's ]
[10] Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Mathematics of Program Construction, 9th International Conference, MPC 2008, volume 5133 of Lecture Notes in Computer Science, pages 305-335. Springer, July 2008. [ bib | Local copy | At publisher's ]
[11] Jean-Baptiste Tristan and Xavier Leroy. Formal verification of translation validators: A case study on instruction scheduling optimizations. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 17-27. ACM Press, January 2008. [ bib | Local copy | At publisher's ]
[12] Boris Yakobowski. Le caractère “backquote” à la rescousse - Factorisation et réutilisation de code grâce aux variants polymorphes. In Journées Francophones des Langages Applicatifs (JFLA'08), pages 63-78, Étretat, France, January 2008. INRIA. [ bib | Local copy | At publisher's ]
[13] Boris Yakobowski and Didier Rémy. Graphic type constraints and efficient type inference: from ML to MLF. In Proceedings of the 13th International Conference on Functional Programming (ICFP'08), pages 63-74. ACM Press, September 2008. [ bib | Local copy | At publisher's ]
Others:
[1] Alexandre Pilkiewicz. Towards a foundational type system for complexity analysis. Master's dissertation (mémoire de stage de Master 2), École Polytechnique, November 2008. [ bib ]

Publications in 2007

PhD and habilitation theses:
[1] Yann Régis-Gianas. Des types aux assertions logiques: Preuve automatique ou assistée de propriétés sur les programmes fonctionnels. PhD thesis, University Paris Diderot (Paris 7), November 2007. English title: From types to logical assertions: automated or assisted proof of properties over functional programs. [ bib | Local copy ]
Journal articles:
[1] Sandrine Blazy. Comment gagner confiance en C ? Technique et Science Informatiques, 26(9):1195-1200, 2007. [ bib | Local copy ]
[2] Vincent Simonet and François Pottier. A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems, 29(1):article no. 1, January 2007. [ bib | Local copy | At publisher's ]
Conference papers:
[1] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 5-21. Springer, 2007. [ bib | Local copy ]
[2] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). In Proc. Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP'06), volume 174(5) of Electronic Notes in Computer Science, pages 95-108, 2007. [ bib | Local copy | At publisher's ]
[3] Sandrine Blazy. Experiments in validating formal semantics for C. In Proceedings of the C/C++ Verification Workshop, pages 95-102. Technical report ICIS-R07015, Radboud University Nijmegen, 2007. [ bib | Local copy ]
[4] Sandrine Blazy, Benoît Robillard, and Éric Soutif. Coloration avec préférences dans les graphes triangulés. In Journées Graphes et Algorithmes (JGA'07), nov 2007. [ bib | Local copy ]
[5] Richard Bonichon, David Delahaye, and Damien Doligez. Zenon: an extensible automated theorem prover producing checkable proofs. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 151-165. Springer, 2007. [ bib | Local copy ]
[6] Zaynah Dargaye. Décurryfication certifiée. In Journées Francophones des Langages Applicatifs (JFLA'07), pages 119-134. INRIA, 2007. [ bib | Local copy ]
[7] Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial Intelligence, pages 211-225. Springer, 2007. [ bib | Local copy ]
[8] Alain Frisch and Haruo Hosoya. Towards practical typechecking for macro tree transducers. In Database Programming Languages, 11th International Symposium, DBPL 2007, volume 4797 of Lecture Notes in Computer Science, pages 246-260. Springer, 2007. [ bib | Local copy ]
[9] Alain Frisch and Keisuke Nakano. Streaming XML transformations using term rewriting. In Workshop Programming Language Technologies for XML (PLAN-X 2007), pages 2-13, January 2007. [ bib | Local copy ]
[10] Peng Li, Simon Marlow, Simon Peyton Jones, and Andrew Tolmach. Lightweight concurrency primitives for GHC. In Haskell '07: Proceedings of the ACM SIGPLAN workshop on Haskell, pages 107-118. ACM Press, 2007. [ bib | Local copy ]
[11] François Pottier. Static name control for FreshML. In Twenty-Second Annual IEEE Symposium on Logic In Computer Science (LICS'07), pages 356-365. IEEE Computer Society Press, July 2007. [ bib | Local copy | At publisher's ]
[12] Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 27-38. ACM Press, January 2007. [ bib | Local copy ]
Others:
[1] Andrew W. Appel and Sandrine Blazy. Separation logic for small-step Cminor (extended version). Research report 6138, INRIA, 2007. [ bib | Local copy ]
[2] Arthur Charguéraud. Proof of imperative programs. Master's dissertation (mémoire de stage de Master 2), ENS Lyon, September 2007. [ bib ]
[3] Didier Le Botlan and Didier Rémy. Recasting MLF. Research report 6228, INRIA, June 2007. [ bib | Local copy ]
[4] Xavier Leroy. A locally nameless solution to the POPLmark challenge. Research report 6098, INRIA, January 2007. [ bib | Local copy ]
[5] Benoît Montagu. Modules de première classe. Master's dissertation (mémoire de stage de Master 2), École Polytechnique, September 2007. [ bib | Local copy ]
[6] Tahina Ramananandro. Vérification formelle d'une implémentation d'un gestionnaire de mémoire pour un compilateur certifié. Master's dissertation (mémoire de stage de Master 2), ENS Paris, September 2007. [ bib | Local copy ]

Publications in 2006

PhD and habilitation theses:
[1] Richard Bonichon. Tableaux et Déduction Modulo. PhD thesis, University Paris 6, December 2006. [ bib ]
Journal articles:
[1] François Pottier and Nadji Gauthier. Polymorphic typed defunctionalization and concretization. Higher-Order and Symbolic Computation, 19(1):125-162, March 2006. [ bib | Local copy ]
Conference papers:
[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, 2006. [ bib | Local copy ]
[2] Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: Int. Symp. on Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 460-475. Springer, 2006. [ bib | Local copy | At publisher's ]
[3] Jaap Boender, Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, Mario Morgado, David Pinheiro, Ralf Treinen, Paulo Trezentos, and Jérôme Vouillon. News from the EDOS project: improving the maintenance of free software distributions. In Proceedings of the VIIth International Workshop on Free Software (IWFS'06), pages 199-207, 2006. [ bib | Local copy ]
[4] Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, and Jérôme Vouillon. Maintaining large software distributions: new challenges from the FOSS era. In Proceedings of the FRCSS 2006 workshop, volume 12 of EASST Newsletter, pages 7-20, 2006. [ bib | Local copy ]
[5] Alain Frisch. OCaml + XDuce. In Workshop Programming Language Technologies for XML (PLAN-X) 2006, pages 36-48. BRICS Notes series NS-05-6, University of Aarhus, January 2006. [ bib ]
[6] Alain Frisch. OCaml + XDuce. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 192-200. ACM Press, September 2006. [ bib | Local copy ]
[7] 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, pages 133-146. INRIA, January 2006. [ bib | Local copy ]
[8] Xavier Leroy. Coinductive big-step operational semantics. In European Symposium on Programming (ESOP'06), volume 3924 of Lecture Notes in Computer Science, pages 54-68. Springer, 2006. [ bib | Local copy | At publisher's ]
[9] 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. [ bib | Local copy | At publisher's ]
[10] Fabio Mancinelli, Roberto Di Cosmo, Jérôme Vouillon, Jaap Boender, Berke Durak, Xavier Leroy, and Ralf Treinen. Managing the complexity of large free and open source package-based software distributions. In 21st IEEE Int. Conf. on Automated Software Engineering (ASE 2006), pages 199-208. IEEE Computer Society Press, 2006. [ bib | Local copy ]
[11] 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. [ bib | Local copy ]
Book chapters:
[1] Emmanuel Chailloux and Michel Mauny. Programmation fonctionnelle. In Encyclopédie des systèmes d'information, pages 1016-1027. Éditions Vuibert, 2006. [ bib ]
Others:
[1] Andrew W. Appel and Xavier Leroy. A list-machine benchmark for mechanized metatheory. Research report 5914, INRIA, 2006. [ bib | Local copy ]
[2] Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. Extended version of the TLDI'07 article, September 2006. [ bib | Local copy | Pdf ]
[3] Jean-Baptiste Tristan. Certification d'un validateur de transformations. Master's dissertation (mémoire de stage de Master 2), ENS Paris, September 2006. [ bib | Local copy ]