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
  • 2T. Balabonski, F. Pottier, J. Protzenko.

    The design and formalization of Mezzo, a permission-based programming language, in: ACM Transactions on Programming Languages and Systems, 2016, vol. 38, no 4, pp. 14:1–14:94.

    http://doi.acm.org/10.1145/2837022
  • 3A. Charguéraud, F. Pottier.

    Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits, in: Journal of Automated Reasoning, September 2017. [ DOI : 10.1007/s10817-017-9431-7 ]

    https://hal.inria.fr/hal-01652785
  • 4K. 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
  • 5J. 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
  • 6J.-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
  • 7D. 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
  • 8X. 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
  • 9X. 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
  • 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

Articles in International Peer-Reviewed Journals

  • 11A. Charguéraud, F. Pottier.

    Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits, in: Journal of Automated Reasoning, September 2017. [ DOI : 10.1007/s10817-017-9431-7 ]

    https://hal.inria.fr/hal-01652785
  • 12J.-H. Jourdan, F. Pottier.

    A Simple, Possibly Correct LR Parser for C11, in: ACM Transactions on Programming Languages and Systems (TOPLAS), September 2017, vol. 39, no 4, pp. 1 - 36. [ DOI : 10.1145/3064848 ]

    https://hal.archives-ouvertes.fr/hal-01633123
  • 13F. Pottier.

    Visitors unchained, in: Proceedings of the ACM on Programming Languages, August 2017, vol. 1, no ICFP, pp. 1 - 28. [ DOI : 10.1145/3110272 ]

    https://hal.inria.fr/hal-01670735
  • 14T. Williams, D. Rémy.

    A Principled Approach to Ornamentation in ML, in: Proceedings of the ACM on Programming Languages, January 2018, pp. 1-30. [ DOI : 10.1145/3158109 ]

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

International Conferences with Proceedings

  • 15U. A. Acar, V. Aksenov, S. Westrick.

    Brief Announcement: Parallel Dynamic Tree Contraction via Self-Adjusting Computation, in: The 29th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA '17), Washington, United States, July 2017. [ DOI : 10.1145/3087556.3087595 ]

    https://hal.inria.fr/hal-01664903
  • 16U. 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
  • 17V. Aksenov, V. Gramoli, P. Kuznetsov, A. Malova, S. Ravi.

    A Concurrency-Optimal Binary Search Tree, in: 23rd International European Conference on Parallel and Distributed Computing - Euro-Par 2017, Santiago de Compostella, Spain, August 2017, https://arxiv.org/abs/1702.04441.

    https://hal.inria.fr/hal-01664898
  • 18T. Balabonski, P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain.

    Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems, in: Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Turin, Italy, Lecture Notes in Computer Science, Springer, September 2017, vol. 10471, pp. 165-181. [ DOI : 10.1007/978-3-319-67113-0_11 ]

    http://hal.upmc.fr/hal-01549942
  • 19G. Barany, J. Signoles.

    Hybrid Information Flow Analysis for Real-World C Code, in: TAP 2017 - 11th International Conference on Tests & Proofs, Marburg, Germany, Springer, July 2017, vol. 10375, pp. 23-40. [ DOI : 10.1007/978-3-319-61467-0_2 ]

    https://hal.inria.fr/hal-01658653
  • 20T. Bourke, L. Brun, P.-E. Dagand, X. Leroy, M. Pouzet, L. Rieg.

    A Formally Verified Compiler for Lustre, in: PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelone, Spain, ACM, June 2017.

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

    Temporary Read-Only Permissions for Separation Logic, in: Proceedings of the 26th European Symposium on Programming (ESOP 2017), Uppsala, Sweden, April 2017.

    https://hal.inria.fr/hal-01408657
  • 22S. 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
  • 23D. Kästner, J. Barrho, U. Wünsche, M. Schlickling, B. Schommer, M. Schmidt, C. Ferdinand, X. Leroy, S. Blazy.

    CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler, in: ERTS2 2018 - Embedded Real Time Software and Systems, Toulouse, France, 3AF, SEE, SIE, January 2018.

    https://hal.inria.fr/hal-01643290
  • 24D. 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, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium, CreateSpace, February 2017, pp. 163-180.

    https://hal.inria.fr/hal-01399482
  • 25F. 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
  • 26M. Raab, G. Barany.

    Challenges in Validating FLOSS Conguration, in: OSS 2017 - The 13th International Conference on Open Source Systems, Buenos Aires, Argentina, OSS 2017: Open Source Systems: Towards Robust Practices, Springer, May 2017, vol. 496, pp. 101-114. [ DOI : 10.1007/978-3-319-57735-7_11 ]

    https://hal.inria.fr/hal-01658595
  • 27M. Raab, G. Barany.

    Introducing Context Awareness in Unmodified, Context-unaware Software, in: ENASE 2017 - 12th International Conference on Evaluation of Novel Approaches to Software Engineering, Porto, Portugal, April 2017, pp. 1-8.

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

Internal Reports

Scientific Popularization

Other Publications

References in notes
  • 38U. A. Acar, A. Charguéraud, M. Rainey.

    , Theory and Practice of Chunked SequencesA. S. Schulz, D. Wagner (editors), Springer Berlin Heidelberg, Berlin, Heidelberg, 2014, pp. 25–36.

    https://doi.org/10.1007/978-3-662-44777-2_3
  • 39U. 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
  • 40F. 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
  • 41V. 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
  • 42F. 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, PODC '07, 2007, pp. 13–22.
  • 43H. 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
  • 44L. 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
  • 45X. 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/
  • 46X. 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
  • 47B. C. Pierce.

    Types and Programming Languages, MIT Press, 2002.
  • 48F. 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
  • 49F. 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
  • 50D. 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


previous Previous | up Home