2024
Journal articles
- auteur
- Alexandre Moine, Sam Westrick, Stephanie Balzer
- titre
- DisLog: A Separation Logic for Disentanglement
- article
- Proceedings of the ACM on Programming Languages, 2024, 8 (POPL), ⟨10.1145/3632853⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Clément Allain, Gabriel Scherer
- titre
- Correct tout seul, sûr à plusieurs
- article
- JFLA 2024 – 35es Journ´ees Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
- auteur
- Milla Valnet, Nathanaëlle Courant, Guillaume Bury, Pierre Chambart, Vincent Laviron
- titre
- Chamelon : un minimiseur pour et en OCaml
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Well-founded recursion done right
- article
- CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, ACM, Jan 2024, London, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
- titre
- Thunks and Debits in Separation Logic with Time Credits
- article
- POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Correct, Fast LR(1) Unparsing
- article
- 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
2023
Journal articles
- auteur
- Paulo Emílio de Vilhena, François Pottier
- titre
- Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
- article
- Logical Methods in Computer Science, 2023, 19 (4), pp.51. ⟨10.46298/lmcs-19(4:5)2023⟩
- Accès au texte intégral et bibtex
-
- auteur
- Andrew W Appel, Xavier Leroy
- titre
- Efficient Extensional Binary Tries
- article
- Journal of Automated Reasoning, 2023, 67, pp.Article number 8. ⟨10.1007/s10817-022-09655-x⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexandre Moine, Arthur Charguéraud, François Pottier
- titre
- A High-Level Separation Logic for Heap Space under Garbage Collection (Extended Version)
- article
- Proceedings of the ACM on Programming Languages, 2023, 7 (POPL), pp.718-747. ⟨10.1145/3571218⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Paulo Emílio de Vilhena, François Pottier
- titre
- A Type System for Effect Handlers and Dynamic Labels
- article
- European Symposium on Programming, Apr 2023, Paris, France. pp.225-252, ⟨10.1007/978-3-031-30044-8_9⟩
- Accès au texte intégral et bibtex
-
- auteur
- Clément Blaudeau, Didier Rémy, Gabriel Radanne
- titre
- Retrofitting OCaml modules
- article
- JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.59-100
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, Kc Sivaramakrishnan, Jérôme Vouillon
- titre
- The OCaml system release 5.1: Documentation and user's manual
- article
- [Intern report] Inria. 2023
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- The CompCert C verified compiler: Documentation and user’s manual
- article
- [Intern report] Inria. 2023, pp.1-79
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
- titre
- Verified Extraction from Coq to OCaml
- article
- 2023
- Accès au texte intégral et bibtex
-
2022
Journal articles
- auteur
- Clément Blaudeau, Fengyun Liu
- titre
- A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model
- article
- Proceedings of the ACM on Programming Languages, 2022, 6 (OOPSLA2), pp.729-757. ⟨10.1145/3563314⟩
- Accès au bibtex
-
- auteur
- Xavier Leroy
- titre
- Sciences du logiciel
- article
- L'Annuaire du Collège de France. Résumés des cours et travaux, 2022, 119, pp.21-33. ⟨10.4000/annuaire-cdf.16737⟩
- Accès au texte intégral et bibtex
-
- auteur
- Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer
- titre
- Debootstrapping without Archeology
- article
- The Art, Science, and Engineering of Programming, 2022, 6 (3), ⟨10.22152/programming-journal.org/2022/6/13⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jean-Marie Madiot, François Pottier
- titre
- A Separation Logic for Heap Space under Garbage Collection
- article
- Proceedings of the ACM on Programming Languages, 2022, ⟨10.1145/3498672⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Basile Clément, Albert Cohen
- titre
- End-to-End Translation Validation for the Halide Language
- article
- OOPSLA 2022 - Conference on Object-Oriented Programming Systems, Languages, and Applications, Dec 2022, Auckland, New Zealand. ⟨10.1145/3527328⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Nathanaëlle Courant
- titre
- An OCaml use case for strong call-by-need reduction
- article
- ACM SIGPLAN Workshop on ML 2022 - ML Family Workshop, Benoit Montagu, Sep 2022, Ljubljana, Slovenia
- Accès au texte intégral et bibtex
-
- auteur
- Alexandre Moine, Arthur Charguéraud, François Pottier
- titre
- Specification and Verification of a Transient Stack
- article
- CPP 2022 - 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503677⟩
- Accès au texte intégral et bibtex
-
- auteur
- Azalea Raad, Luc Maranget, Viktor Vafeiadis
- titre
- Extending Intel-x86 Consistency and Persistency
- article
- POPL 2022 - Symposium on Principles of Programming Languages, Jan 2022, Philadelphia, United States. ⟨10.1145/3498683⟩
- Accès au texte intégral et bibtex
-
Books
- auteur
- Chantal Keller, Timothy Bourke, Sandrine Blazy, Frédéric Bour, Guillaume Bury, Stefania Dumbrava, Diane Gallois-Wong, Adrien Guatto, David Janin, Marie Kerjean, Luc Pellissier, Mário Pereira, Alix Trieu, Yannick Zakowski
- titre
- 33èmes journées francophones des langages applicatifs
- article
- Chantal Keller; Timothy Bourke. , pp.1-292, 2022
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Paulo Emílio de Vilhena
- titre
- Proof of Programs with Effect Handlers
- article
- Computation and Language [cs.CL]. Université Paris Cité, 2022. English. ⟨NNT : 2022UNIP7133⟩
- Accès au texte intégral et bibtex
-
- auteur
- Basile Clément
- titre
- Translation Validation of Tensor Compilers
- article
- Computer Science [cs]. École Normale Supérieure (Paris), 2022. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal
- titre
- Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic
- article
- 2022
- Accès au bibtex
-
2021
Journal articles
- auteur
- Jean-Marie Madiot, Damien Pous, Davide Sangiorgi
- titre
- Modular coinduction up-to for higher-order languages via first-order transition systems
- article
- Logical Methods in Computer Science, 2021, Volume 17, Issue 3, ⟨10.46298/lmcs-17(3:25)2021⟩
- Accès au bibtex
-
- auteur
- Jade Alglave, Will Deacon, Richard Grisenthwaite, Antoine Hacquard, Luc Maranget
- titre
- Armed Cats: formal concurrency modelling at Arm
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2021, 43, pp.1 - 54. ⟨10.1145/3458926⟩
- Accès au texte intégral et bibtex
-
- auteur
- Paulo Emílio de Vilhena, François Pottier
- titre
- A Separation Logic for Effect Handlers
- article
- Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), ⟨10.1145/3434314⟩
- Accès au texte intégral et bibtex
-
- auteur
- Nathanaël Courant, Xavier Leroy
- titre
- Verified Code Generation for the Polyhedral Model
- article
- Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.40:1-40:24. ⟨10.1145/3434321⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Frédéric Bour, François Pottier
- titre
- Faster reachability analysis for LR(1) parsers
- article
- SLE 2021 - ACM SIGPLAN International Conference on Software Language Engineering, Oct 2021, Chicago, United States. ⟨10.1145/3486608.3486903⟩
- Accès au texte intégral et bibtex
-
- auteur
- Glen Mével, Jacques-Henri Jourdan
- titre
- Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
- article
- ICFP 2021 - 26th ACM SIGPLAN International Conference on Functional Programming, Aug 2021, Virtual, Japan. ⟨10.1145/3473571⟩
- Accès au texte intégral et bibtex
-
- auteur
- Quentin Ladeveze
- titre
- Mécanisation du modèle RC11 et de la propriété DRF-SC
- article
- JFLA 2021 - 32es Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France
- Accès au texte intégral et bibtex
-
- auteur
- Frédéric Bour, Basile Clément, Gabriel Scherer
- titre
- Tail Modulo Cons
- article
- JFLA 2021 - Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Strong Automated Testing of OCaml Libraries
- article
- JFLA 2021 - 32es Journées Francophones des Langages Applicatifs, Feb 2021, Saint Médard d’Excideuil, France
- Accès au texte intégral et bibtex
-
Master thesis
- auteur
- Clément Blaudeau
- titre
- OCaml modules: formalization, insights and improvements
- article
- Computer Science [cs]. 2021
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Anne Canteaut, Miguel Angel Fernández, Luc Maranget, Sophie Perin, Mario Ricchiuto, Manuel Serrano, Emmanuel Thomé
- titre
- Évaluation des Logiciels
- article
- [Rapport de recherche] Inria. 2021
- Accès au texte intégral et bibtex
-
- auteur
- Anne Canteaut, Miguel Angel Fernández, Luc Maranget, Sophie Perin, Mario Ricchiuto, Manuel Serrano, Emmanuel Thomé
- titre
- Software Evaluation
- article
- [Research Report] Inria. 2021
- Accès au texte intégral et bibtex
-
Software
- auteur
- Alexandre Moine, Arthur Charguéraud, François Pottier
- titre
- Specification and Verification of a Transient Stack (Artifact)
- article
- 2021, ⟨swh:1:dir:80952d7602e8e9614979f1b1f50fdad8a4c369f1;origin=https://hal.archives-ouvertes.fr/hal-03473197;visit=swh:1:snp:781fc4f58efbdfa6ea16006272793bf7c610d760;anchor=swh:1:rel:3df60f40567bfdf2b365cac2fe61c6bb38d94503;path=/⟩
- Accès au texte intégral et bibtex
-
2020
Journal articles
- auteur
- Glen Mével, Jacques-Henri Jourdan, François Pottier
- titre
- Cosmo: A Concurrent Separation Logic for Multicore OCaml
- article
- Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), ⟨10.1145/3408978⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Radanne, Hannes Saffrich, Peter Thiemann
- titre
- Kindly bent to free us
- article
- Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), pp.1-29. ⟨10.1145/3408985⟩
- Accès au texte intégral et bibtex
-
- auteur
- Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan
- titre
- Spy Game: Verifying a Local Generic Solver in Iris
- article
- Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Paulo Emílio de Vilhena, Lawrence C. Paulson
- titre
- Algebraically Closed Fields in Isabelle/HOL
- article
- IJCAR 2020 - International Joint Conference on Automated Reasoning, Jul 2020, Paris, France. pp.204-220, ⟨10.1007/978-3-030-51054-1_12⟩
- Accès au texte intégral et bibtex
-
- auteur
- Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
- titre
- ARMv8-A system semantics: instruction fetch in relaxed architectures
- article
- ESOP 2020 - 29th European Symposium on Programming, Mar 2020, Dublin, Ireland
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Simon Castellan, Léo Stefanesco, Nobuko Yoshida
- titre
- Concurrent Game Semantics: Easy as Pi
- article
- [Research Report] Inria. 2020
- Accès au texte intégral et bibtex
-
2019
Journal articles
- auteur
- Arthur Charguéraud, François Pottier
- titre
- Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
- article
- Journal of Automated Reasoning, 2019, 62 (3), pp.331--365. ⟨10.1007/s10817-017-9431-7⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
- titre
- Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
- article
- Interactive Theorem Proving, Sep 2019, Portland, United States
- Accès au texte intégral et bibtex
-
- auteur
- Glen Mével, Jacques-Henri Jourdan, François Pottier
- titre
- Time Credits and Time Receipts in Iris
- article
- European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩
- Accès au texte intégral et bibtex
-
- auteur
- Umut A Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey
- titre
- Provably and Practically Efficient Granularity Control
- article
- PPoPP 2019 - Principles and Practice of Parallel Programming, Feb 2019, Washington DC, United States. ⟨10.1145/3293883.3295725⟩
- Accès au texte intégral et bibtex
-
Master thesis
- auteur
- Carine Morel
- titre
- Inférence de types et élaboration modulaire avec contraintes pour le langage ML étendu avec des abréviations de types
- article
- Langage de programmation [cs.PL]. 2019
- Accès au texte intégral et bibtex
-
Books
- auteur
- Steve Kremer, Ludovic Mé, Didier Rémy, Vincent Roca
- titre
- Cybersécurité
- article
- Inria, 3, pp.18, 2019, Inria white book
- Accès au texte intégral et bibtex
-
- auteur
- Steve Kremer, Ludovic Mé, Didier Rémy, Vincent Roca
- titre
- Cybersecurity
- article
- Inria, 3, pp.172, 2019, Inria white book
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Armaël Gueneau
- titre
- Mechanized verification of the correctness and asymptotic complexity of programs : the right answer at the right time
- article
- Logic in Computer Science [cs.LO]. Université Paris Cité, 2019. English. ⟨NNT : 2019UNIP7110⟩
- Accès au texte intégral et bibtex
-
- auteur
- Armaël Guéneau
- titre
- Mechanized Verification of the Correctness and Asymptotic Complexity of Programs
- article
- Programming Languages [cs.PL]. Université de Paris, 2019. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2018
Journal articles
- auteur
- Thomas Williams, Didier Rémy
- titre
- A Principled Approach to Ornamentation in ML
- article
- Proceedings of the ACM on Programming Languages, 2018, pp.1-30. ⟨10.1145/3158109⟩
- Accès au texte intégral et bibtex
-
Scientific blog post
- auteur
- Xavier Leroy
- titre
- À la recherche du logiciel parfait
- article
- 2018
- Accès au bibtex
-
Conference papers
- auteur
- Lucas Baudin, Didier Rémy
- titre
- Disornamentation
- article
- ML 2018 - ML Family Workshop, Sep 2018, St. Louis, Missouri, United States
- Accès au bibtex
-
- auteur
- Vitalii Aksenov, Dan Alistarh, Petr Kuznetsov
- titre
- Brief Announcement: Performance Prediction for Coarse-Grained Locking
- article
- PODC 2018 - ACM Symposium on Principles of Distributed Computing, Jul 2018, Egham, United Kingdom. ⟨10.1145/3212734.3212785⟩
- Accès au texte intégral et bibtex
-
- auteur
- Didier Rémy
- titre
- Ornamentation put into Practice in ML
- article
- Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), Jul 2018, Oxford, United Kingdom
- Accès au bibtex
-
- auteur
- Gergö Barany
- titre
- A more precise, more correct stack and register model for CompCert
- article
- LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- auteur
- Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener
- titre
- Embedded Program Annotations for WCET Analysis
- article
- WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩
- Accès au texte intégral et bibtex
-
- auteur
- Umut A Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski
- titre
- Heartbeat scheduling: provable efficiency for nested parallelism
- article
- PLDI’18 - 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2018, Philadelphia, United States. ⟨10.1145/3192366.3192391⟩
- Accès au texte intégral et bibtex
-
- auteur
- Vitalii Aksenov, Petr Kuznetsov, Anatoly Shalyto
- titre
- On Helping and Stacks
- article
- The International Conference on Networked Systems, May 2018, Essaouira, Morocco
- Accès au texte intégral et bibtex
-
- auteur
- Armaël Guéneau, Arthur Charguéraud, François Pottier
- titre
- A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
- article
- ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89884-1_19⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jade Alglave, Luc Maranget, Paul Mckenney, Andrea Parri, Alan Stern
- titre
- Frightening Small Children and Disconcerting Grown-ups
- article
- ASPLOS2018 - 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Mar 2018, Williamsburg, VA, United States. ⟨10.1145/3173162.3177156⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gergö Barany
- titre
- Finding Missed Compiler Optimizations by Differential Testing
- article
- CC'18 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. ⟨10.1145/3178372.3179521⟩
- Accès au texte intégral et bibtex
-
- auteur
- Vitalii Aksenov, Umut A. Acar, Arthur Charguéraud, Mike Rainey
- titre
- Poster: Performance challenges in modular parallel programs
- article
- PPoPP 2018 - 23rd ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, Feb 2018, Vienna, Austria. ⟨10.1145/3178487.3178516⟩
- Accès au texte intégral et bibtex
-
- auteur
- Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, Sandrine Blazy
- titre
- CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler
- article
- ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9
- Accès au texte intégral et bibtex
-
- auteur
- Gergö Barany, Gabriel Scherer
- titre
- Génération aléatoire de programmes guidée par la vivacité
- article
- JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
- Accès au texte intégral et bibtex
-
Book sections
- auteur
- Emmanuel Chailloux, Romain Demangeon, Michel Mauny
- titre
- Typage des langages de programmation
- article
- Techniques de l'ingénieur, ref. article : h3320, Editions T.I., 2018
- Accès au bibtex
-
Documents associated with scientific events
- auteur
- Armaël Guéneau
- titre
- Procrastination: A proof engineering technique
- article
- Coq Workshop 2018, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
Reports
- auteur
- François Pessaux, Damien Doligez
- titre
- Compiling Programs and Proofs: FoCaLiZe Internals
- article
- [Research Report] Ensta ParisTech. 2018
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Vitalii Aksenov
- titre
- Synchronization Costs in Parallel Programs and Concurrent Data Structures
- article
- Distributed, Parallel, and Cluster Computing [cs.DC]. ITMO University; Paris Diderot University, 2018. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2017
Journal articles
- auteur
- Jacques-Henri Jourdan, François Pottier
- titre
- A Simple, Possibly Correct LR Parser for C11
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2017, 39 (4), pp.1 - 36. ⟨10.1145/3064848⟩
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Visitors unchained
- article
- Proceedings of the ACM on Programming Languages, 2017, 1 (ICFP), pp.1 - 28. ⟨10.1145/3110272⟩
- Accès au texte intégral et bibtex
-
Scientific blog post
- auteur
- Xavier Leroy
- titre
- How I found a crash bug with hyperthreading in Intel's Skylake processors
- article
- 2017
- Accès au bibtex
-
Conference papers
- auteur
- Gergö Barany
- titre
- Liveness-Driven Random Program Generation
- article
- Logic-Based Program Synthesis and Transformation. LOPSTR 2017, Oct 2017, Namur, Belgium
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
- titre
- Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems
- article
- Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Sep 2017, Turin, Italy. pp.165-181, ⟨10.1007/978-3-319-67113-0_11⟩
- Accès au bibtex
-
- auteur
- Benjamin Canou, Grégoire Henry, Pierre Chambart, Fabrice Le Fessant, Cagdas Bozman, Vincent Bernardoff, Guillem Rieu, Mohamed Iguernelala, Alain Mebsout, Arthur Breitman
- titre
- Tezos: the OCaml Crypto-Ledger
- article
- OCaml 2017 - OCaml Users and Developers Workshop, Sep 2017, Oxford, United Kingdom. pp.1-2
- Accès au texte intégral et bibtex
-
- auteur
- Didier Rémy
- titre
- Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk)
- article
- the 10th ACM SIGPLAN Symposium on Haskell, Sep 2017, Oxford, France. pp.1-1
- Accès au bibtex
-
- auteur
- Vitalii Aksenov, Vincent Gramoli, Petr Kuznetsov, Anna Malova, Srivatsan Ravi
- titre
- A Concurrency-Optimal Binary Search Tree
- article
- 23rd International European Conference on Parallel and Distributed Computing - Euro-Par 2017, Aug 2017, Santiago de Compostella, Spain
- Accès au bibtex
-
- auteur
- Umut A. Acar, Vitalii Aksenov, Sam Westrick
- titre
- Brief Announcement: Parallel Dynamic Tree Contraction via Self-Adjusting Computation
- article
- The 29th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA '17), Jul 2017, Washington, United States. ⟨10.1145/3087556.3087595⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gergö Barany, Julien Signoles
- titre
- Hybrid Information Flow Analysis for Real-World C Code
- article
- TAP 2017 - 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. pp.23-40, ⟨10.1007/978-3-319-61467-0_2⟩
- Accès au texte intégral et bibtex
-
- auteur
- Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
- titre
- A Formally Verified Compiler for Lustre
- article
- PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain
- Accès au texte intégral et bibtex
-
- auteur
- Pietro Abate, Roberto Di Cosmo
- titre
- Adoption of Academic Tools in Open Source Communities: The Debian Case Study
- article
- 13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. pp.139-150, ⟨10.1007/978-3-319-57735-7_14⟩
- Accès au texte intégral et bibtex
-
- auteur
- Markus Raab, Gergö Barany
- titre
- Challenges in Validating FLOSS Conguration
- article
- 13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. pp.101-114, ⟨10.1007/978-3-319-57735-7_11⟩
- Accès au texte intégral et bibtex
-
- auteur
- Markus Raab, Gergö Barany
- titre
- Introducing Context Awareness in Unmodified, Context-unaware Software
- article
- ENASE 2017 - 12th International Conference on Evaluation of Novel Approaches to Software Engineering, Apr 2017, Porto, Portugal. pp.1-8
- Accès au texte intégral et bibtex
-
- auteur
- Arthur Charguéraud, François Pottier
- titre
- Temporary Read-Only Permissions for Separation Logic
- article
- Proceedings of the 26th European Symposium on Programming (ESOP 2017), Apr 2017, Uppsala, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, Christian Ferdinand
- titre
- Closing the Gap – The Formally Verified Optimizing Compiler CompCert
- article
- SSS'17: Safety-critical Systems Symposium 2017, Feb 2017, Bristol, United Kingdom. pp.163-180
- Accès au texte intégral et bibtex
-
- auteur
- Umut A Acar, Naama Ben-David, Mike Rainey
- titre
- Contention in Structured Concurrency: Provably Efficient Dynamic Non-Zero Indicators for Nested Parallelism
- article
- 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Feb 2017, Austin, United States. ⟨10.1145/3018743.3018762⟩
- Accès au texte intégral et bibtex
-
- auteur
- Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell
- titre
- Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
- article
- 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), ACM, Jan 2017, Paris, France
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
- article
- Certified Programs and Proofs, Jan 2017, Paris, France
- Accès au texte intégral et bibtex
-
Other publications
- auteur
- The Coq Development Team
- titre
- The Coq Proof Assistant, version 8.7.1
- article
- 2017, pp.1-571. ⟨10.5281/zenodo.1133970⟩
- Accès au bibtex
-
- auteur
- Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier
- titre
- VOCAL – A Verified OCAml Library
- article
- 2017
- Accès au texte intégral et bibtex
-
- auteur
- Jade Alglave, Luc Maranget, Paul Mckenney, Alan Stern, Andrea Parri
- titre
- A formal kernel memory-ordering model (Part 1 and 2)
- article
- 2017
- Accès au bibtex
-
Poster communications
- auteur
- Arthur Charguéraud, Mike Rainey
- titre
- Efficient Representations for Large Dynamic Sequences in ML
- article
- ML Family Workshop, Sep 2017, Oxford, United Kingdom. 2017
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Thomas Williams, Didier Rémy
- titre
- A Principled Approach to Ornamentation in ML
- article
- [Research Report] Inria. 2017
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Markus Raab, Gergö Barany
- titre
- Introducing Context Awareness in Unmodified, Context-unaware Software
- article
- 2017
- Accès au texte intégral et bibtex
-
- auteur
- Gergö Barany
- titre
- Liveness-Driven Random Program Generation
- article
- 2017
- Accès au texte intégral et bibtex
-
- auteur
- Florent Balestrieri, Michel Mauny
- titre
- Generic Programming in OCAML
- article
- 2017
- Accès au texte intégral et bibtex
-
2016
Journal articles
- auteur
- Umut A Acar, Arthur Charguéraud, Mike Rainey
- titre
- Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages
- article
- Journal of Functional Programming, 2016, 26, ⟨10.1017/S0956796816000101⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski, François Pottier, Jonathan Protzenko
- titre
- The Design and Formalization of Mezzo, a Permission-Based Programming Language
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
- Accès au texte intégral et bibtex
-
- auteur
- Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo De Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
- titre
- Testing Noninterference, Quickly
- article
- Journal of Functional Programming, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
- Accès au bibtex
-
- auteur
- Marie-Karelle Riviere, Ying Yuan, Jacques-Henri Jourdan, Frédéric Dubois, Sarah Zohar
- titre
- Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization
- article
- Statistical Methods in Medical Research, 2016, ⟨10.1177/0962280216631763⟩
- Accès au texte intégral et bibtex
-
- auteur
- Marie-Karelle Riviere, Jacques-Henri Jourdan, Sarah Zohar
- titre
- dfcomb: An R-package for phase I/II trials of drug combinations
- article
- Computer Methods and Programs in Biomedicine, 2016, 125, pp.117-133. ⟨10.1016/j.cmpb.2015.10.018⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Kasper Svendsen, Filip Sieczkowski, Lars Birkedal
- titre
- Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
- article
- 25th European Symposium on Programming Languages and Systems, Dec 2016, Eindhoven, Netherlands. pp.727 - 751, ⟨10.1007/978-3-662-49498-1_28⟩
- Accès au texte intégral et bibtex
-
- auteur
- Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
- titre
- A Certified Universal Gathering Algorithm for Oblivious Mobile Robots
- article
- Distributed Computing (DISC), Sep 2016, Paris, France
- Accès au bibtex
-
- auteur
- Benjamin Canou, Grégoire Henry, Çagdas Bozman, Fabrice Le Fessant
- titre
- Learn OCaml, An Online Learning Center for OCaml
- article
- OCaml Users and Developers Workshop 2016, Sep 2016, Nara, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Luc Maranget, Thomas Réfis
- titre
- Ambiguous pattern variables
- article
- OCaml 2016: The OCaml Users and Developers Workshop, Sep 2016, Nara, Japan. pp.2
- Accès au texte intégral et bibtex
-
- auteur
- Çagdas Bozman, Théophane Huffschmitt, Michael Laporte, Fabrice Le Fessant
- titre
- ocp-lint, A Plugin-based Style-Checker with Semantic Patches
- article
- OCaml Users and Developers Workshop 2016, Sep 2016, Nara, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Florent Balestrieri, Michel Mauny
- titre
- Generic Programming in OCaml
- article
- OCaml 2016 - The OCaml Users and Developers Workshop, Sep 2016, Nara, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Fabrice Le Fessant
- titre
- OPAM-builder: Continuous Monitoring of OPAM Repositories
- article
- OCaml Users and Developers Workshop 2016, Sep 2016, Nara, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Jacques-Henri Jourdan
- titre
- Statistically profiling memory in OCaml
- article
- OCaml 2016, Sep 2016, Nara, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Umut A Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski
- titre
- Dag-calculus: a calculus for parallel computation
- article
- Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), Sep 2016, Nara, Japan. pp.18 - 32, ⟨10.1145/2951913.2951946⟩
- Accès au texte intégral et bibtex
-
- auteur
- Ram A Raghunathan, Stefan A Muller, Umut A Acar, Guy A Blelloch
- titre
- Hierarchical Memory Management for Parallel Programs
- article
- Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. ⟨10.1145/3022670.2951935⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jacques-Henri Jourdan
- titre
- Sparsity Preserving Algorithms for Octagons
- article
- NSAD 2016 - Numerical and symbolic abstract domains workshop , Sep 2016, Edinburgh, United Kingdom. pp.14
- Accès au texte intégral et bibtex
-
- auteur
- Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
- titre
- Brief announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots
- article
- ACM Conference on Principles of Distributed Computing (PODC), ACM, Jul 2016, Chicago, United States
- Accès au bibtex
-
- auteur
- Benoît Vaugon, Michel Mauny
- titre
- A Type Inference System Based on Saturation of Subtyping Constraints
- article
- Trends in Functional Programming, Jun 2016, College Park (MD), United States
- Accès au texte intégral et bibtex
-
- auteur
- Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
- titre
- Proving Determinacy of the PharOS Real-Time Operating System
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Reachability and Error Diagnosis in LR(1) Parsers
- article
- CC 2016 - 25th International Conference on Compiler Construction, Mar 2016, Barcelone, Spain. pp.11, ⟨10.1145/2892208.2892224⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand
- titre
- CompCert - A Formally Verified Optimizing Compiler
- article
- ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France
- Accès au texte intégral et bibtex
-
- auteur
- Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
- titre
- Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
- article
- Principles of Programming Languages 2016 (POPL 2016), Jan 2016, Saint Petersburg, United States
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Reachability and error diagnosis in LR(1) automata
- article
- Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Jacques-Henri Jourdan
- titre
- Verasco: a Formally Verified C Static Analyzer
- article
- Programming Languages [cs.PL]. Universite Paris Diderot-Paris VII, 2016. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer
- titre
- Which types have a unique inhabitant?
- article
- Programming Languages [cs.PL]. Université Paris-Diderot, 2016. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2015
Journal articles
- auteur
- Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
- titre
- Impossibility of gathering, a certification
- article
- Information Processing Letters, 2015, 115 (3), pp.447-452. ⟨10.1016/j.ipl.2014.11.001⟩
- Accès au bibtex
-
- auteur
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
- titre
- Verified Compilation of Floating-Point Computations
- article
- Journal of Automated Reasoning, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
- Accès au texte intégral et bibtex
-
- auteur
- Béatrice Bérard, Pierre Courtieu, Laure Millet, Maria Potop-Butucaru, Lionel Rieg, Nathalie Sznajder, Sébastien Tixeuil, Xavier Urbain
- titre
- [Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems
- article
- International Journal of Informatics Society, 2015, 7 (3), pp.101-114
- Accès au bibtex
-
Conference papers
- auteur
- Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant
- titre
- Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
- article
- LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
- Accès au texte intégral et bibtex
-
- auteur
- Umut A. Acar, Arthur Charguéraud, Mike Rainey
- titre
- A Work-Efficient Algorithm for Parallel Unordered Depth-First Search
- article
- Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, Nov 2015, Austin, Texas, United States. ⟨10.1145/2807591.2807651⟩
- Accès au texte intégral et bibtex
-
- auteur
- Pierre Chambart, Michael Laporte, Vincent Bernardoff, Fabrice Le Fessant
- titre
- Operf: Benchmarking the OCaml Compiler
- article
- OCaml Users and Developers Workshop, Sep 2015, Vancouver, Canada
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Blanc, Pierre Chambart, Michel Mauny, Fabrice Le Fessant
- titre
- Global Semantic Analysis on OCaml programs
- article
- OCaml 2015 - The OCaml Users and Developers Workshop, Sep 2015, Vancouver, Canada
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- Which simple types have a unique inhabitant?
- article
- The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Aug 2015, Vancouver, Canada
- Accès au texte intégral et bibtex
-
- auteur
- Arthur Charguéraud, François Pottier
- titre
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
- article
- 6th International Conference on Interactive Theorem Proving (ITP), Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_9⟩
- Accès au texte intégral et bibtex
-
- auteur
- Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce
- titre
- Foundational Property-Based Testing
- article
- ITP 2015 - 6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_22⟩
- Accès au texte intégral et bibtex
-
- auteur
- Guillaume Munch-Maccagnoni, Gabriel Scherer
- titre
- Polarised Intermediate Representation of Lambda Calculus with Sums
- article
- Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.22⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer
- titre
- Multi-focusing on extensional rewriting with sums
- article
- Typed Lambda Calculi and Applications, Jun 2015, Warsaw, Poland
- Accès au texte intégral et bibtex
-
- auteur
- Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach
- titre
- Micro-Policies: Formally Verified, Tag-Based Security Monitors
- article
- 2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier, Jonathan Protzenko
- titre
- A few lessons from the Mezzo project
- article
- Summit oN Advances in Programming Languages (SNAPL), May 2015, Asilomar, United States. ⟨10.4230/LIPIcs.SNAPL.2015.221⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- Full reduction in the face of absurdity
- article
- ESOP'2015: European Conference on Programming Languages and Systems, Apr 2015, London, United Kingdom
- Accès au bibtex
-
- auteur
- Ezgi Çiçek, Deepak Garg, Umut Acar
- titre
- Refinement Types for Incremental Computational Complexity
- article
- 24th European Symposium on Programming (ESOP), Apr 2015, London, United Kingdom. pp.406-431, ⟨10.1007/978-3-662-46669-8_17⟩
- Accès au bibtex
-
- auteur
- Pramod Bhatotia, Pedro Fonseca, Umut A. Acar, Brandenburg Björn, Rodrigo Rodrigues
- titre
- iThreads: A Threading Library for Parallel Incremental Computation
- article
- Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, Mar 2015, Istanbul, Turkey. pp.645--659, ⟨10.1145/2694344.2694371⟩
- Accès au bibtex
-
- auteur
- Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
- titre
- A formally-verified C static analyzer
- article
- POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩
- Accès au texte intégral et bibtex
-
- auteur
- Çagdas Bozman, Grégoire Henry, Mohamed Iguernelala, Fabrice Le Fessant, Michel Mauny
- titre
- ocp-memprof: un profileur mémoire pour OCaml
- article
- Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- Depth-First Search and Strong Connectivity in Coq
- article
- Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France
- Accès au texte intégral et bibtex
-
- auteur
- Pierre-Évariste Dagand, Gabriel Scherer
- titre
- Normalization by realizability also evaluates
- article
- Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France
- Accès au texte intégral et bibtex
-
Other publications
- auteur
- Luc Maranget, Jade Alglave
- titre
- Towards a Formalization of the HSA Memory Model in the cat Language
- article
- 2015, pp.57
- Accès au bibtex
-
Proceedings
- auteur
- Xavier Leroy, Alwen Tiu
- titre
- CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs
- article
- Conference on Certified Programs and Proofs, Jan 2015, Mumbai, India. ACM, pp.184, 2015, 978-1-4503-3296-5
- Accès au bibtex
-
Reports
- auteur
- Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
- titre
- A Certified Universal Gathering Algorithm for Oblivious Mobile Robots
- article
- [Research Report] UPMC, Sorbonne Universites CNRS; CNAM, Paris; College de France; Université Paris Sud. 2015
- Accès au texte intégral et bibtex
-
- auteur
- Umut A. Acar, Arthur Charguéraud, Mike Rainey
- titre
- Fast Parallel Graph-Search with Splittable and Catenable Frontiers
- article
- [Technical Report] Inria. 2015
- Accès au texte intégral et bibtex
-
2014
Journal articles
- auteur
- Jade Alglave, Luc Maranget, Michael Tautschnig
- titre
- Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, 36 (2), pp.7:1--7:74. ⟨10.1145/2627752⟩
- Accès au texte intégral et bibtex
-
- auteur
- Pierre-Évariste Dagand, Conor Mcbride
- titre
- Transporting functions across ornaments
- article
- Journal of Functional Programming, 2014, 24 (2-3), pp.67. ⟨10.1017/S0956796814000069⟩
- Accès au texte intégral et bibtex
-
- auteur
- Yan Chen, Joshua Dunfield, Matthew A. Hammer, Umut A. Acar
- titre
- Implicit self-adjusting computation for purely functional programs
- article
- Journal of Functional Programming, 2014, 24 (1), pp.56-112
- Accès au bibtex
-
- auteur
- Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
- titre
- Implementing and reasoning about hash-consed data structures in Coq
- article
- Journal of Automated Reasoning, 2014, 53 (3), pp.271-304. ⟨10.1007/s10817-014-9306-0⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Pramod Bhatotia, Umut A. Acar, Flavio P. Junqueira, Rodrigo Rodrigues
- titre
- Slider: Incremental Sliding Window Analytics
- article
- Middleware 2014: Proceedings of the 15th International Middleware Conference, Dec 2014, Bordeaux, France. ⟨10.1145/2663165.2663334⟩
- Accès au bibtex
-
- auteur
- Xavier Leroy
- titre
- Compiler verification for fun and profit
- article
- FMCAD 2014 - Formal Methods in Computer-Aided Design, Oct 2014, Lausanne, Switzerland. pp.9
- Accès au texte intégral et bibtex
-
- auteur
- Umut A. Acar, Arthur Charguéraud, Mike Rainey
- titre
- Theory and Practice of Chunked Sequences
- article
- European Symposium on Algorithms, Sep 2014, Wrocław, Poland. pp.25 - 36, ⟨10.1007/978-3-662-44777-2_3⟩
- Accès au texte intégral et bibtex
-
- auteur
- James Cheney, Ahmed Amal, Umut A. Acar
- titre
- Database Queries that Explain their Work
- article
- PPDP 2014: 16th International Symposium on Principles and Practice of Declarative Programming, Sep 2014, Canterbury, United Kingdom. ⟨10.1145/2643135.2643143⟩
- Accès au bibtex
-
- auteur
- Pietro Abate, Roberto Di Cosmo, Louis Gesbert, Fabrice Le Fessant, Stefano Zacchiroli
- titre
- Using Preferences to Tame your Package Manager
- article
- OCaml 2014, Sep 2014, Goteborg, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Fabrice Le Fessant
- titre
- A Case for Multi-Switch Constraints in OPAM
- article
- OCaml 2014, Sep 2014, goteborg, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Michel Mauny, Benoît Vaugon
- titre
- Nullable Type Inference
- article
- OCaml 2014 - The OCaml Users and Developers Workshop, Sep 2014, Gothenbourg, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Pierrick Couderc, Benjamin Canou, Pierre Chambart, Fabrice Le Fessant
- titre
- A Proposal for Non-Intrusive Namespaces in OCaml
- article
- OCaml 2014, Sep 2014, Goteborg, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Formal proofs of code generation and verification tools
- article
- SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩
- Accès au texte intégral et bibtex
-
- auteur
- Yan Chen, Umut A. Acar, Kanat Tangwongsan
- titre
- Functional Programming for Dynamic and Large Data with Self-Adjusting Computation
- article
- ICFP 2014: 19th ACM SIGPLAN International Conference on Functional Programming, Sep 2014, Gothenburg, Sweden. ⟨10.1145/2628136.2628150⟩
- Accès au bibtex
-
- auteur
- François Pottier
- titre
- Hindley-Milner Elaboration in Applicative Style
- article
- ICFP 2014: 19th ACM SIGPLAN International Conference on Functional Programming, Sep 2014, Goteborg, Sweden. ⟨10.1145/2628136.2628145⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Williams, Pierre-Évariste Dagand, Didier Rémy
- titre
- Ornaments in practice
- article
- WGP 2014: ACM workshop on Generic programming, Aug 2014, Gothenburg, Sweden. ⟨10.1145/2633628.2633631⟩
- Accès au bibtex
-
- auteur
- Thomas Braibant, Jonathan Protzenko, Gabriel Scherer
- titre
- Well-typed generic smart-fuzzing for APIs
- article
- ML'14 - ACM SIGPLAN ML Family Workshop, Aug 2014, Göteborg, Sweden
- Accès au texte intégral et bibtex
-
- auteur
- Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
- titre
- Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
- article
- ARQNL 2014 - The first International Workshop on Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. pp.1-16
- Accès au texte intégral et bibtex
-
- auteur
- Robbert Krebbers, Xavier Leroy, Freek Wiedijk
- titre
- Formal C semantics: CompCert and the C standard
- article
- ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩
- Accès au texte intégral et bibtex
-
- auteur
- Julien Cretin, Didier Rémy
- titre
- System F with Coercion Constraints
- article
- CSL-LICS 2014: Joint Meeting of the Annual Conference on Computer Science Logic and the Annual Symposium on Logic in Computer Science, Jul 2014, Vienna, Austria. pp.34, ⟨10.1145/2603088.2603128⟩
- Accès au texte intégral et bibtex
-
- auteur
- Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan
- titre
- Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials
- article
- American Control Conference (ACC), Jun 2014, Portland, United States
- Accès au texte intégral et bibtex
-
- auteur
- Jade Alglave, Luc Maranget, Michael Tautschnig
- titre
- Herding cats: Modelling, simulation, testing, and data-mining for weak memory
- article
- PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2014, Edinburg, United Kingdom. pp.40, ⟨10.1145/2594291.2594347⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski, François Pottier, Jonathan Protzenko
- titre
- Type Soundness and Race Freedom for Mezzo
- article
- FLOPS 2014: 12th International Symposium on Functional and Logic Programming, Jun 2014, Kanazawa, Japan. pp.253 - 269, ⟨10.1007/978-3-319-07151-0_16⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Formal verification of a static analyzer: abstract interpretation in type theory
- article
- Types - The 2014 Types Meeting, May 2014, Paris, France
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- Deciding unique inhabitants with sums (work in progress)
- article
- TYPES, May 2014, Paris, France
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Proof assistants in computer science research
- article
- IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France
- Accès au bibtex
-
- auteur
- Sylvain Conchon, Luc Maranget, Alain Mebsout, David Declerck
- titre
- Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières
- article
- JFLA, Jan 2014, Fréjus, France
- Accès au texte intégral et bibtex
-
Book sections
- auteur
- Didier Rémy, Julien Cretin
- titre
- From Amber to Coercion Constraints
- article
- Martin Abadi; Philippa Gardner; Andrew D. Gordon; Radu Mardare. Essays for the Luca Cardelli Fest, MSR-TR-2014-104, Microsoft Research, 2014, TechReport
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart
- titre
- The CompCert memory model
- article
- Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010
- Accès au bibtex
-
Reports
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- Full reduction in the face of absurdity
- article
- [Research Report] INRIA. 2014
- Accès au texte intégral et bibtex
-
- auteur
- Julien Cretin, Didier Rémy
- titre
- System F with Coercion Constraints
- article
- [Research Report] RR-8456, INRIA. 2014, pp.36
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Çağdaş Bozman
- titre
- Profilage mémoire d’applications OCaml
- article
- Informatique [cs]. ENSTA ParisTech, 2014. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jonathan Protzenko
- titre
- Mezzo: a typed language for safe effectful concurrent programs
- article
- Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Julien Cretin
- titre
- Erasable coercions: a unified approach to type systems
- article
- Programming Languages [cs.PL]. Université Paris-Diderot - Paris VII, 2014. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Gabriel Scherer
- titre
- 2-or-more approximation for intuitionistic logic
- article
- 2014
- Accès au texte intégral et bibtex
-
2013
Journal articles
- auteur
- François Pottier
- titre
- Syntactic soundness proof of a type-and-capability system with hidden state
- article
- Journal of Functional Programming, 2013, 23 (1), pp.38-144. ⟨10.1017/S0956796812000366⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
- titre
- A step-indexed Kripke Model of Hidden State
- article
- Mathematical Structures in Computer Science, 2013, 23 (1), pp.1--54
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
- titre
- Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
- article
- LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩
- Accès au texte intégral et bibtex
-
- auteur
- David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant
- titre
- Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
- article
- IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Jan Hoffmann
- titre
- Tracking Data-Flow with Open Closure Types
- article
- LPAR 2013 - 19th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, Dec 2013, Stellenbosch, South Africa. pp.710-726
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski
- titre
- Weak Optimality, and the Meaning of Sharing
- article
- International Conference on Functional Programming (ICFP), Sep 2013, Boston, United States. pp.263-274, ⟨10.1145/2500365.2500606⟩
- Accès au bibtex
-
- auteur
- François Pottier, Jonathan Protzenko
- titre
- Programming with permissions in Mezzo
- article
- ICFP - The 18th ACM SIGPLAN International Conference on Functional Programming - 2013, Sep 2013, Boston, United States. pp.173-184, ⟨10.1145/2500365.2500598⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
- titre
- Implementing hash-consed structures in Coq
- article
- Interactive Theorem Proving, 4th international conference, Jul 2013, Rennes, France. pp.477-483, ⟨10.1007/978-3-642-39634-2_36⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thomas Braibant, Adam Chlipala
- titre
- Formal Verification of Hardware Synthesis
- article
- Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. pp.213-228, ⟨10.1007/978-3-642-39799-8_14⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
- titre
- A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
- article
- Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- GADTs meet subtyping
- article
- ESOP 2013 - 22nd European Symposium on Programming, Mar 2013, Rome, Italy. pp.554-573, ⟨10.1007/978-3-642-37036-6⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jacques Garrigue, Didier Rémy
- titre
- Ambivalent Types for Principal Type Inference with GADTs
- article
- APLAS 2013 - 11th Asian Symposium on Programming Languages and Systems, 2013, Melbourne, Australia. pp.257-272, ⟨10.1007/978-3-319-03542-0_19⟩
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Umut A. Acar, Arthur Charguéraud, Stefan Muller, Mike Rainey
- titre
- Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing
- article
- [Research Report] 2013
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Jan Hoffmann
- titre
- Tracking Data-Flow with Open Closure Types
- article
- [Research Report] RR-8345, INRIA. 2013, pp.24
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Jacques Garrigue, Didier Rémy
- titre
- Ambivalent Types for Principal Type Inference with GADTs (extended version)
- article
- 2013
- Accès au texte intégral et bibtex
-
- auteur
- Armaël Guéneau, François Pottier, Jonathan Protzenko
- titre
- The ins and outs of iteration in Mezzo
- article
- 2013
- Accès au bibtex
-
- auteur
- Jonathan Protzenko
- titre
- Illustrating the Mezzo programming language
- article
- 2013
- Accès au bibtex
-
2012
Journal articles
- auteur
- Nicolas Pouillard, François Pottier
- titre
- A unified treatment of syntax with binders
- article
- Journal of Functional Programming, 2012, 22 (4--5), pp.614--704. ⟨10.1017/S0956796812000251⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gregor Goessler, Dana N. Xu, Alain Girault
- titre
- Probabilistic contracts for component-based design
- article
- Formal Methods in System Design, 2012, 41 (2), pp.211-231. ⟨10.1007/s10703-012-0162-4⟩
- Accès au bibtex
-
- auteur
- Didier Rémy, Boris Yakobowski
- titre
- A Church-Style Intermediate Language for MLF
- article
- Theoretical Computer Science, 2012, 435, pp.77--105. ⟨10.1016/j.tcs.2012.02.026⟩
- Accès au texte intégral et bibtex
-
- auteur
- Andrew W. Appel, Robert Dockins, Xavier Leroy
- titre
- A list-machine benchmark for mechanized metatheory
- article
- Journal of Automated Reasoning, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Valentin Robert, Xavier Leroy
- titre
- A formally-verified alias analysis
- article
- CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.11-26, ⟨10.1007/978-3-642-35308-6_5⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Mechanized Semantics for Compiler Verification
- article
- APLAS 2012 - 10th Asian Symposium on Programming Languages and Systems, Dec 2012, Kyoto, Japan. pp.386-388, ⟨10.1007/978-3-642-35182-2_27⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jacques Garrigue, Didier Rémy
- titre
- Tracing ambiguity in GADT type inference
- article
- ACM SIGPLAN Workshop on ML, Sep 2012, copenhagen, Denmark
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- GADTs Meet Subtyping
- article
- ACM SIGPLAN Workshop on ML, Sep 2012, Copenhagen, Denmark
- Accès au texte intégral et bibtex
-
- auteur
- Jonathan Protzenko, François Pottier
- titre
- Programming with permissions: the Mezzo language
- article
- ACM SIGPLAN Workshop on ML, Sep 2012, Copenhagen, Denmark
- Accès au texte intégral et bibtex
-
- auteur
- Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
- titre
- TLA+ Proofs
- article
- 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩
- Accès au texte intégral et bibtex
-
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- GADT meet subtyping
- article
- ACM SIGPLAN Workshop on ML, Aug 2012, Copenhague, Denmark
- Accès au texte intégral et bibtex
-
- auteur
- Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
- titre
- TLA+ Proofs
- article
- AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p
- Accès au bibtex
-
- auteur
- Damien Doligez, Mathieu Jaume, Renaud Rioboo
- titre
- Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment. A case study within the FoCaLiZe environment
- article
- PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Jun 2012, Beijing, China. ⟨10.1145/2336717.2336726⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jacques-Henri Jourdan, François Pottier, Xavier Leroy
- titre
- Validating LR(1) Parsers
- article
- ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩
- Accès au texte intégral et bibtex
-
- auteur
- Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris
- titre
- Formally verified optimizing compilation in ACG-based flight control software
- article
- ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France
- Accès au texte intégral et bibtex
-
- auteur
- Tahina Ramananandro, Gabriel dos Reis, Xavier Leroy
- titre
- A mechanized semantics for C++ object construction and destruction, with applications to resource management
- article
- POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2012, Philadelphia, PA, United States. pp.521-532, ⟨10.1145/2103656.2103718⟩
- Accès au texte intégral et bibtex
-
- auteur
- Julien Cretin, Didier Rémy
- titre
- On the Power of Coercion Abstraction
- article
- POPL 2012: 39th ACM SIGPLAN-SIGACT Symposium on Principle Of Programming Languages, ACM, Jan 2012, Philadelphia, United States. ⟨10.1145/2103656.2103699⟩
- Accès au bibtex
-
- auteur
- Dana N. Xu
- titre
- Hybrid contract checking via symbolic simplification
- article
- PEPM'12: ACM workshop on Partial evaluation and program manipulation, Jan 2012, Philadelphia, United States. pp.107-116, ⟨10.1145/2103746.2103767⟩
- Accès au bibtex
-
Reports
- auteur
- Gabriel Scherer, Didier Rémy
- titre
- GADT meet Subtyping
- article
- [Research Report] RR-8114, INRIA. 2012, pp.33
- Accès au texte intégral et bibtex
-
- auteur
- Gregor Gössler, Dana N. Xu, Alain Girault
- titre
- Probabilistic Contracts for Component-based Design
- article
- [Research Report] RR-7328, INRIA. 2012
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy, Andrew W. Appel, Sandrine Blazy, Gordon Stewart
- titre
- The CompCert Memory Model, Version 2
- article
- [Research Report] RR-7987, INRIA. 2012, pp.26
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Nicolas Pouillard
- titre
- Namely, Painless: A unifying approach to safe programming with first-order syntax with binders
- article
- Programming Languages [cs.PL]. Université Paris-Diderot - Paris VII, 2012. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Tahina Ramananandro
- titre
- Mechanized Formal Semantics and Verified Compilation for C++ Objects
- article
- Programming Languages [cs.PL]. Université Paris-Diderot - Paris VII, 2012. English. ⟨NNT : 2012PA077001⟩
- Accès au texte intégral et bibtex
-
2011
Journal articles
- auteur
- Xavier Leroy
- titre
- Safety First! (technical perspective)
- article
- Communications of the ACM, 2011, 54 (12), pp.122. ⟨10.1145/2043174.2043196⟩
- Accès au bibtex
-
Conference papers
- auteur
- Nicolas Pouillard
- titre
- Nameless, Painless
- article
- ICFP 2011: 16th International Conference on Functional Programming, Sep 2011, Tokyo, Japan. pp.320-332, ⟨10.1145/2034773.2034817⟩
- Accès au bibtex
-
- auteur
- Pascal Cuoq, Julien Signoles, Damien Doligez
- titre
- Lightweight Typed Customizable Unmarshaling
- article
- ACM SIGPLAN Workshop on ML, Sep 2011, Tokyo, Japan
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Formally verifying a compiler: Why? How? How far?
- article
- CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, Apr 2011, Chamonix, France. ⟨10.1109/CGO.2011.5764668⟩
- Accès au texte intégral et bibtex
-
- auteur
- Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris
- titre
- Towards Formally Verified Optimizing Compilation in Flight Control Software
- article
- PPES 2011: Predictability and Performance in Embedded Systems, Mar 2011, Grenoble, France. pp.59-68, ⟨10.4230/OASIcs.PPES.2011.59⟩
- Accès au texte intégral et bibtex
-
- auteur
- Tahina Ramananandro, Gabriel dos Reis, Xavier Leroy
- titre
- Formal verification of object layout for C++ multiple inheritance
- article
- POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2011, Austin, TX, United States. pp.67-79, ⟨10.1145/1926385.1926395⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Verified squared: does critical software deserve verified tools?
- article
- POPL 2011 - 38th symposium Principles of Programming Languages, Jan 2011, Austin, United States. pp.1-2, ⟨10.1145/1926385.1926387⟩
- Accès au texte intégral et bibtex
-
- auteur
- François Pottier
- titre
- A typed store-passing translation for general references
- article
- POPL 2011: 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Jan 2011, Austin, United States. ⟨10.1145/1925844.1926403⟩
- Accès au texte intégral et bibtex
-
- auteur
- Alexandre Pilkiewicz, François Pottier
- titre
- The essence of monotonic state
- article
- TLDI 2011: The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2011, Austin, United States. ⟨10.1145/1929553.1929565⟩
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Julien Cretin, Didier Rémy
- titre
- On the Power of Coercion Abstraction
- article
- [Research Report] RR-7587, INRIA. 2011, pp.59
- Accès au texte intégral et bibtex
-
- auteur
- Na Xu
- titre
- Hybrid Contract Checking via Symbolic Simplification
- article
- [Research Report] RR-7794, INRIA. 2011
- Accès au texte intégral et bibtex
-
2010
Journal articles
- auteur
- Xavier Leroy
- titre
- Comment faire confiance à un compilateur ?
- article
- Interstices, 2010
- Accès au bibtex
-
- auteur
- Xavier Leroy
- titre
- Comment faire confiance à un compilateur ?
- article
- Les Cahiers de l'INRIA - La Recherche, 2010, Cancer la révolution, 440 avril 2010
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Dana N. Xu, Gregor Goessler, Alain Girault
- titre
- Probabilistic Contracts for Component-Based Design
- article
- the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore. pp.325-340, ⟨10.1007/978-3-642-15643-4_24⟩
- Accès au bibtex
-
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- titre
- The TLA+ Proof System: Building a Heterogeneous Verification Platform
- article
- International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩
- Accès au bibtex
-
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- titre
- Verifying Safety Properties With the TLA+ Proof System
- article
- Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142--148, ⟨10.1007/978-3-642-14203-1_12⟩
- Accès au texte intégral et bibtex
-
- auteur
- Silvain Rideau, Xavier Leroy
- titre
- Validating register allocation and spilling
- article
- Compiler Construction 2010, Mar 2010, Paphos, Cyprus. pp.224-243, ⟨10.1007/978-3-642-11970-5_13⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jean-Baptiste Tristan, Xavier Leroy
- titre
- A simple, verified validator for software pipelining
- article
- 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. ⟨10.1145/1706299.1706311⟩
- Accès au texte intégral et bibtex
-
Book sections
- auteur
- Xavier Leroy
- titre
- Mechanized semantics
- article
- J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp.195-224, 2010, NATO Science for Peace and Security Series D: Information and Communication Security, ⟨10.3233/978-1-60750-100-8-195⟩
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Benoît Montagu
- titre
- Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types
- article
- Programming Languages [cs.PL]. Ecole Polytechnique X, 2010. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2009
Journal articles
- auteur
- Xavier Leroy
- titre
- A formally verified compiler back-end
- article
- Journal of Automated Reasoning, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
- Accès au texte intégral et bibtex
-
- auteur
- Zaynah Dargaye, Xavier Leroy
- titre
- A verified framework for higher-order uncurrying optimizations
- article
- Higher-Order and Symbolic Computation, 2009, 22 (3), ⟨10.1007/s10990-010-9050-z⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Formal verification of a realistic compiler
- article
- Communications of the ACM, 2009, 52 (7), pp.107-115. ⟨10.1145/1538788.1538814⟩
- Accès au texte intégral et bibtex
-
- auteur
- Didier Le Botlan, Didier Rémy
- titre
- Recasting MLF
- article
- Information and Computation, 2009, Volume 207, Issue 6, June 2009, Pages 726-785, 207 (6), pp.726-785. ⟨10.1016/j.ic.2008.12.006⟩
- Accès au texte intégral et bibtex
-
- auteur
- Tom Hirschowitz, Xavier Leroy, J. B. Wells
- titre
- Compilation of extended recursion in call-by-value functional languages
- article
- Higher-Order and Symbolic Computation, 2009, 22 (1), pp.3-66. ⟨10.1007/s10990-009-9042-z⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sandrine Blazy, Xavier Leroy
- titre
- Mechanized semantics for the Clight subset of the C language
- article
- Journal of Automated Reasoning, 2009, 43 (3), pp.263-288. ⟨10.1007/s10817-009-9148-3⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy, Hervé Grall
- titre
- Coinductive big-step operational semantics
- article
- Information and Computation, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Sandrine Blazy, Benoît Robillard
- titre
- Register allocation by graph coloring under full live-range splitting
- article
- ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded systems (LCTES'2009), ACM, Jun 2009, Dublin, Ireland
- Accès au texte intégral et bibtex
-
- auteur
- Jean-Baptiste Tristan, Xavier Leroy
- titre
- Verified Validation of Lazy Code Motion
- article
- ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), Jun 2009, Dublin, Ireland. pp.316-326, ⟨10.1145/1542476.1542512⟩
- Accès au texte intégral et bibtex
-
- auteur
- Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, Gilles Muller
- titre
- A foundation for flow-based program matching: using temporal logic and model checking
- article
- The 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'09, Jan 2009, Savannah, Georgia, United States. pp.114-126, ⟨10.1145/1480881.1480897⟩
- Accès au bibtex
-
Theses
- auteur
- Benoit Razet
- titre
- Machines d'Eilenberg Effectives
- article
- Informatique [cs]. Université Paris-Diderot - Paris VII, 2009. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Jean-Baptiste Tristan
- titre
- Formal verification of translation validators
- article
- Génie logiciel [cs.SE]. Université Paris-Diderot - Paris VII, 2009. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- auteur
- Zaynah Dargaye
- titre
- Vérification formelle d'un compilateur optimisant pour langages fonctionnels
- article
- Génie logiciel [cs.SE]. Université Paris-Diderot - Paris VII, 2009. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
2008
Journal articles
- auteur
- Laurence Rideau, Bernard P. Serpette, Xavier Leroy
- titre
- Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
- article
- Journal of Automated Reasoning, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy, Sandrine Blazy
- titre
- Formal verification of a C-like memory model and its uses for verifying program transformations
- article
- Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- 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, Pierre Weis
- titre
- Trusted Software within Focal
- article
- C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. pp.162-179
- Accès au texte intégral et bibtex
-
- auteur
- Yann Régis-Gianas, François Pottier
- titre
- A Hoare Logic for Call-by-Value Functional Programs
- article
- MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. pp.305--335, ⟨10.1007/978-3-540-70594-9_17⟩
- Accès au bibtex
-
- auteur
- Benoît Robillard, Sandrine Blazy, Eric Soutif
- titre
- Coloration avec préférences : complexité, inégalités valides et vérification formelle
- article
- ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, ROADEF, Feb 2008, Clermont-Ferrand, France. pp.123-138
- Accès au texte intégral et bibtex
-
- auteur
- Jean-Baptiste Tristan, Xavier Leroy
- titre
- Formal verification of translation validators: A case study on instruction scheduling optimizations
- article
- 35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩
- Accès au texte intégral et bibtex
-
- auteur
- Boris Yakobowski
- titre
- Le caractère ` à la rescousse -- Factorisation et réutilisation de code grâce aux variants polymorphes
- article
- JFLA (Journées Francophones des Langages Applicatifs), INRIA, Jan 2008, Etretat, France. pp.63-78
- Accès au texte intégral et bibtex
-
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- titre
- A TLA+ Proof System
- article
- Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar
- Accès au texte intégral et bibtex
-
Books
- auteur
- Sandrine Blazy
- titre
- Actes de la conférence JFLA2008 (Journées Francophones des Langages Applicatifs)
- article
- INRIA. INRIA, pp.173, 2008, 2-7261-1295-1
- Accès au texte intégral et bibtex
-
Theses
- auteur
- Boris Yakobowski
- titre
- Graphical types and constraints - second-order polymorphism and inference
- article
- Software Engineering [cs.SE]. Université Paris-Diderot - Paris VII, 2008. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia Lawall, Gilles Muller
- titre
- A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
- article
- 2008
- Accès au texte intégral et bibtex
-
2007
Journal articles
- auteur
- Sandrine Blazy
- titre
- Comment gagner confiance en C ?
- article
- Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2007, numéro spécial "Langages applicatifs", 26 (9), pp.1195-1200. ⟨10.3166/TSI.26.1195-1200⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Sandrine Blazy, Benoît Robillard, Eric Soutif
- titre
- Coloration avec préférences dans les graphes triangulés
- article
- Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp.32
- Accès au bibtex
-
- auteur
- Zaynah Dargaye, Xavier Leroy
- titre
- Mechanized verification of CPS transformations
- article
- Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. pp.211-225, ⟨10.1007/978-3-540-75560-9_17⟩
- Accès au texte intégral et bibtex
-
- auteur
- Richard Bonichon, David Delahaye, Damien Doligez
- titre
- Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs
- article
- LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. pp.151-165, ⟨10.1007/978-3-540-75560-9_13⟩
- Accès au texte intégral et bibtex
-
- auteur
- Andrew W. W. Appel, Sandrine Blazy
- titre
- Separation Logic for Small-step Cminor
- article
- 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. pp.5-21
- Accès au texte intégral et bibtex
-
- auteur
- Zaynah Dargaye
- titre
- Décurryfication certifiée
- article
- Journées Francophones des Langages Applicatifs (JFLA 2007), INRIA, Jan 2007, Aix-les-Bains, France. pp.119-134
- Accès au texte intégral et bibtex
-
- auteur
- Sandrine Blazy
- titre
- Experiments in validating formal semantics for C
- article
- C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Alain Frisch, Haruo Hosoya
- titre
- Towards Practical Typechecking for Macro Tree Transducers
- article
- [Research Report] RR-6107, INRIA. 2007, pp.28
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- A locally nameless solution to the POPLmark challenge
- article
- [Research Report] RR-6098, INRIA. 2007, pp.54
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Laurence Rideau, Bernard P. Serpette, Xavier Leroy
- titre
- Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves
- article
- 2007
- Accès au texte intégral et bibtex
-
2006
Conference papers
- auteur
- Andrew W. W. Appel, Xavier Leroy
- titre
- A list-machine benchmark for mechanized metatheory (extended abstract)
- article
- Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Coinductive big-step operational semantics
- article
- European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. pp.42-54, ⟨10.1007/11693024_5⟩
- Accès au texte intégral et bibtex
-
- auteur
- Xavier Leroy
- titre
- Formal certification of a compiler back-end, or: programming a compiler with a proof assistant
- article
- 33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. pp.42--54, ⟨10.1145/1111037.1111042⟩
- Accès au texte intégral et bibtex
-
Reports
- auteur
- Andrew W. W. Appel, Xavier Leroy
- titre
- A list-machine benchmark for mechanized metatheory
- article
- [Research Report] RR-5914, INRIA. 2006
- Accès au texte intégral et bibtex
-
2005
Journal articles
- auteur
- Tom Hirschowitz, Xavier Leroy
- titre
- Mixin modules in a call-by-value setting
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2005, 27 (5), pp.857 - 881. ⟨10.1145/1086642.1086644⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Serge Abiteboul, Xavier Leroy, Boris Vrdoljak, Ciaran Bryce, Roberto Di Cosmo, Klaus R. Dittrich, Stéphane Fermigier, Tova Milo, Assaf Sagi, Yotam Shtossel, Stéphane Laurière, Frédéric Lepied, Radu Pop, Eleonora Panto, Jean-Paul Smets
- titre
- EDOS: Environment for the Development and Distribution of Open Source Software
- article
- OSS 2005 - The First International Conference on Open Source Systems, Jul 2005, Genova, Italy
- Accès au bibtex
-
- auteur
- Giuseppe Castagna, Alain Frisch
- titre
- A gentle introduction to semantic subtyping
- article
- Proceedings of PPDP '05, the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pages 198-208, ACM Press (full version) and ICALP '05, 32nd International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science n. 3580, pages 30-34, Springer (summary), 2005, Portugal
- Accès au bibtex
-
- auteur
- Haruo Hosoya, Alain Frisch, Giuseppe Castagna
- titre
- Parametric Polymorphism for XML
- article
- 2005, pp.50-62
- Accès au bibtex
-
- auteur
- Giuseppe Castagna, Dario Colazzo, Alain Frisch
- titre
- Error Mining for Regular Expression Patterns
- article
- 2005, pp.160-172
- Accès au bibtex
-
2004
Conference papers
- auteur
- Yves Bertot, Benjamin Grégoire, Xavier Leroy
- titre
- A structured approach to proving compiler optimizations based on dataflow analysis
- article
- Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩
- Accès au texte intégral et bibtex
-
- auteur
- Tom Hirschowitz, Xavier Leroy, J. B. Wells
- titre
- Call-by-value mixin modules: Reduction semantics, side effects, types
- article
- European Symposium on Programming, 2004, Barcelona, Spain. pp.64-78, ⟨10.1007/b96702⟩
- Accès au texte intégral et bibtex
-
2002
Conference papers
- auteur
- Tom Hirschowitz, Xavier Leroy
- titre
- Mixin modules in a call-by-value setting
- article
- European Symposium on Programming, 2002, Grenoble, France. pp.207-236, ⟨10.1007/3-540-45927-8⟩
- Accès au texte intégral et bibtex
-