Publications HAL du labo/EPI Gallium

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, ACM, 2018, pp.1-30. 〈10.1145/3158109〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01666104/file/ornaments-popl18-final.pdf BibTex

Conference papers

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
https://hal.inria.fr/hal-01887733/file/main.pdf 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
https://hal.inria.fr/hal-01799629/file/LOLA_2018_paper_4.pdf 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. Dagstuhl Publishing, OpenAccess Series in Informatics, 63, 〈10.4230/OASIcs.WCET.2018.8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01848686/file/wcet2018_embedded_program_annotations.pdf 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
https://hal.inria.fr/hal-01888607/file/main.pdf 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. 2018, 〈10.1145/3173162.3177156〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01873636/file/asplos2018.pdf 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
https://hal.inria.fr/hal-01682683/file/cc2018.pdf BibTex
auteur
Vitalii Aksenov, Umut 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. 18, 2018, 〈10.1145/3178487.3178516〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01887717/file/main.pdf 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, Jan 2018, Toulouse, France. pp.1-9, 2018, 〈https://www.erts2018.org/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643290/file/ERTS_2018_paper_59.pdf 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. 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01682691/file/jfla2018.pdf BibTex

Reports

auteur
Xavier Leroy
titre
The CompCert C verified compiler: Documentation and user’s manual
article
[Intern report] Inria. 2018, pp.1-77
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091802/file/manual.pdf BibTex
auteur
Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, Jérôme Vouillon
titre
The OCaml system release 4.07: Documentation and user's manual
article
[Intern report] Inria. 2018, pp.1-752
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00930213/file/ocaml-4.07-refman.pdf BibTex
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
https://hal.archives-ouvertes.fr/hal-01801276/file/compil-fcl.pdf 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
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01887505/file/main.pdf BibTex

2017

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, Springer Verlag, 2017, 〈10.1007/s10817-017-9431-7〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01652785/file/credits_jar.pdf BibTex
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), ACM, 2017, 39 (4), pp.1 - 36. 〈10.1145/3064848〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633123/file/jourdan2017simple.pdf BibTex
auteur
François Pottier
titre
Visitors unchained
article
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.1 - 28. 〈10.1145/3110272〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670735/file/fpottier-visitors-unchained.pdf 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. 10855, 2018, Lecture Notes in Computer Science. 〈https://www.sci.unich.it/lopstr17/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01860621/file/lopstr2017.pdf 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. Springer, Proceedings of AVOCS 2017, 10471, pp.165-181, 2017, Lecture Notes in Computer Science. 〈https://easychair.org/cfp/FMICS-AVoCS2017〉. 〈10.1007/978-3-319-67113-0_11〉
Accès au bibtex
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, 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01661696/file/main.pdf 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
https://arxiv.org/pdf/1702.04441 BibTex
auteur
Umut 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
https://hal.inria.fr/hal-01664903/file/main.pdf 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. Springer, LNCS, 10375, pp.23-40, 〈10.1007/978-3-319-61467-0_2〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658653/file/hybrid_information_flow.pdf 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, Jun 2017, Barcelone, Spain. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, 〈http://pldi17.sigplan.og〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01512286/file/velus-pldi17.pdf BibTex
auteur
Markus Raab, Gergö Barany
titre
Challenges in Validating FLOSS Conguration
article
Federico Balaguer; Roberto Di Cosmo; Alejandra Garrido; Fabio Kon; Gregorio Robles; Stefano Zacchiroli. 13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. Springer, IFIP Advances in Information and Communication Technology, AICT-496, pp.101-114, 2017, Open Source Systems: Towards Robust Practices. 〈10.1007/978-3-319-57735-7_11〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658595/file/oss.pdf BibTex
auteur
Pietro Abate, Roberto Cosmo
titre
Adoption of Academic Tools in Open Source Communities: The Debian Case Study
article
Federico Balaguer; Roberto Di Cosmo; Alejandra Garrido; Fabio Kon; Gregorio Robles; Stefano Zacchiroli. 13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. Springer International Publishing, IFIP Advances in Information and Communication Technology, AICT-496, pp.139-150, 2017, Open Source Systems: Towards Robust Practices. 〈10.1007/978-3-319-57735-7_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01776283/file/432701_1_En_14_Chapter.pdf 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
https://hal.inria.fr/hal-01658620/file/enase_submission.pdf 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
https://hal.inria.fr/hal-01408657/file/readonlysep.pdf 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. CreateSpace, pp.163-180, 2017, Developments in System Safety Engineering: Proceedings of the Twenty-fifth Safety-critical Systems Symposium
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01399482/file/SSS2017_kaestner_et_al.pdf BibTex
auteur
Umut 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
https://hal.inria.fr/hal-01416531/file/dynsnzi.pdf BibTex
auteur
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn 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), Jan 2017, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413221/file/mixed-size.pdf 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. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01417102/file/fpottier-hashtable.pdf BibTex

