Publications in 2019

Books:
[1] Steve Kremer, Ludovic Mé, Didier Rémy, and Vincent Roca. Cybersecurity, volume 3 of Inria white books. Inria, January 2019. [ bib | HAL archive ]
[2] Xavier Leroy. Le logiciel, entre l'esprit et la matière, volume 284 of Leçons inaugurales du Collège de France. Fayard, September 2019. [ bib ]
Conference papers:
[1] Umut Acar, Vitaly Aksenov, Arthur Charguéraud, and Mike Rainey. Provably and practically efficient granularity control. In PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, pages 213--228. ACM Press, 2019. [ bib | HAL archive | At publisher's ]
[2] Cagdas Bozman, Benjamin Canou, Roberto Di Cosmo, Pierrick Couderc, Louis Gesbert, Grégoire Henry, Fabrice le Fessant, Michel Mauny, Carine Morel, and Loïc Peyrot. Learn-OCaml : un assistant à l'enseignement d'OCaml. In Journées Francophones des Langages Applicatifs (JFLA), January 2019. [ bib | HAL archive ]
[3] Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal proof and analysis of an incremental cycle detection algorithm. In ITP 2019, 10th Conference on Interactive Theorem Proving, volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1--18:20. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, September 2019. [ bib | HAL archive | At publisher's ]
[4] Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in Iris. In Luis Caires, editor, European Symposium on Programming (ESOP), volume 11423 of Lecture Notes in Computer Science, pages 1--27. Springer, April 2019. [ bib | Local copy | At publisher's ]

Publications in 2018

PhD and habilitation theses:
[1] Vitalii Aksenov. Synchronization Costs in Parallel Programs and Concurrent Data Structures. PhD thesis, ITMO University; Paris Diderot University, September 2018. [ bib | HAL archive ]
Journal articles:
[1] Thomas Williams and Didier Rémy. A principled approach to ornamentation in ML. Proc. ACM on Programming Languages, 2(POPL), January 2018. [ bib | HAL archive | At publisher's ]
Conference papers:
[1] Umut A. Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, and Filip Sieczkowski. Heartbeat scheduling: provable efficiency for nested parallelism. In PLDI 2018: 39th ACM Conference on Programming Language Design and Implementation, pages 769--782. ACM, 2018. [ bib | Local copy | At publisher's ]
[2] Vitalii Aksenov, Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Poster: Performance challenges in modular parallel programs. In PPoPP 2018: 23rd ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, February 2018. [ bib | DOI | HAL archive | At publisher's ]
[3] Vitalii Aksenov, Dan Alistarh, and Petr Kuznetsov. Brief announcement: Performance prediction for coarse-grained locking. In PODC 2018 -- ACM Symposium on Principles of Distributed Computing, July 2018. [ bib | DOI | HAL archive ]
[4] Jade Alglave, Luc Maranget, Paul McKenney, Andrea Parri, and Alan Stern. Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel. In ASPLOS2018 - 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pages 405--418. ACM Press, 2018. [ bib | HAL archive | At publisher's ]
[5] Gergö Barany. Finding missed compiler optimizations by differential testing. In 27th International Conference on Compiler Construction, Vienna, Austria, February 2018. [ bib | HAL archive | At publisher's ]
[6] Gergö Barany. A more precise, more correct stack and register model for CompCert. In LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018, Oxford, United Kingdom, July 2018. [ bib | HAL archive ]
[7] Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In ESOP 2018: Programming Languages and Systems - 27th European Symposium on Programming, volume 10801 of Lecture Notes in Computer Science, pages 533--560. Springer, 2018. [ bib | At publisher's ]
[8] Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. In ERTS 2018: Embedded Real Time Software and Systems. SEE, January 2018. [ bib | HAL archive ]
[9] Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener. Embedded program annotations for WCET analysis. In WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, volume 63 of OpenAccess Series in Informatics (OASIcs), pages 8:1--8:13. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, July 2018. [ bib | HAL archive | At publisher's ]

Publications in 2017

Journal articles:
[1] Arthur Charguéraud and François Pottier. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, September 2017. [ bib | DOI | HAL archive ]
[2] Jacques-Henri Jourdan and François Pottier. A simple, possibly correct LR parser for C11. ACM Trans. Program. Lang. Syst., 39(4):14:1--14:36, September 2017. [ bib | HAL archive | At publisher's ]
[3] François Pottier. Visitors unchained. Proc. ACM on Programming Languages, 1(ICFP):28:1--28:28, 2017. [ bib | Local copy | At publisher's ]
Conference papers:
[1] Umut A Acar, Naama Ben-David, and Mike Rainey. Contention in structured concurrency: Provably efficient dynamic non-zero indicators for nested parallelism. In PPoPP 2017: 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, February 2017. [ bib | DOI | HAL archive ]
[2] Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. A formally verified compiler for Lustre. In PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, Spain, June 2017. ACM. [ bib | HAL archive | At publisher's ]
[3] Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL -- A Verified OCAml Library. In ML Family Workshop 2017. ACM, September 2017. [ bib | HAL archive ]
[4] Arthur Charguéraud and François Pottier. Temporary read-only permissions for separation logic. In Hongseok Yang, editor, ESOP 2017: Proceedings of the European Symposium on Programming, volume 10201 of Lecture Notes in Computer Science, pages 260--286. Springer, April 2017. [ bib | HAL archive | Local copy | At publisher's ]
[5] Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. In POPL 2017: 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pages 429--442, January 2017. [ bib | DOI | HAL archive ]
[6] Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, and Christian Ferdinand. Closing the gap -- the formally verified optimizing compiler CompCert. In SSS 2017: Safety-critical Systems Symposium 2017, February 2017. [ bib | HAL archive ]
[7] François Pottier. Verifying a hash table and its iterators in higher-order separation logic. In CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 3--16, January 2017. [ bib | DOI | HAL archive ]
Others:
[1] Xavier Leroy. The CompCert C verified compiler, documentation and user's manual. INRIA, August 2017. [ bib | HAL archive | Local copy ]
[2] 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.06. INRIA, November 2017. [ bib | HAL archive | Local copy ]

Publications in 2016

PhD and habilitation theses:
[1] Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. PhD thesis, Université Paris Diderot (Paris 7), May 2016. [ bib | HAL archive | Local copy ]
[2] Gabriel Scherer. Which types have a unique inhabitant? Focusing on pure program equivalence. PhD thesis, Université Paris Diderot (Paris 7), March 2016. [ bib | HAL archive | Local copy ]
Journal articles:
[1] Umut A Acar, Arthur Charguéraud, and Mike Rainey. Oracle-guided scheduling for controlling granularity in implicitly parallel languages. Journal of Functional Programming, 26, November 2016. [ bib | DOI | HAL archive ]
[2] Thibaut Balabonski, François Pottier, and Jonathan Protzenko. The design and formalization of Mezzo, a permission-based programming language. ACM Transactions on Programming Languages and Systems, 38(4):14:1--14:94, 2016. [ bib | HAL archive | Local copy | At publisher's ]
Conference papers:
[1] Umut Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski. Dag-calculus: A calculus for parallel computation. In ICFP 2016: 21st International Conference on Functional Programming. ACM Press, 2016. [ bib | Local copy ]
[2] Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, and Stephan Merz. Proving determinacy of the PharOS real-time operating system. In ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, volume 9675 of LNCS, pages 70--85. Springer, May 2016. [ bib | DOI | Local copy ]
[3] Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In POPL 2016: ACM Symposium on Principles of Programming Languages. ACM Press, 2016. [ bib | HAL archive ]
[4] Jacques-Henri Jourdan. Sparsity preserving algorithms for octagons. In NSAD 2016: Numerical and symbolic abstract domains workshop , page 14. Elsevier, September 2016. [ bib | HAL archive ]
[5] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. Compcert -- a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016. [ bib | HAL archive | Local copy ]
[6] François Pottier. Reachability and error diagnosis in LR(1) parsers. In CC 2016: 25th International Conference on Compiler Construction, pages 88--98. ACM, 2016. [ bib | At publisher's ]
[7] Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. Transfinite step-indexing: Decoupling concrete and logical steps. In ESOP 2016: Programming Languages and Systems, 25th European Symposium on Programming, volume 9632 of Lecture Notes in Computer Science, pages 727--751. Springer, 2016. [ bib | At publisher's ]

Publications in 2015

Journal articles:
[1] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified compilation of floating-point computations. Journal of Automated Reasoning, 54(2):135--163, 2015. [ bib | HAL archive | Local copy | At publisher's ]
Conference papers:
[1] Pietro Abate, Roberto Di Cosmo, Louis Gesbert, Fabrice Le Fessant, Ralf Treinen, and Stefano Zacchiroli. Mining component repositories for installability issues. In MSR: 12th IEEE/ACM Working Conference on Mining Software Repositories, pages 24--33. IEEE, 2015. [ bib | At publisher's ]
[2] Umut Acar, Arthur Charguéraud, and Mike Rainey. A work-efficient algorithm for parallel unordered depth-first search. In SC 2015: International Conference for High Performance Computing, Networking, Storage and Analysis, pages 67:1--67:12. ACM, November 2015. [ bib | At publisher's ]
[3] Çagdas Bozman, Grégoire Henry, Mohamed Iguernelala, Fabrice Le Fessant, and Michel Mauny. ocp-memprof: un profileur mémoire pour OCaml. In David Baelde and Jade Alglave, editors, JFLA 2015: Vingt-sixièmes journées francophones des langages applicatifs, Le Val d'Ajol, France, January 2015. [ bib | HAL archive ]
[4] Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, and Olivier Hermant. Automated deduction in the B set theory using typed proof search and deduction modulo. In LPAR 2015: 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 9450 of Lecture Notes in Computer Science. Springer, November 2015. [ bib | HAL archive ]
[5] Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In ITP 2015: 6th conference on Interactive Theorem Proving, volume 9236 of Lecture Notes in Computer Science, pages 137--153. Springer, 2015. [ bib | Local copy | At publisher's ]
[6] Pierre-Évariste Dagand and Gabriel Scherer. Normalization by realizability also evaluates. In David Baelde and Jade Alglave, editors, JFLA 2015: Vingt-sixièmes Journées Francophones des Langages Applicatifs, Le Val d'Ajol, France, January 2015. [ bib | HAL archive ]
[7] Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Micro-policies: Formally verified, tag-based security monitors. In SP 2015: IEEE Symposium on Security and Privacy, pages 813--830. IEEE Computer Society, 2015. [ bib | At publisher's ]
[8] Damien Doligez, Christèle Faure, Thérèse Hardin, and Manuel Maarek. Avoiding security pitfalls with functional programming: A report on the development of a secure XML validator. In ICSE 2015: 37th IEEE/ACM International Conference on Software Engineering, pages 209--218. IEEE, April 2015. [ bib | At publisher's ]
[9] 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, pages 247--259. ACM Press, January 2015. [ bib | HAL archive | Local copy | At publisher's ]
[10] Guillaume Munch-Maccagnoni and Gabriel Scherer. Polarised intermediate representation of lambda calculus with sums. In LICS 2015: 30th Symposium on Logic In Computer Science, pages 127--140. IEEE Computer Society Press, 2015. [ bib | HAL archive | At publisher's ]
[11] Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational property-based testing. In ITP 2015: 6th conference on Interactive Theorem Proving, volume 9236 of Lecture Notes in Computer Science, pages 325--343. Springer, 2015. [ bib | HAL archive | At publisher's ]
[12] François Pottier and Jonathan Protzenko. A few lessons from the Mezzo project. In SNAPL 2015: 1st Summit on Advances in Programming Languages, volume 32 of LIPIcs, pages 221--237. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2015. [ bib | At publisher's ]
[13] François Pottier. Depth-first search and strong connectivity in Coq. In David Baelde and Jade Alglave, editors, JFLA 2015: Vingt-sixièmes journées francophones des langages applicatifs, Le Val d'Ajol, France, January 2015. [ bib | HAL archive ]
[14] Gabriel Scherer. Multi-focusing on extensional rewriting with sums. In TLCA 2015: 13th International Conference on Typed Lambda Calculi and Applications, volume 38 of LIPIcs, pages 317--331. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2015. [ bib | At publisher's ]
[15] Gabriel Scherer and Didier Rémy. Full reduction in the face of absurdity. In ESOP 2015: Programming Languages and Systems, 24th European Symposium on Programming, volume 9032 of Lecture Notes in Computer Science, pages 685--709. Springer, 2015. [ bib | HAL archive | At publisher's ]
[16] Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? In ICFP'15: 20th International Conference on Functional Programming, pages 243--255. ACM Press, 2015. [ bib | At publisher's ]

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 | HAL archive | 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] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. Journal of Automated Reasoning, 53(3):271--304, 2014. [ bib | HAL archive | At publisher's ]
[3] 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 Algorithms, ESA 2014, volume 8737 of Lecture Notes in Computer Science, pages 25--36. Springer, 2014. [ bib | HAL archive | 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 | HAL archive | Local copy ]
[5] Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. In JFLA'14: Journées Francophones des Langages Applicatifs, Fréjus, France, January 2014. [ bib | HAL archive ]
[6] 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 | HAL archive | At publisher's ]
[7] 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 ]
[8] 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 ]
[9] 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 ]
[10] 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 ]
[11] 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] Umut A. Acar, Arthur Charguéraud, and Mike Rainey. Data Structures and Algorithms for Robust and Fast Parallel Graph Search. Technical report, Inria, December 2014. [ bib | HAL archive ]
[2] 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] 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 | HAL archive | 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-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 ]
[7] 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 ]
[8] Jonathan Protzenko and François Pottier. Programming with permissions: the Mezzo language. In ACM SIGPLAN Workshop on ML, 2012. [ bib | HAL archive | Local copy ]
[9] 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 ]
[10] 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 ]
[11] Gabriel Scherer and Didier Rémy. GADTs meet subtyping. In ACM SIGPLAN Workshop on ML, 2012. [ bib | HAL archive | Local copy ]
[12] 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 ]
[13] 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 | HAL archive | 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. 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 | HAL archive | 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 ]