chargueraud.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc chargueraud.cite -ob chargueraud.bib -c 'author : "Charguéraud"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@inproceedings{chargueraud08icfp,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Functional Translation of a Calculus of Capabilities},
  booktitle = {{ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP)},
  month = sep,
  year = {2008},
  pages = {213--224},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilities.pdf},
  doi = {10.1145/1411204.1411235},
  abstract = {Reasoning about imperative programs requires the
                 ability to track aliasing and ownership properties. We
                 present a type system that provides this ability, by
                 using regions, capabilities, and singleton types. It is
                 designed for a high-level calculus with higher-order
                 functions, algebraic data structures, and references
                 (mutable memory cells). The type system has
                 polymorphism, yet does not require a value restriction,
                 because capabilities act as explicit store typings.\par
                 We exhibit a type-directed, type-preserving, and
                 meaning-preserving translation of this imperative
                 calculus into a pure calculus. Like the monadic
                 translation, this is a store-passing translation. Here,
                 however, the store is partitioned into multiple
                 fragments, which are threaded through a computation
                 only if they are relevant to it. Furthermore, the
                 decomposition of the store into fragments can evolve
                 dynamically to reflect ownership transfers.\par The
                 translation offers deep insight about the inner
                 workings and soundness of the type system. If coupled
                 with a semantic model of its target calculus, it leads
                 to a semantic model of its imperative source calculus.
                 Furthermore, it provides a foundation for our long-term
                 objective of designing a system for specifying and
                 certifying imperative programs with dynamic memory
                 allocation.}
}
@phdthesis{chargueraud10these,
  author = {Arthur Chargu\'eraud},
  title = {Characteristic Formulae for Mechanized Program Verification},
  school = {Universit\'e Paris 7},
  year = 2010,
  note = {\url{http://www.chargueraud.org/arthur/research/2010/thesis/}}
}
@inproceedings{chargueraud11icfp,
  author = {Arthur Chargu{\'e}raud},
  title = {Characteristic formulae for the verification of imperative
               programs},
  year = 2011,
  pages = {418-430},
  editor = {Manuel M. T. Chakravarty and
               Zhenjiang Hu and
               Olivier Danvy},
  booktitle = {Proceeding of the 16th ACM SIGPLAN international conference
               on Functional Programming (ICFP)},
  address = {Tokyo, Japan},
  month = {September},
  publisher = {ACM}
}
@article{chargueraud-pottier-uf-sltc-17,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Verifying the Correctness and Amortized Complexity of
                 a Union-Find Implementation in Separation Logic with
                 Time Credits},
  journal = {Journal of Automated Reasoning},
  month = mar,
  year = {2019},
  volume = {62},
  number = {3},
  pages = {331--365},
  pdf = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf},
  off = {http://rdcu.be/v7EN},
  soft = {http://gallium.inria.fr/~fpottier/dev/uf},
  abstract = {Union-Find is a famous example of a simple data
                 structure whose amortized asymptotic time complexity
                 analysis is nontrivial. We present a Coq formalization
                 of this analysis, following Alstrup et al.'s recent
                 proof (2014). Moreover, we implement Union-Find as an
                 OCaml library and formally endow it with a modular
                 specification that offers a full functional correctness
                 guarantee as well as an amortized complexity bound. In
                 order to reason in Coq about imperative OCaml code, we
                 use the CFML tool, which implements Separation Logic
                 for a subset of OCaml, and which we extend with time
                 credits. Although it was known in principle that
                 amortized analysis can be explained in terms of time
                 credits and that time credits can be viewed as
                 resources in Separation Logic, we believe our work is
                 the first practical demonstration of this approach.
                 Finally, in order to explain the meta-theoretical
                 foundations of our approach, we define a Separation
                 Logic with time credits for an untyped call-by-value
                 lambda-calculus, and formally verify its soundness.}
}
@inproceedings{gueneau18esop,
  title = {A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification},
  author = {Gu{\'e}neau, Arma{\"e}l and Chargu{\'e}raud, Arthur and Pottier, Fran\c{c}ois},
  booktitle = {ESOP 2018 - 27th European Symposium on Programming},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 10801,
  year = 2018,
  doi = {10.1007/978-3-319-89884-1\_19}
}
@inproceedings{chargueraud13esop,
  author = {Arthur Chargu{\'e}raud},
  title = {Pretty-Big-Step Semantics},
  booktitle = {Proceedings of the 22nd European Symposium on Programming},
  month = mar,
  year = 2013,
  volume = {7792},
  editor = {Matthias Felleisen and Philippa Gardner},
  pages = {41--60},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  hal = {http://hal.inria.fr/hal-00798227},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ESOP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{chargueraud13ppopp,
  author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
  title = {Scheduling parallel programs by work stealing with private deques},
  booktitle = {Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
  month = feb,
  year = 2013,
  series = {PPoPP '13},
  pages = {219-228},
  publisher = {ACM Press},
  doi = {10.1145/2442516.2442538},
  hal = {http://hal.inria.fr/hal-00863028},
  topics = {team,lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {PPOPP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@inproceedings{bodin14popl,
  hal = {http://hal.inria.fr/hal-00910135},
  topics = {team},
  author = {M. Bodin and A. Chargu{\'e}raud and D. Filaretti and P. Gardner and S. Maffeis and D. Naudziuniene and A. Schmitt and G. Smith},
  title = {A Trusted Mechanised {JavaScript} Specification},
  crossref = {popl2014}
}
@inproceedings{acar-chargueraud-rainey-12-primitives,
  author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
  title = {Efficient Primitives for Creating and Scheduling Parallel Computations},
  year = {2012},
  month = {January},
  booktitle = {Declarative Aspects and Applications of Multicore Programming (DAMP)}
}
@inproceedings{acar-chargueraud-rainey-11-oracle,
  author = {Umut A. Acar and Arthur Chargu{\'e}raud and Mike Rainey},
  title = {Oracle Scheduling: Controlling Granularity in Implicitly Parallel Languages},
  year = {2011},
  month = {October},
  url = {http://arthur.chargueraud.org/research/2011/oracle},
  pages = {499-518},
  editor = {Cristina Videira Lopes and Kathleen Fisher},
  booktitle = {Proceedings of the 26th Annual ACM SIGPLAN Conference on
               Object-Oriented Programming, Systems, Languages, and Applications,
               ({OOPSLA})},
  publisher = {ACM}
}
@techreport{acar13rr,
  hal = {http://hal.inria.fr/hal-00910130},
  title = {Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Muller, Stefan and Rainey, Mike},
  abstract = {We present a work-stealing algorithm for total-store memory architectures, such as Intel's X86, that does not rely on atomic read-modify-write instructions such as compare-and-swap. In our algorithm, processors communicate solely by reading from and writing (non-atomically) into weakly consistent memory. We also show that join resolution, an important problem in scheduling parallel programs, can also be solved without using atomic read-modify-write instructions. At a high level, our work-stealing algorithm closely resembles traditional work-stealing algorithms, but certain details are more complex. Instead of relying on atomic read-modify-write operations, our algorithm uses a steal protocol that enables processors to perform load balancing by using only two memory cells per processor. The steal protocol permits data races but guarantees correctness by using a time-stamping technique. Proving the correctness of our algorithms is made challenging by weakly consistent shared-memory that permits processors to observe sequentially inconsistent views. We therefore carefully specify our algorithms and prove them correct by considering a costed refinement of the X86-TSO model, a precise characterization of total-store-order architectures. We show that our algorithms are practical by implementing them as part of a C++ library and performing an experimental evaluation. Our results show that our work-stealing algorithm is competitive with the state-of-the-art implementations even on current architectures where atomic read-modify-write instructions are cheap. Our join resolution algorithm incurs a relatively small overhead compared to an efficient algorithm that uses atomic read-modify-write instructions.},
  institution = {HAL},
  type = {Research Report},
  year = 2013,
  month = sep
}
@inproceedings{acar14esa,
  topics = {team},
  title = {Theory and Practice of Chunked Sequences},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01087245},
  booktitle = {European Symposium on Algorithms},
  address = {Wroclaw, Poland},
  editor = {Schulz, AndreasS. and Wagner, Dorothea},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 8737,
  pages = {25--36},
  year = 2014,
  month = sep,
  doi = {10.1007/978-3-662-44777-2_3},
  keywords = {Data structure ;  Sequence ;  Chunk ;  Amortization}
}
@techreport{acar15rr,
  topics = {team},
  title = {Fast Parallel Graph-Search with Splittable and Catenable Frontiers},
  author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01089125},
  type = {Technical Report},
  institution = {Inria},
  year = 2015,
  month = jan
}
@inproceedings{chargueraud:hal-01245872,
  topics = {team},
  title = {{Machine-Checked Verification of the Correctness and Amortized
                  Complexity of an Efficient Union-Find Implementation}},
  author = {Chargu\'eraud, Arthur and Pottier, Fran\c{c}ois},
  booktitle = {{6th International Conference on Interactive Theorem Proving
                  (ITP)}},
  address = {Nanjing, China},
  year = 2015,
  month = aug,
  doi = {10.1007/978-3-319-22102-1\_9},
  hal = {https://hal.inria.fr/hal-01245872},
  pdf = {https://hal.inria.fr/hal-01245872/document},
  hal_id = {hal-01245872},
  hal_version = {v1},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@inproceedings{acar:hal-01245837,
  topics = {team},
  title = {{A Work-Efficient Algorithm for Parallel Unordered Depth-First
                  Search}},
  author = {Acar, Umut A. and Chargu\'eraud, Arthur and Rainey, Mike},
  booktitle = {{Proceedings of the International Conference for High Performance
                  Computing, Networking, Storage and Analysis}},
  address = {Austin, Texas, United States},
  year = {2015},
  month = nov,
  doi = {10.1145/2807591.2807651},
  hal = {https://hal.inria.fr/hal-01245837},
  pdf = {https://hal.inria.fr/hal-01245837/document},
  hal_id = {hal-01245837},
  hal_version = {v1},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-invited-conference = {no},
  x-scientific-popularization = {no}
}
@inproceedings{chargueraud:hal-01245865,
  topics = {team},
  title = {{Higher-Order Representation Predicates in Separation Logic}},
  author = {Chargu{\'e}raud, Arthur},
  hal = {https://hal.inria.fr/hal-01245865},
  booktitle = {{Proceedings of the 5th ACM SIGPLAN Conference on Certified
                  Programs and Proofs}},
  address = {Saint Petersburg, Florida, United States},
  year = {2016},
  month = jan,
  hal_id = {hal-01245865},
  hal_version = {v1}
}
@misc{cfpp17,
  topics = {team},
  author = {Arthur Chargu{\'e}raud and Jean-Christophe Filli{\^a}tre and
                  M{\'a}rio Pereira and Fran\c{c}ois Pottier},
  title = {{VOCAL} -- {A} {V}erified {OC}aml {L}ibrary},
  howpublished = {ML Family Workshop},
  month = {September},
  year = {2017},
  hal = {https://hal.inria.fr/hal-01561094}
}
@inproceedings{acar:hal-01409022,
  topics = {team},
  title = {Dag-calculus: a calculus for parallel computation},
  author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike and Sieczkowski, Filip},
  hal = {https://hal.inria.fr/hal-01409022},
  booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP)},
  address = {Nara, Japan},
  pages = {18--32},
  year = 2016,
  month = sep,
  doi = {10.1145/2951913.2951946}
}
@article{acar:hal-01409069,
  topics = {team},
  title = {Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages},
  author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike},
  hal = {https://hal.inria.fr/hal-01409069},
  journal = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  volume = 26,
  year = 2016,
  month = nov,
  doi = {10.1017/S0956796816000101}
}
@inproceedings{gospelfm19,
  topics = {team},
  crossref = {fm19},
  author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Belo Louren\c{c}o and M\'ario Pereira},
  title = {{GOSPEL} --- Providing {OCaml} with a Formal Specification Language},
  hal = {https://hal.inria.fr/hal-02157484}
}
@proceedings{popl2014,
  title = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = 2014,
  booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  address = {San Diego, USA},
  month = jan,
  publisher = {ACM Press}
}
@proceedings{fm19,
  title = {FM 2019 23rd International Symposium on Formal Methods},
  booktitle = {FM 2019 23rd International Symposium on Formal Methods},
  month = oct,
  year = 2019,
  address = {Porto, Portugal},
  editor = {Annabelle McIver and Maurice ter Beek}
}