Other publications

auteur
The Coq Development Team
titre
The Coq Proof Assistant, version 8.7.1
article
Official Release. 2017, pp.1-571. 〈10.5281/zenodo.1133970〉
Accès au bibtex
BibTex
auteur
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier
titre
VOCAL – A Verified OCAml Library
article
ML Family Workshop 2017. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01561094/file/main.pdf BibTex
auteur
Xavier Leroy
titre
How I found a crash bug with hyperthreading in Intel's Skylake processors
article
News article at The Next Web (\url). 2017
Accès au bibtex
BibTex
auteur
Jade Alglave, Luc Maranget, Paul Mckenney, Alan Stern, Andrea Parri
titre
A formal kernel memory-ordering model (Part 1 and 2)
article
Article published in the online magazine "Linux Weekly News" (LWN), available on the web at \url.. 2017
Accès au bibtex
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
https://hal.inria.fr/hal-01669407/file/chunkseq_ml.pdf BibTex

Reports

auteur
Thomas Williams, Didier Rémy
titre
A Principled Approach to Ornamentation in ML
article
[Research Report] RR-9117, Inria. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01628060/file/ornaments-long.pdf BibTex

Preprints, Working Papers, ...

auteur
Gergö Barany
titre
Liveness-Driven Random Program Generation
article
Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthe.. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658563/file/lopstr2017.pdf BibTex
auteur
Markus Raab, Gergö Barany
titre
Introducing Context Awareness in Unmodified, Context-unaware Software
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658638/file/document.pdf BibTex
auteur
Florent Balestrieri, Michel Mauny
titre
Generic Programming in OCAML
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01664286/file/generic.submitted.pdf BibTex

2016

Journal articles

auteur
Umut Acar, Arthur Charguéraud, Mike Rainey
titre
Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages
article
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, 〈10.1017/S0956796816000101〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409069/file/granularity_jfp16.pdf 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), ACM, 2016, 38 (4), pp.94. 〈10.1145/2837022〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246534/file/bpp-mezzo-journal.pdf BibTex
auteur
Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
titre
Testing Noninterference, Quickly
article
Journal of Functional Programming (JFP); Special issue for ICFP 2013, 2016, 26, e4 (62 p.). 〈10.1017/S0956796816000058〉
Accès au bibtex
https://arxiv.org/pdf/1409.0393 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, SAGE Publications, 2016, 〈10.1177/0962280216631763〉
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01298681/file/Riviere_2016_Phase_I-II.pdf 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, Elsevier, 2016, 125, pp.117-133. 〈10.1016/j.cmpb.2015.10.018〉
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01297367/file/packages_CMPB.pdf 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. 9632, pp.727 - 751, 2016, 〈10.1007/978-3-662-49498-1_28〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01408649/file/biglater-conf%20%281%29.pdf 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. 〈http://www.disc-conference.org/wp/disc2016/〉
Accès au bibtex
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, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413241/file/ml-workshop-abstract.pdf BibTex
auteur
Florent Balestrieri, Michel Mauny
titre
Generic Programming in OCaml
article
OCaml 2016 - The OCaml Users and Developers Workshop, Sep 2016, Nara, Japan. OCaml 2016 - The OCaml Users and Developers Workshop, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413061/file/OUD_2016_paper_2.pdf BibTex
auteur
Jacques-Henri Jourdan
titre
Statistically profiling memory in OCaml
article
OCaml 2016, Sep 2016, Nara, Japan. 2016, 〈https://ocaml.org/meetings/ocaml/2016/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406809/file/jourdan2016statistically.pdf 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
https://hal.inria.fr/hal-01352008/file/ocaml2016-opam-builder.pdf 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
https://hal.inria.fr/hal-01352013/file/ocaml-2016-typerex-lint.pdf 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
https://hal.inria.fr/hal-01352015/file/ocaml-2016-learn-ocaml.pdf BibTex
auteur
Ram Raghunathan, Stefan Muller, Umut Acar, Guy 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
https://hal.inria.fr/hal-01416237/file/icfp2016-steel.pdf BibTex
auteur
Umut 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, 2016, 〈10.1145/2951913.2951946〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01409022/file/dag_calculus_icfp16.pdf BibTex
auteur
Jacques-Henri Jourdan
titre
Sparsity Preserving Algorithms for Octagons
article
Isabella Mastroeni. NSAD 2016 - Numerical and symbolic abstract domains workshop , Sep 2016, Edinburgh, United Kingdom. Elsevier, Numerical and symbolic abstract domains, pp.14, 2016, 〈http://nsad16.di.univr.it/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406795/file/jourdan2016sparsity.pdf 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), Jul 2016, Chicago, United States
Accès au bibtex
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. Trends in Functional Programming. 16th International Symposium, TFP 2016, College Park (MD), USA, June 8-10, 2016. Revised Selected Papers (to appear)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413043/file/article.pdf BibTex
auteur
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
titre
Proving Determinacy of the PharOS Real-Time Operating System
article
Michael J. Butler; Klaus-Dieter Schewe; Atif Mashkoor; Miklós Biró. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. Springer, 9675, pp.70-85, 2016, LNCS - Lecture Notes in Computer Science. 〈10.1007/978-3-319-33600-8_4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01322335/file/final.pdf 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, 2016, Proceedings of the 25th International Conference on Compiler Construction (CC 2016). 〈10.1145/2892208.2892224〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01417004/file/fpottier-reachability-cc2016.pdf 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, Jan 2016, Toulouse, France. 〈http://www.erts2016.org/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238879/file/erts2016_compcert.pdf 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
https://hal.inria.fr/hal-01244776/file/top.pdf 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. 2016, 〈http://jfla.inria.fr/2016/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01248101/file/fpottier-reachability-jfla2016.pdf 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
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/tel-01327023/file/thesis.pdf BibTex
auteur
Gabriel Scherer
titre
Which types have a unique inhabitant?
article
Programming Languages [cs.PL]. Université Paris-Diderot, 2016. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01309712/file/scherer-thesis.pdf BibTex

