EN FR
EN FR


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1J. Alglave, L. Maranget, M. Tautschnig.

    Herding cats: modelling, simulation, testing, and data-mining for weak memory, in: ACM Transactions on Programming Languages and Systems, 2014, vol. 36, no 2, article no 7 p.

    http://dx.doi.org/10.1145/2627752
  • 2K. Chaudhuri, D. Doligez, L. Lamport, S. Merz.

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

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

    System F with Coercion Constraints, in: CSL-LICS 2014: Computer Science Logic / Logic In Computer Science, ACM, 2014, article no 34.

    http://dx.doi.org/10.1145/2603088.2603128
  • 4D. Le Botlan, D. Rémy.

    Recasting MLF, in: Information and Computation, 2009, vol. 207, no 6, pp. 726–785.

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

    A formally verified compiler back-end, in: Journal of Automated Reasoning, 2009, vol. 43, no 4, pp. 363–446.

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

    Formal verification of a realistic compiler, in: Communications of the ACM, 2009, vol. 52, no 7, pp. 107–115.

    http://doi.acm.org/10.1145/1538788.1538814
  • 7F. Pottier.

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

    http://dx.doi.org/10.1109/LICS.2008.16
  • 8F. Pottier, J. Protzenko.

    Programming with permissions in Mezzo, in: Proceedings of the 18th International Conference on Functional Programming (ICFP 2013), ACM Press, 2013, pp. 173–184.

    http://dx.doi.org/10.1145/2500365.2500598
  • 9N. Pouillard, F. Pottier.

    A unified treatment of syntax with binders, in: Journal of Functional Programming, 2012, vol. 22, no 4–5, pp. 614–704.

    http://dx.doi.org/10.1017/S0956796812000251
  • 10J.-B. Tristan, X. Leroy.

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

    http://doi.acm.org/10.1145/1706299.1706311
Publications of the year

