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 p.

    http://dx.doi.org/10.1145/2603088.2603128
  • 4J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, D. Pichardie.

    A Formally-Verified C Static Analyzer, in: POPL'15: 42nd ACM Symposium on Principles of Programming Languages, ACM Press, January 2015, pp. 247-259.

    http://dx.doi.org/10.1145/2676726.2676966
  • 5D. 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
  • 6X. 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
  • 7X. 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
  • 8F. 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
  • 9F. 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
  • 10N. 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
Publications of the year

Doctoral Dissertations and Habilitation Theses

Articles in International Peer-Reviewed Journals

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

    Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages, in: Journal of Functional Programming, November 2016, vol. 26. [ DOI : 10.1017/S0956796816000101 ]

    https://hal.inria.fr/hal-01409069
  • 14T. 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), August 2016, vol. 38, no 4, 94 p. [ DOI : 10.1145/2837022 ]

    https://hal.inria.fr/hal-01246534
  • 15M.-K. Riviere, J.-H. Jourdan, S. Zohar.

    dfcomb: An R-package for phase I/II trials of drug combinations, in: Computer Methods and Programs in Biomedicine, 2016, vol. 125, pp. 117–133. [ DOI : 10.1016/j.cmpb.2015.10.018 ]

    http://hal.upmc.fr/hal-01297367
  • 16M.-K. Riviere, Y. Yuan, J.-H. Jourdan, F. Dubois, S. Zohar.

    Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization, in: Statistical Methods in Medical Research, March 2016. [ DOI : 10.1177/0962280216631763 ]

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

International Conferences with Proceedings

  • 17U. A. Acar, N. Ben-David, M. Rainey.

    Contention in Structured Concurrency: Provably Efficient Dynamic Non-Zero Indicators for Nested Parallelism, in: 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Austin, United States, February 2017. [ DOI : 10.1145/3018743.3018762 ]

    https://hal.inria.fr/hal-01416531
  • 18U. A. Acar, A. Charguéraud, M. Rainey, F. Sieczkowski.

    Dag-calculus: a calculus for parallel computation, in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Nara, Japan, September 2016, pp. 18 - 32. [ DOI : 10.1145/2951913.2951946 ]

    https://hal.inria.fr/hal-01409022
  • 19D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy.

    Dijkstra Monads for Free, in: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Unknown, Unknown or Invalid Region, ACM, 2017, pp. 515-529.

    https://hal.archives-ouvertes.fr/hal-01424794
  • 20S. Azaiez, D. Doligez, M. Lemerre, T. Libal, S. Merz.

    Proving Determinacy of the PharOS Real-Time Operating System, in: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, M. J. Butler, K.-D. Schewe, A. Mashkoor, M. Biró (editors), LNCS - Lecture Notes in Computer Science, Springer, May 2016, vol. 9675, pp. 70-85. [ DOI : 10.1007/978-3-319-33600-8_4 ]

    https://hal.inria.fr/hal-01322335
  • 21F. Balestrieri, M. Mauny.

    Generic Programming in OCaml, in: OCaml 2016 - The OCaml Users and Developers Workshop, Nara, Japan, September 2016.

    https://hal.inria.fr/hal-01413061
  • 22S. 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
  • 23S. Flur, S. Sarkar, C. Pulte, K. Nienhuis, L. Maranget, K. E. Gray, A. Sezgin, M. Batty, P. Sewell.

    Mixed-size Concurrency: ARM, POWER, C/C++11, and SC, in: 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), Paris, France, ACM, January 2017.

    https://hal.inria.fr/hal-01413221
  • 24J.-H. Jourdan.

    Sparsity Preserving Algorithms for Octagons, in: NSAD 2016 - Numerical and symbolic abstract domains workshop, Edinburgh, United Kingdom, I. Mastroeni (editor), Elsevier, September 2016, 14 p.

    https://hal.inria.fr/hal-01406795
  • 25D. Kästner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt, C. Ferdinand.

    Closing the Gap – The Formally Verified Optimizing Compiler CompCert, in: SSS'17: Safety-critical Systems Symposium 2017, Bristol, United Kingdom, Proceedings of the Twenty-fifth Safety-Critical Systems Symposium, February 2017.

    https://hal.inria.fr/hal-01399482
  • 26F. Pottier.

    Reachability and Error Diagnosis in LR(1) Parsers, in: CC 2016 - 25th International Conference on Compiler Construction, Barcelone, Spain, Proceedings of the 25th International Conference on Compiler Construction (CC 2016), March 2016, 11 p. [ DOI : 10.1145/2892208.2892224 ]

    https://hal.inria.fr/hal-01417004
  • 27F. Pottier.

    Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic, in: Certified Programs and Proofs, Paris, France, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), January 2017.

    https://hal.inria.fr/hal-01417102
  • 28R. A. Raghunathan, S. A. Muller, U. A. Acar, G. A. Blelloch.

    Hierarchical Memory Management for Parallel Programs, in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, Nara, Japan, September 2016. [ DOI : 10.1145/3022670.2951935 ]

    https://hal.inria.fr/hal-01416237
  • 29K. Svendsen, F. Sieczkowski, L. Birkedal.

    Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, in: 25th European Symposium on Programming Languages and Systems, Eindhoven, Netherlands, December 2016, vol. 9632, pp. 727 - 751. [ DOI : 10.1007/978-3-662-49498-1_28 ]

    https://hal.inria.fr/hal-01408649
  • 30B. Vaugon, M. Mauny.

    A Type Inference System Based on Saturation of Subtyping Constraints, in: Trends in Functional Programming, College Park (MD), United States, June 2016.

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