2015

Journal articles

auteur
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
titre
Impossibility of gathering, a certification
article
Information Processing Letters, Elsevier, 2015, 115 (3), pp.447-452. 〈10.1016/j.ipl.2014.11.001〉
Accès au bibtex
https://arxiv.org/pdf/1405.5902 BibTex
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
Verified Compilation of Floating-Point Computations
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. 〈10.1007/s10817-014-9317-x〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862689/file/floating-point-compcert.pdf 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, Japan Informatics Society, 2015, 7 (3), pp.101-114. 〈http://www.infsoc.org/journal/vol07/IJIS_07_3_101-114.pdf〉
Accès au bibtex
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
https://hal-mines-paristech.archives-ouvertes.fr/hal-01204701/file/A-615-v2.pdf 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
https://hal.inria.fr/hal-01245837/file/pdfs_sc15.pdf 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. 2015, OCaml 2015 - The OCaml Users and Developers Workshop
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413319/file/OCaml_2015_submission_3.pdf 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
https://hal.inria.fr/hal-01245844/file/main.pdf 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. The 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), 2015, 〈http://icfpconference.org/icfp2015/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01235596/file/unique_stlc_sums.pdf 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. 2015, 〈10.1007/978-3-319-22102-1_9〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01245872/file/credits_itp15.pdf 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. Springer, 9236, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-22102-1_22〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01162898/file/main.pdf 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
https://hal.inria.fr/hal-01160579/file/principles.pdf BibTex
auteur
Gabriel Scherer
titre
Multi-focusing on extensional rewriting with sums
article
Typed Lambda Calculi and Applications, Jun 2015, Warsaw, Poland. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 2015, 〈http://drops.dagstuhl.de/portals/extern/index.php?semnr=15006〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01235372/file/multifoc_sums-long.pdf BibTex
auteur
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin 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, 2015, 2015 IEEE Symposium on Security and Privacy. 〈10.1109/SP.2015.55〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01265666/file/micro-policies.pdf 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. 32, 2015, Leibniz International Proceedings in Informatics. 〈10.4230/LIPIcs.SNAPL.2015.221〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246360/file/fpottier-protzenko-lessons-mezzo.pdf 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. 9032, pp.406-431, 〈10.1007/978-3-662-46669-8_17〉
Accès au bibtex
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. Proceedings of the 24th European Conference on Programming Languages and Systems, 2015
Accès au bibtex
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. ACM, pp.645--659, 〈10.1145/2694344.2694371〉
Accès au bibtex
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. ACM, pp.247-259, 〈10.1145/2676726.2676966〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01078386/file/verasco-popl2015.pdf BibTex
auteur
François Pottier
titre
Depth-First Search and Strong Connectivity in Coq
article
David Baelde; Jade Alglave. Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. 〈http://jfla.inria.fr/2015〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01096354/file/jfla15_submission_2.pdf BibTex
auteur
Çagdas Bozman, Grégoire Henry, Mohamed Iguernelala, Fabrice Le Fessant, Michel Mauny
titre
ocp-memprof: un profileur mémoire pour OCaml
article
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01099134/file/jfla15_submission_22.pdf BibTex
auteur
Pierre-Évariste Dagand, Gabriel Scherer
titre
Normalization by realizability also evaluates
article
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01099138/file/jfla15_submission_31.pdf BibTex