Articles in International Peer-Reviewed Journals

  • 11T. Balabonski, F. Pottier, J. Protzenko.

    The Design and Formalization of Mezzo, a Permission-Based Programming Language, in: ACM Transactions on Programming Languages and Systems (TOPLAS), 2016. [ DOI : 10.1145/2837022 ]

    https://hal.inria.fr/hal-01246534
  • 12S. Boldo, J.-H. Jourdan, X. Leroy, G. Melquiond.

    Verified Compilation of Floating-Point Computations, in: Journal of Automated Reasoning, February 2015, vol. 54, no 2, pp. 135-163. [ DOI : 10.1007/s10817-014-9317-x ]

    https://hal.inria.fr/hal-00862689
  • 13B. Bérard, P. Courtieu, L. Millet, M. Potop-Butucaru, L. Rieg, N. Sznajder, S. Tixeuil, X. Urbain.

    [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems, in: International Journal of Informatics Society, 2015, vol. 7, no 3, pp. 101-114.

    http://hal.upmc.fr/hal-01238784
  • 14P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain.

    Impossibility of gathering, a certification, in: Information Processing Letters, March 2015, vol. 115, no 3, pp. 447-452. [ DOI : 10.1016/j.ipl.2014.11.001 ]

    http://hal.upmc.fr/hal-01122869

International Conferences with Proceedings

  • 15U. A. Acar, A. Charguéraud, M. Rainey.

    A Work-Efficient Algorithm for Parallel Unordered Depth-First Search, in: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Austin, Texas, United States, November 2015. [ DOI : 10.1145/2807591.2807651 ]

    https://hal.inria.fr/hal-01245837
  • 16P. Bhatotia, P. Fonseca, U. A. Acar, B. Björn, R. Rodrigues.

    iThreads: A Threading Library for Parallel Incremental Computation, in: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, Istanbul, Turkey, ACM, March 2015, pp. 645–659. [ DOI : 10.1145/2694344.2694371 ]

    https://hal.inria.fr/hal-01245884
  • 17A. Charguéraud, F. Pottier.

    Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, in: 6th International Conference on Interactive Theorem Proving (ITP), Nanjing, China, August 2015. [ DOI : 10.1007/978-3-319-22102-1_9 ]

    https://hal.inria.fr/hal-01245872
  • 18S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin, L. Maranget, W. Deacon, P. Sewell.

    Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA, in: Principles of Programming Languages 2016 (POPL 2016), Saint Petersburg, United States, January 2016.

    https://hal.inria.fr/hal-01244776
  • 19J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, D. Pichardie.

    A formally-verified C static analyzer, in: POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, ACM, January 2015, pp. 247-259. [ DOI : 10.1145/2676726.2676966 ]

    https://hal.inria.fr/hal-01078386
  • 20Z. Paraskevopoulou, C. Hriţcu, M. Dénès, L. Lampropoulos, B. C. Pierce.

    Foundational Property-Based Testing, in: ITP 2015 - 6th conference on Interactive Theorem Proving, Nanjing, China, Lecture Notes in Computer Science, Springer, August 2015, vol. 9236. [ DOI : 10.1007/978-3-319-22102-1_22 ]

    https://hal.inria.fr/hal-01162898
  • 21F. Pottier, J. Protzenko.

    A few lessons from the Mezzo project, in: Summit oN Advances in Programming Languages (SNAPL), Asilomar, United States, Leibniz International Proceedings in Informatics, May 2015, vol. 32. [ DOI : 10.4230/LIPIcs.SNAPL.2015.221 ]

    https://hal.inria.fr/hal-01246360
  • 22G. Scherer, D. Rémy.

    Full reduction in the face of absurdity, in: ESOP'2015: European Conference on Programming Languages and Systems, London, United Kingdom, April 2015.

    https://hal.inria.fr/hal-01095390
  • 23G. Scherer, D. Rémy.

    Which simple types have a unique inhabitant?, in: The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Vancouver, Canada, August 2015.

    https://hal.inria.fr/hal-01235596
  • 24G. Scherer.

    Multi-focusing on extensional rewriting with sums, in: Typed Lambda Calculi and Applications, Warsaw, Poland, June 2015.

    https://hal.inria.fr/hal-01235372
  • 25E. Çiçek, D. Garg, U. Acar.

    Refinement Types for Incremental Computational Complexity, in: 24th European Symposium on Programming (ESOP), London, United Kingdom, April 2015, vol. 9032, pp. 406-431. [ DOI : 10.1007/978-3-662-46669-8_17 ]

    https://hal.inria.fr/hal-01245888

National Conferences with Proceedings

  • 26Ç. Bozman, G. Henry, M. Iguernelala, F. Le Fessant, M. Mauny.

    ocp-memprof: un profileur mémoire pour OCaml, in: Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Le Val d'Ajol, France, D. Baelde, J. Alglave (editors), January 2015.

    https://hal.inria.fr/hal-01099134
  • 27P.-É. Dagand, G. Scherer.

    Normalization by realizability also evaluates, in: Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Le Val d'Ajol, France, D. Baelde, J. Alglave (editors), January 2015.

    https://hal.inria.fr/hal-01099138
  • 28F. Pottier.

    Depth-First Search and Strong Connectivity in Coq, in: Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Le Val d'Ajol, France, D. Baelde, J. Alglave (editors), January 2015.

    https://hal.inria.fr/hal-01096354
  • 29F. Pottier.

    Reachability and error diagnosis in LR(1) automata, in: Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016.

    https://hal.inria.fr/hal-01248101

Conferences without Proceedings

  • 30G. Bury, D. Delahaye, D. Doligez, P. Halmagrand, O. Hermant.

    Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo, in: LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Suva, Fiji, November 2015.

    https://hal-mines-paristech.archives-ouvertes.fr/hal-01204701
  • 31P. Chambart, M. Laporte, V. Bernardoff, F. Le Fessant.

    Operf: Benchmarking the OCaml Compiler, in: OCaml Users and Developers Workshop, Vancouver, Canada, September 2015.

    https://hal.inria.fr/hal-01245844
  • 32X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister, C. Ferdinand.

    CompCert - A Formally Verified Optimizing Compiler, in: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Toulouse, France, SEE, January 2016.

    https://hal.inria.fr/hal-01238879
  • 33G. Munch-Maccagnoni, G. Scherer.

    Polarised Intermediate Representation of Lambda Calculus with Sums, in: Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015), Kyoto, Japan, July 2015, Dec. 2015: see the added footnote on page 7. [ DOI : 10.1109/LICS.2015.22 ]

    https://hal.inria.fr/hal-01160579

Scientific Books (or Scientific Book chapters)

Internal Reports

  • 35U. A. Acar, A. Charguéraud, M. Rainey.

    Fast Parallel Graph-Search with Splittable and Catenable Frontiers, Inria, January 2015.

    https://hal.inria.fr/hal-01089125
  • 36P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain.

    A Certified Universal Gathering Algorithm for Oblivious Mobile Robots, UPMC, Sorbonne Universites CNRS ; CNAM, Paris ; College de France ; Université Paris Sud, June 2015.

    http://hal.upmc.fr/hal-01159890
  • 37X. Leroy.

    The CompCert C verified compiler: Documentation and user’s manual, Inria, December 2015.

    https://hal.inria.fr/hal-01091802
References in notes


previous Previous | up Home