National Conferences with Proceedings

  • 31F. 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

  • 32Ç. Bozman, T. Huffschmitt, M. Laporte, F. Le Fessant.

    ocp-lint, A Plugin-based Style-Checker with Semantic Patches, in: OCaml Users and Developers Workshop 2016, Nara, Japan, September 2016.

    https://hal.inria.fr/hal-01352013
  • 33B. Canou, G. Henry, Ç. Bozman, F. Le Fessant.

    Learn OCaml, An Online Learning Center for OCaml, in: OCaml Users and Developers Workshop 2016, Nara, Japan, September 2016.

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

    A Certified Universal Gathering Algorithm for Oblivious Mobile Robots, in: Distributed Computing (DISC), Paris, France, September 2016.

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

    Certified Universal Gathering in R2 for Oblivious Mobile Robots, in: ACM Conference on Principles of Distributed Computing (PODC), Chicago, United States, ACM, July 2016.

    http://hal.upmc.fr/hal-01349084
  • 36J.-H. Jourdan.

    Statistically profiling memory in OCaml, in: OCaml 2016, Nara, Japan, September 2016.

    https://hal.inria.fr/hal-01406809
  • 37F. Le Fessant.

    OPAM-builder: Continuous Monitoring of OPAM Repositories, in: OCaml Users and Developers Workshop 2016, Nara, Japan, September 2016.

    https://hal.inria.fr/hal-01352008
  • 38X. 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
  • 39G. Scherer, L. Maranget, T. Réfis.

    Ambiguous pattern variables, in: OCaml 2016: The OCaml Users and Developers Workshop, Nara, Japan, September 2016, 2 p.

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

Internal Reports

  • 40X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy, J. Vouillon.

    The OCaml system release 4.04: Documentation and user's manual, Inria, November 2016.

    https://hal.inria.fr/hal-00930213
  • 41X. Leroy.

    The CompCert C verified compiler: Documentation and user’s manual: Version 2.7, Inria, June 2016.

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

Other Publications

References in notes
  • 43V. Benzaken, G. Castagna, A. Frisch.

    CDuce: an XML-centric general-purpose language, in: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, C. Runciman, O. Shivers (editors), ACM, 2003, pp. 51–63.

    https://www.lri.fr/~benzaken/papers/icfp03.ps
  • 44F. Ellen, Y. Lev, V. Luchangco, M. Moir.

    SNZI: Scalable NonZero Indicators, in: Proceedings of the Twenty-sixth Annual ACM Symposium on Principles of Distributed Computing, 2007, pp. 13–22.

    http://dl.acm.org/citation.cfm?id=1281106
  • 45P. Halmagrand.

    Automated Deduction and Proof Certification for the B Method, Conservatoire National des Arts et Métiers, December 2016.
  • 46H. Hosoya, B. C. Pierce.

    XDuce: A Statically Typed XML Processing Language, in: ACM Transactions on Internet Technology, 2003, vol. 3, no 2, pp. 117–148.

    http://doi.acm.org/10.1145/767193.767195
  • 47J. Kang, Y. Kim, C. Hur, D. Dreyer, V. Vafeiadis.

    Lightweight verification of separate compilation, in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, pp. 178–190.

    http://doi.acm.org/10.1145/2837614.2837642
  • 48L. Lamport.

    How to write a 21st century proof, in: Journal of Fixed Point Theory and Applications, 2012, vol. 11, pp. 43–63.

    http://dx.doi.org/10.1007/s11784-012-0071-6
  • 49X. Leroy, D. Doligez, J. Garrigue, D. Rémy, J. Vouillon.

    The Objective Caml system, documentation and user's manual – release 4.02, Inria, August 2014.

    http://caml.inria.fr/pub/docs/manual-ocaml-4.02/
  • 50X. Leroy.

    Java bytecode verification: algorithms and formalizations, in: Journal of Automated Reasoning, 2003, vol. 30, no 3–4, pp. 235–269.

    http://dx.doi.org/10.1023/A:1025055424017
  • 51X. 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, ACM Press, 2006, pp. 42–54.

    http://doi.acm.org/10.1145/1111037.1111042
  • 52B. C. Pierce.

    Types and Programming Languages, MIT Press, 2002.
  • 53F. Pottier.

    Simplifying subtyping constraints: a theory, in: Information and Computation, 2001, vol. 170, no 2, pp. 153–183.

    http://gallium.inria.fr/~fpottier/publis/fpottier-ic01.ps.gz
  • 54F. Pottier, V. Simonet.

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

    http://dx.doi.org/10.1145/596980.596983
  • 55D. Rémy, J. Vouillon.

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

    http://gallium.inria.fr/~remy/ftp/objective-ml!popl97.pdf
  • 56G. Scherer, D. Rémy.

    Which simple types have a unique inhabitant?, in: ICFP'15: 20th International Conference on Functional Programming, ACM Press, 2015, pp. 243–255.

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


previous Previous | up Home