Directions of work or 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. 〈http://dl.acm.org/citation.cfm?id=2676724〉
Accès au bibtex
BibTex

Other publications

auteur
Luc Maranget, Jade Alglave
titre
Towards a Formalization of the HSA Memory Model in the cat Language
article
HSA Foundation technical and normative document, available at http://www.hsafoundation.com/standa.. 2015, pp.57
Accès au bibtex
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
https://hal.sorbonne-universite.fr/hal-01159890/file/hal.pdf 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
https://hal.inria.fr/hal-01089125/file/psearch.pdf 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), ACM, 2014, 36 (2), pp.7:1--7:74. 〈10.1145/2627752〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081364/file/a7-alglave.pdf BibTex
auteur
Pierre-Évariste  Dagand, Conor  Mcbride
titre
Transporting functions across ornaments
article
Journal of Functional Programming, Cambridge University Press (CUP), 2014, 24 (2-3), pp.67. 〈10.1017/S0956796814000069〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00922581/file/paper_colour.pdf https://hal.inria.fr/hal-00922581/file/paper_bw.pdf 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, Cambridge University Press (CUP), 2014, 24 (1), pp.56-112
Accès au bibtex
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, Springer Verlag, 2014, 53 (3), pp.271-304. 〈10.1007/s10817-014-9306-0〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00881085/file/main.pdf 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
BibTex
auteur
Xavier Leroy
titre
Compiler verification for fun and profit
article
Koen Claessen and Viktor Kuncak. FMCAD 2014 - Formal Methods in Computer-Aided Design, Oct 2014, Lausanne, Switzerland. FMCAD Inc, pp.9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01076547/file/FMCAD14-Leroy.pdf 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
BibTex
auteur
Umut A. Acar, Arthur Charguéraud, Mike Rainey
titre
Theory and Practice of Chunked Sequences
article
Schulz, AndreasS. and Wagner, Dorothea. European Symposium on Algorithms, Sep 2014, Wrocław, Poland. Springer Berlin Heidelberg, Algorithms - ESA 2014, pp.25 - 36, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-662-44777-2_3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01087245/file/chunkedseq.pdf BibTex
auteur
Michel Mauny, Benoît Vaugon
titre
Nullable Type Inference
article
OCaml 2014 - The OCaml Users and Developers Workshop, Sep 2014, Gothenbourg, Sweden. OCaml 2014 - The OCaml Users and Developers Workshop, 〈https://ocaml.org/meetings/ocaml/2014/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413294/file/ocaml2014_14.pdf BibTex
auteur
Fabrice Le Fessant
titre
A Case for Multi-Switch Constraints in OPAM
article
OCaml 2014, Sep 2014, goteborg, Sweden. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091175/file/ocaml2014_12.pdf 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. OCaml 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091173/file/ocaml2014_8.pdf 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. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091177/file/ocaml2014_17.pdf BibTex
auteur
Xavier Leroy
titre
Formal proofs of code generation and verification tools
article
Dimitra Giannakopoulou and Gwen Salaün. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. Springer, 8702, pp.1-4, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-10431-7_1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01059423/file/abstract.pdf 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
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. ACM, 〈10.1145/2628136.2628145〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081233/file/fpottier-elaboration.pdf 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
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. 2014, 〈http://okmij.org/ftp/ML/ML14.html〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094006/file/articheck-ml-workshop-extended-abstract.pdf BibTex
auteur
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
titre
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
article
Christoph Benzmüller and Jens Otten. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. 33, pp.1-16, 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244623/file/final.pdf 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 - Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01063512/file/final.pdf 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. Springer, 8558, pp.543-548, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08970-6_36〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00981212/file/Formal-C-CompCert.pdf BibTex
auteur
Julien Cretin, Didier Rémy
titre
System F with Coercion Constraints
article
Thomas A. Henzinger; Dale Miller. 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. ACM, pp.34, 2014, 〈10.1145/2603088.2603128〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093239/file/Cretin-Remy%21fcc%40lics2014.pdf 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. 2014
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633155/file/goubault2014finding.pdf 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. Springer, 8475, pp.253 - 269, 2014, LNCS. 〈10.1007/978-3-319-07151-0_16〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081194/file/bpp-mezzo.pdf 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, Jun 2014, Edinburg, United Kingdom. pp.40, 〈10.1145/2594291.2594347〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081413/file/p40-alglave.pdf 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. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00983847/file/invited-2.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
Deciding unique inhabitants with sums (work in progress)
article
TYPES, May 2014, Paris, France. 2014, 〈http://www.pps.univ-paris-diderot.fr/types2014/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01094127/file/scherer-types14-extended-abstract.pdf BibTex
auteur
Xavier Leroy
titre
Proof assistants in computer science research
article
IHP thematic trimester on Semantics of proofs and certified mathematics, Apr 2014, Paris, France. 2014
Accès au bibtex
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. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01088655/file/main.pdf 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, Microsoft Research, 2014, TechReport, 〈http://research.microsoft.com/pubs/226237/Luca-Cardelli-Fest-MSR-TR-2014-104.pdf〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093216/file/DidierRemyCoercions.pdf 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
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
https://hal.inria.fr/hal-01093910/file/Scherer-Remy%21fich%40rr2014.pdf 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
https://hal.inria.fr/hal-00934408/file/RR-8456.pdf BibTex

Theses

auteur
Çağdaş Bozman
titre
Profilage mémoire d’applications OCaml
article
Informatique [cs]. ENSTA ParisTech, 2014. Français
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-01122262/file/thesis-cagdas-bozman.pdf 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
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01086106/file/snapshot-0909.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00940511/file/manuscript-final.pdf 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
https://hal.inria.fr/hal-01094120/file/2-or-more-approximation.pdf 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, Cambridge University Press (CUP), 2013, 23 (1), pp.38-144. 〈10.1017/S0956796812000366〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00877589/file/fpottier-ssphs.pdf 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, Cambridge University Press (CUP), 2013, 23 (1), pp.1--54
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772757/file/sikmhs.pdf 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
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS. 〈10.1007/978-3-642-45221-5_20〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909784/file/Zenon-modulo-lpar-19.pdf BibTex
auteur
Gabriel Scherer, Jan Hoffmann
titre
Tracking Data-Flow with Open Closure Types
article
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR- 19th International Conference Logic for Programming, Artificial Intelligence, and Reasoning, Dec 2013, Stellenbosch, South Africa. Springer Verlag, 8312, pp.710-726, 2013, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00911656/file/closures.pdf 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
Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00909688/file/zenon-modulo-iwil-2013.pdf 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, 2013, 〈10.1145/2500365.2500606〉
Accès au bibtex
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, 2013, 〈10.1145/2500365.2500598〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00877590/file/pottier-protzenko-mezzo.pdf BibTex
auteur
Thomas Braibant, Jacques-Henri Jourdan, David Monniaux
titre
Implementing hash-consed structures in Coq
article
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. Interactive Theorem Proving, 4th international conference, Jul 2013, Rennes, France. Springer, 7998, pp.477-483, 2013, Lecture notes in computer science. 〈10.1007/978-3-642-39634-2_36〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00816672/file/Braibant_Jourdan_Monniaux_ITP2013.pdf BibTex
auteur
Thomas Braibant, Adam Chlipala
titre
Formal Verification of Hardware Synthesis
article
Natasha Sharygina and Helmut Veith. Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. Springer, 8044, pp.213-228, 2013, Lecture notes in computer science. 〈10.1007/978-3-642-39799-8_14〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00776876/file/main.pdf BibTex
auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
article
Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. IEEE, pp.107-115, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00743090/file/article.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
GADTs meet subtyping
article
Matthias Felleisen and Philippa Gardner. ESOP 2013 - 22nd European Symposium on Programming, Mar 2013, Rome, Italy. Springer, 7792, pp.554-573, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-37036-6〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00772993/file/esop.pdf BibTex
auteur
Jacques Garrigue, Didier Rémy
titre
Ambivalent Types for Principal Type Inference with GADTs
article
Chung-chieh Shan. APLAS 2013 - 11th Asian Symposium on Programming Languages and Systems, 2013, Melbourne, Australia. 8301, pp.257-272, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-319-03542-0_19〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00914560/file/Garrigue-Remy_gadts_applas2013.pdf BibTex

Reports

auteur
Umut 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
https://hal.inria.fr/hal-00910130/file/main.pdf 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
https://hal.inria.fr/hal-00851658/file/RR-8345.pdf 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
https://hal.inria.fr/hal-00914493/file/Garrigue-Remy_gadts_long2013.pdf 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
https://arxiv.org/pdf/1311.7256 BibTex
auteur
Jonathan Protzenko
titre
Illustrating the Mezzo programming language
article
2013
Accès au bibtex
https://arxiv.org/pdf/1311.6929 BibTex

2012

Journal articles

auteur
Nicolas Pouillard, François Pottier
titre
A unified treatment of syntax with binders
article
Journal of Functional Programming, Cambridge University Press (CUP), 2012, 22 (4--5), pp.614--704. 〈10.1017/S0956796812000251〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772721/file/pouillard-pottier-unified.pdf BibTex
auteur
Didier Rémy, Boris Yakobowski
titre
A Church-Style Intermediate Language for MLF
article
Theoretical Computer Science, Elsevier, 2012, 435, pp.77--105. 〈http://dx.doi.org/10.1016/j.tcs.2012.02.026〉. 〈10.1016/j.tcs.2012.02.026〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093719/file/xmlf%40tcs2011.pdf BibTex
auteur
Andrew Appel, Robert Dockins, Xavier Leroy
titre
A list-machine benchmark for mechanized metatheory
article
Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. 〈10.1007/s10817-011-9226-1〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00674176/file/listmachine-journal.pdf BibTex
auteur
Gregor Goessler, Dana Xu, Alain Girault
titre
Probabilistic contracts for component-based design
article
Formal Methods in System Design, Springer Verlag, 2012, 41 (2), pp.211-231. 〈10.1007/s10703-012-0162-4〉
Accès au bibtex
BibTex

Conference papers

auteur
Valentin Robert, Xavier Leroy
titre
A formally-verified alias analysis
article
Hawblitzel, Chris and Miller, Dale. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.11-26, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35308-6_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00773109/file/alias-analysis.pdf 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. 7705, pp.386-388, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35182-2_27〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01079337/file/mechanized-semantics-aplas-cpp-2012.pdf 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
https://hal.inria.fr/hal-01092204/file/extended-abstract.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
GADTs Meet Subtyping
article
ACM SIGPLAN Workshop on ML, Sep 2012, Copenhagen, Denmark. 2012, 〈http://www.lexifi.com/ml2012/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093816/file/Scherer-Remy%3Agadts-subtyping%40ml2012.pdf BibTex
auteur
Jacques Garrigue, Didier Rémy
titre
Tracing ambiguity in GADT type inference
article
ACM SIGPLAN Workshop on ML, Sep 2012, copenhagen, Denmark. 2012, 〈http://www.lexifi.com/ml2012/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093845/file/Garrigue-Remy%3Agadts%40ml2012.pdf BibTex
auteur
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
titre
TLA+ Proofs
article
Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, 7436, pp.147-154, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32759-9_14〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00726631/file/final.pdf BibTex
auteur
Gabriel Scherer, Didier Rémy
titre
GADT meet subtyping
article
ACM SIGPLAN Workshop on ML, Aug 2012, Copenhague, Denmark. 2012, 〈http://www.lexifi.com/ml2012/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093940/file/scherer_remy_gadts_variance_ml_workshop_extended_abstract.pdf 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., 2012, 〈http://arxiv.org/abs/1208.5933〉
Accès au bibtex
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. ACM, 2012, 〈10.1145/2336717.2336726〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00773654/file/DJR.pdf 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. Springer, 7211, pp.397-416, Lecture Notes in Computer Science. 〈10.1007/978-3-642-28869-2_20〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01077321/file/validated-parser.pdf 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, Feb 2012, Toulouse, France. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00653367/file/erts2012.pdf 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, Jan 2012, Philadelphia, PA, United States. pp.521-532, 2012, 〈10.1145/2103656.2103718〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00674663/file/cpp-construction.pdf 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, Jan 2012, Philadelphia, United States. ACM, 2012, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 〈10.1145/2103656.2103699〉
Accès au bibtex
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. ACM, pp.107-116, 〈10.1145/2103746.2103767〉
Accès au bibtex
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
https://hal.inria.fr/hal-00744292/file/RR-8114.pdf BibTex
auteur
Gregor Gössler, Dana 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
https://hal.inria.fr/inria-00507785/file/RR-7328.pdf BibTex
auteur
Xavier Leroy, Andrew 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
https://hal.inria.fr/hal-00703441/file/RR-7987.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00759059/file/PhD-thesis-latest.pdf 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
https://tel.archives-ouvertes.fr/tel-00769044/file/PhD-Ramananandro.pdf BibTex

2011

Journal articles

auteur
Xavier Leroy
titre
Safety First! (technical perspective)
article
Communications of the ACM, ACM, 2011, 54 (12), pp.122. 〈10.1145/2043174.2043196〉
Accès au bibtex
BibTex

Conference papers

auteur
Nicolas Pouillard
titre
Nameless, Painless
article
ICFP 2011: 16th International Conference on Functional Programming, Sep 2011, Tokyo, Japan. ACM, pp.320-332, 〈10.1145/2034773.2034817〉
Accès au bibtex
BibTex
auteur
Pascal Cuoq, Julien Signoles, Damien Doligez
titre
Lightweight Typed Customizable Unmarshaling
article
ACM SIGPLAN Workshop on ML, Sep 2011, Tokyo, Japan. 〈http://conway.rutgers.edu/ml2011/〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091947/file/unmarshal-final.pdf 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. IEEE, 〈10.1109/CGO.2011.5764668〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091800/file/abstract.pdf 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. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 18, pp.59-68, 2011, OpenAccess Series in Informatics. 〈10.4230/OASIcs.PPES.2011.59〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00551370/file/pppes2011_2112.pdf 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. ACM, pp.1-2, 〈10.1145/1926385.1926387〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01076682/file/popl11-invited-talk.pdf 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, Jan 2011, Austin, TX, United States. ACM Press, pp.67-79, 2011, 〈10.1145/1926385.1926395〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00674174/file/cpp-object-layout.pdf 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
https://hal.inria.fr/hal-01081187/file/fpottier-fork.pdf 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. 2011, 〈10.1145/1929553.1929565〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01081193/file/pilkiewicz-pottier-monotonicity.pdf 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
https://hal.inria.fr/inria-00582570/file/RR-7587.pdf 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
https://hal.inria.fr/hal-00644156/file/RR-7794.pdf BibTex

2010

Journal articles

auteur
Xavier Leroy
titre
Comment faire confiance à un compilateur ?
article
Interstices, INRIA, 2010, 〈https://interstices.info/jcms/n_52365/comment-faire-confiance-a-un-compilateur〉
Accès au bibtex
BibTex
auteur
Xavier Leroy
titre
Comment faire confiance à un compilateur ?
article
Les Cahiers de l'INRIA - La Recherche, INRIA, 2010, Cancer la révolution
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00511377/file/inria-n440-avril10.pdf 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. Springer, pp.325-340, 2010, 〈10.1007/978-3-642-15643-4_24〉
Accès au bibtex
BibTex
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
titre
The TLA+ Proof System: Building a Heterogeneous Verification Platform
article
Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, 6255, pp.44, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14808-8_3〉
Accès au bibtex
BibTex
auteur
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
titre
Verifying Safety Properties With the TLA+ Proof System
article
Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-14203-1_12〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534821/file/tlaps.pdf BibTex
auteur
Silvain Rideau, Xavier Leroy
titre
Validating register allocation and spilling
article
Compiler Construction 2010, Mar 2010, Paphos, Cyprus. Springer, 6011, pp.224-243, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-11970-5_13〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00529841/file/validation-regalloc.pdf BibTex
auteur
Jean-Baptiste Tristan, Xavier Leroy
titre
A simple, verified validator for software pipelining
article
ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain. 2010, 〈10.1145/1706299.1706311〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00529836/file/validation-softpipe.pdf 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
https://hal.inria.fr/inria-00529848/file/notes.pdf 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
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-00550331/file/montagu_thesis.pdf BibTex

2009

Journal articles

auteur
Xavier Leroy
titre
A formally verified compiler back-end
article
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. 〈10.1007/s10817-009-9155-4〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00360768/file/paper2.pdf BibTex
auteur
Zaynah Dargaye, Xavier Leroy
titre
A verified framework for higher-order uncurrying optimizations
article
Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (3), 〈10.1007/s10990-010-9050-z〉
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01499915/file/higher-order-uncurrying.pdf BibTex
auteur
Xavier Leroy
titre
Formal verification of a realistic compiler
article
Communications- ACM, Association for Computing Machinery, 2009, 52 (7), pp.107-115. 〈10.1145/1538788.1538814〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00415861/file/compcert-CACM.pdf BibTex
auteur
Didier Le Botlan, Didier Rémy
titre
Recasting MLF
article
Information and Computation, Elsevier, 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
https://hal.inria.fr/inria-00156628/file/recasting-mlf-RR.pdf BibTex
auteur
Xavier Leroy, Hervé Grall
titre
Coinductive big-step operational semantics
article
Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. 〈10.1016/j.ic.2007.12.004〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00309010/file/leroy-grall.pdf 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, Springer Verlag, 2009, 22 (1), pp.3-66. 〈10.1007/s10990-009-9042-z〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00359213/file/letrec.pdf BibTex
auteur
Sandrine Blazy, Xavier Leroy
titre
Mechanized semantics for the Clight subset of the C language
article
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (3), pp.263-288. 〈10.1007/s10817-009-9148-3〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00352524/file/paper.pdf 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), Jun 2009, Dublin, Ireland. 2009
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00387749/file/LCTES09.pdf 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. ACM, pp.316-326, 2009, 〈10.1145/1542476.1542512〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00415865/file/validation-LCM.pdf BibTex

Theses

auteur
Benoit Razet
titre
Machines d'Eilenberg Effectives
article
Informatique [cs]. Université Paris-Diderot - Paris VII, 2009. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00463049/file/these.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00437582/file/dissertation_english.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00452440/file/these_Zaynah_Dargaye.pdf BibTex

2008

Journal articles

auteur
Laurence Rideau, Bernard Serpette, Xavier Leroy
titre
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
article
Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. 〈10.1007/s10817-007-9096-8〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289709/file/parallel-move.pdf 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, Springer Verlag, 2008, 41 (1), pp.1-31. 〈10.1007/s10817-008-9099-0〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289542/file/memory-model-journal.pdf 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. Trusting Trusted Computing ?, pp.162-179, 2008
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01125667/file/cesar.pdf 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. Springer, 5133, pp.305--335, 2008, Lecture notes in computer scinece. 〈10.1007/978-3-540-70594-9_17〉
Accès au bibtex
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
Presses Universitaires de l'Université Blaise Pascal. ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, Feb 2008, Clermont-Ferrand, France. pp.123-138, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00260712/file/ROADEF08.pdf 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), Jan 2008, San Francisco, United States. ACM Press, pp.17-27, 2008, 〈10.1145/1328438.1328444〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289540/file/validation-scheduling.pdf 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), Jan 2008, Etretat, France. pp.63-78, 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00202817/file/yakobowski.pdf 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. 2008
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338299/file/main.pdf BibTex

Directions of work or proceedings

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
https://hal.inria.fr/inria-00202715/file/actes_avec_couverture.pdf 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
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00357708/file/these-finale-english.pdf https://tel.archives-ouvertes.fr/tel-00357708/file/these-finale-francais.pdf BibTex

Preprints, Working Papers, ...

auteur
Julien Brunel, Damien Doligez, René Hansen, Julia Lawall, Gilles Muller
titre
A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
article
EMN 08/2/INFO. pp16. 2008
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00297708/file/EMN_INFO_02_8.pdf 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, Lavoisier, 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
https://hal.inria.fr/inria-00292049/file/TSIchronique_sansentete.pdf 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, 2007
Accès au bibtex
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. Springer, 4790, pp.211-225, 2007, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-540-75560-9_17〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289541/file/cps-dargaye-leroy.pdf 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. Springer, 4790, pp.151-165, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-75560-9_13〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00315920/file/bonichon-delahaye-doligez-lpar-2007.pdf BibTex
auteur
Andrew W. Appel, Sandrine Blazy
titre
Separation Logic for Small-step Cminor
article
Springer-Verlag. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. 4732, pp.5-21, 2007, Lecture Notes in Computer Science
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165915/file/paperTPHOL.pdf BibTex
auteur
Zaynah Dargaye
titre
Décurryfication certifiée
article
Pierre-Etienne Moreau et Sandrine Blazy. Journées Francophones des Langages Applicatifs (JFLA 2007), Jan 2007, Aix-les-Bains, France. INRIA, pp.119-134, 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00338974/file/dargaye.pdf BibTex
auteur
Sandrine Blazy
titre
Experiments in validating formal semantics for C
article
C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp.95-102, 2007
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00292043/file/C07Blazy.pdf 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
https://hal.inria.fr/inria-00126895/file/RR-6107.pdf 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
https://hal.inria.fr/inria-00123945/file/RR-6098.pdf BibTex

Preprints, Working Papers, ...

auteur
Laurence Rideau, Bernard 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
https://hal.inria.fr/inria-00176007/file/pmov.pdf BibTex

2006

Conference papers

auteur
Andrew 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. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2007.01.020〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289543/file/listmachine-lfmtp.pdf BibTex
auteur
Xavier Leroy
titre
Coinductive big-step operational semantics
article
Peter Sestoft. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. Springer, 3924, pp.42-54, 2006, Lecture Notes in Computer Science. 〈10.1007/11693024_5〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289545/file/coindsem.pdf 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. ACM Press, pp.42--54, 2006, 〈10.1145/1111037.1111042〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00000963/file/compiler-certif.pdf BibTex

Reports

auteur
Andrew 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
https://hal.inria.fr/inria-00077531/file/RR-5914.pdf 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), ACM, 2005, 27 (5), pp.857 - 881. 〈10.1145/1086642.1086644〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310317/file/cmsv-long.pdf 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. 2005
Accès au bibtex
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. 2005, Joint ICALP-PPDP keynote talk
Accès au bibtex
BibTex
auteur
Giuseppe Castagna, Dario Colazzo, Alain Frisch
titre
Error Mining for Regular Expression Patterns
article
2005, Springer, pp.160-172, 2005, n. 3701, LNCS
Accès au bibtex
BibTex
auteur
Haruo Hosoya, Alain Frisch, Giuseppe Castagna
titre
Parametric Polymorphism for XML
article
2005, ACM Press, pp.50-62, 2005
Accès au bibtex
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. Springer, 3839, pp.66-81, 2006, Lecture Notes in Computer Science. 〈10.1007/11617990〉
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00289549/file/proofs_dataflow_optimizations.pdf 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. Springer, 2986, pp.64-78, 2004, Lecture Notes in Computer Science. 〈10.1007/b96702〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310123/file/cbv-mixins.pdf 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. Springer, 2305, pp.207-236, 2002, Lecture Notes in Computer Science. 〈10.1007/3-540-45927-8〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00310119/file/mixins-cbv-esop2002.pdf BibTex