|
[1]
|
Umut Acar, Vitaly Aksenov, Arthur Charguéraud, and Mike Rainey.
Provably and practically efficient granularity control.
In PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles
and Practice of Parallel Programming, pages 213--228. ACM Press, 2019.
[ bib |
HAL archive |
At publisher's ]
|
|
[2]
|
Cagdas Bozman, Benjamin Canou, Roberto Di Cosmo, Pierrick Couderc, Louis
Gesbert, Grégoire Henry, Fabrice le Fessant, Michel Mauny, Carine Morel,
and Loïc Peyrot.
Learn-OCaml : un assistant à l'enseignement d'OCaml.
In Journées Francophones des Langages Applicatifs (JFLA),
January 2019.
[ bib |
HAL archive ]
|
|
[3]
|
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and
François Pottier.
Formal proof and analysis of an incremental cycle detection
algorithm.
In ITP 2019, 10th Conference on Interactive Theorem Proving,
volume 141 of Leibniz International Proceedings in Informatics
(LIPIcs), pages 18:1--18:20. Schloss Dagstuhl--Leibniz-Zentrum fuer
Informatik, September 2019.
[ bib |
HAL archive |
At publisher's ]
|
|
[4]
|
Glen Mével, Jacques-Henri Jourdan, and François Pottier.
Time credits and time receipts in Iris.
In Luis Caires, editor, European Symposium on Programming
(ESOP), volume 11423 of Lecture Notes in Computer Science, pages
1--27. Springer, April 2019.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Umut A. Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, and Filip
Sieczkowski.
Heartbeat scheduling: provable efficiency for nested parallelism.
In PLDI 2018: 39th ACM Conference on Programming Language Design
and Implementation, pages 769--782. ACM, 2018.
[ bib |
Local copy |
At publisher's ]
|
|
[2]
|
Vitalii Aksenov, Umut A. Acar, Arthur Charguéraud, and Mike Rainey.
Poster: Performance challenges in modular parallel programs.
In PPoPP 2018: 23rd ACM SIGPLAN Annual Symposium on Principles
and Practice of Parallel Programming, February 2018.
[ bib |
DOI |
HAL archive |
At publisher's ]
|
|
[3]
|
Vitalii Aksenov, Dan Alistarh, and Petr Kuznetsov.
Brief announcement: Performance prediction for coarse-grained
locking.
In PODC 2018 -- ACM Symposium on Principles of Distributed
Computing, July 2018.
[ bib |
DOI |
HAL archive ]
|
|
[4]
|
Jade Alglave, Luc Maranget, Paul McKenney, Andrea Parri, and Alan Stern.
Frightening small children and disconcerting grown-ups: Concurrency
in the Linux kernel.
In ASPLOS2018 - 23rd ACM International Conference on
Architectural Support for Programming Languages and Operating Systems, pages
405--418. ACM Press, 2018.
[ bib |
HAL archive |
At publisher's ]
|
|
[5]
|
Gergö Barany.
Finding missed compiler optimizations by differential testing.
In 27th International Conference on Compiler Construction,
Vienna, Austria, February 2018.
[ bib |
HAL archive |
At publisher's ]
|
|
[6]
|
Gergö Barany.
A more precise, more correct stack and register model for CompCert.
In LOLA 2018 - Syntax and Semantics of Low-Level Languages
2018, Oxford, United Kingdom, July 2018.
[ bib |
HAL archive ]
|
|
[7]
|
Armaël Guéneau, Arthur Charguéraud, and François
Pottier.
A fistful of dollars: Formalizing asymptotic complexity claims via
deductive program verification.
In ESOP 2018: Programming Languages and Systems - 27th European
Symposium on Programming, volume 10801 of Lecture Notes in Computer
Science, pages 533--560. Springer, 2018.
[ bib |
At publisher's ]
|
|
[8]
|
Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard
Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine
Blazy.
CompCert: Practical experience on integrating and qualifying a
formally verified optimizing compiler.
In ERTS 2018: Embedded Real Time Software and Systems. SEE,
January 2018.
[ bib |
HAL archive ]
|
|
[9]
|
Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael
Schmidt, and Simon Wegener.
Embedded program annotations for WCET analysis.
In WCET 2018: 18th International Workshop on Worst-Case
Execution Time Analysis, volume 63 of OpenAccess Series in Informatics
(OASIcs), pages 8:1--8:13. Schloss Dagstuhl--Leibniz-Zentrum fuer
Informatik, July 2018.
[ bib |
HAL archive |
At publisher's ]
|
|
[1]
|
Umut A Acar, Naama Ben-David, and Mike Rainey.
Contention in structured concurrency: Provably efficient dynamic
non-zero indicators for nested parallelism.
In PPoPP 2017: 22nd ACM SIGPLAN Symposium on Principles and
Practice of Parallel Programming, February 2017.
[ bib |
DOI |
HAL archive ]
|
|
[2]
|
Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc
Pouzet, and Lionel Rieg.
A formally verified compiler for Lustre.
In PLDI 2017 - 38th ACM SIGPLAN Conference on Programming
Language Design and Implementation, Barcelona, Spain, June 2017. ACM.
[ bib |
HAL archive |
At publisher's ]
|
|
[3]
|
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and
François Pottier.
VOCAL -- A Verified OCAml Library.
In ML Family Workshop 2017. ACM, September 2017.
[ bib |
HAL archive ]
|
|
[4]
|
Arthur Charguéraud and François Pottier.
Temporary read-only permissions for separation logic.
In Hongseok Yang, editor, ESOP 2017: Proceedings of the European
Symposium on Programming, volume 10201 of Lecture Notes in Computer
Science, pages 260--286. Springer, April 2017.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[5]
|
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget,
Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell.
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC.
In POPL 2017: 44th ACM SIGPLAN Symposium on Principles of
Programming Languages, pages 429--442, January 2017.
[ bib |
DOI |
HAL archive ]
|
|
[6]
|
Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael
Schmidt, and Christian Ferdinand.
Closing the gap -- the formally verified optimizing compiler
CompCert.
In SSS 2017: Safety-critical Systems Symposium 2017, February
2017.
[ bib |
HAL archive ]
|
|
[7]
|
François Pottier.
Verifying a hash table and its iterators in higher-order separation
logic.
In CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on
Certified Programs and Proofs, pages 3--16, January 2017.
[ bib |
DOI |
HAL archive ]
|
|
[1]
|
Umut Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski.
Dag-calculus: A calculus for parallel computation.
In ICFP 2016: 21st International Conference on Functional
Programming. ACM Press, 2016.
[ bib |
Local copy ]
|
|
[2]
|
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, and Stephan Merz.
Proving determinacy of the PharOS real-time operating system.
In ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z
- 5th International Conference, volume 9675 of LNCS, pages 70--85.
Springer, May 2016.
[ bib |
DOI |
Local copy ]
|
|
[3]
|
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc
Maranget, Will Deacon, and Peter Sewell.
Modelling the ARMv8 architecture, operationally: Concurrency and
ISA.
In POPL 2016: ACM Symposium on Principles of Programming
Languages. ACM Press, 2016.
[ bib |
HAL archive ]
|
|
[4]
|
Jacques-Henri Jourdan.
Sparsity preserving algorithms for octagons.
In NSAD 2016: Numerical and symbolic abstract domains workshop
, page 14. Elsevier, September 2016.
[ bib |
HAL archive ]
|
|
[5]
|
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus
Pister, and Christian Ferdinand.
Compcert -- a formally verified optimizing compiler.
In ERTS 2016: Embedded Real Time Software and Systems. SEE,
2016.
[ bib |
HAL archive |
Local copy ]
|
|
[6]
|
François Pottier.
Reachability and error diagnosis in LR(1) parsers.
In CC 2016: 25th International Conference on Compiler
Construction, pages 88--98. ACM, 2016.
[ bib |
At publisher's ]
|
|
[7]
|
Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal.
Transfinite step-indexing: Decoupling concrete and logical steps.
In ESOP 2016: Programming Languages and Systems, 25th European
Symposium on Programming, volume 9632 of Lecture Notes in Computer
Science, pages 727--751. Springer, 2016.
[ bib |
At publisher's ]
|
|
[1]
|
Pietro Abate, Roberto Di Cosmo, Louis Gesbert, Fabrice Le Fessant, Ralf
Treinen, and Stefano Zacchiroli.
Mining component repositories for installability issues.
In MSR: 12th IEEE/ACM Working Conference on Mining Software
Repositories, pages 24--33. IEEE, 2015.
[ bib |
At publisher's ]
|
|
[2]
|
Umut Acar, Arthur Charguéraud, and Mike Rainey.
A work-efficient algorithm for parallel unordered depth-first search.
In SC 2015: International Conference for High Performance
Computing, Networking, Storage and Analysis, pages 67:1--67:12. ACM,
November 2015.
[ bib |
At publisher's ]
|
|
[3]
|
Çagdas Bozman, Grégoire Henry, Mohamed Iguernelala, Fabrice
Le Fessant, and Michel Mauny.
ocp-memprof: un profileur mémoire pour OCaml.
In David Baelde and Jade Alglave, editors, JFLA 2015:
Vingt-sixièmes journées francophones des langages applicatifs, Le Val
d'Ajol, France, January 2015.
[ bib |
HAL archive ]
|
|
[4]
|
Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, and Olivier
Hermant.
Automated deduction in the B set theory using typed proof search
and deduction modulo.
In LPAR 2015: 20th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning, volume 9450 of
Lecture Notes in Computer Science. Springer, November 2015.
[ bib |
HAL archive ]
|
|
[5]
|
Arthur Charguéraud and François Pottier.
Machine-checked verification of the correctness and amortized
complexity of an efficient union-find implementation.
In ITP 2015: 6th conference on Interactive Theorem Proving,
volume 9236 of Lecture Notes in Computer Science, pages 137--153.
Springer, 2015.
[ bib |
Local copy |
At publisher's ]
|
|
[6]
|
Pierre-Évariste Dagand and Gabriel Scherer.
Normalization by realizability also evaluates.
In David Baelde and Jade Alglave, editors, JFLA 2015:
Vingt-sixièmes Journées Francophones des Langages Applicatifs, Le Val
d'Ajol, France, January 2015.
[ bib |
HAL archive ]
|
|
[7]
|
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin
Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach.
Micro-policies: Formally verified, tag-based security monitors.
In SP 2015: IEEE Symposium on Security and Privacy, pages
813--830. IEEE Computer Society, 2015.
[ bib |
At publisher's ]
|
|
[8]
|
Damien Doligez, Christèle Faure, Thérèse Hardin, and Manuel
Maarek.
Avoiding security pitfalls with functional programming: A report on
the development of a secure XML validator.
In ICSE 2015: 37th IEEE/ACM International Conference on
Software Engineering, pages 209--218. IEEE, April 2015.
[ bib |
At publisher's ]
|
|
[9]
|
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David
Pichardie.
A formally-verified C static analyzer.
In POPL'15: 42nd ACM Symposium on Principles of Programming
Languages, pages 247--259. ACM Press, January 2015.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[10]
|
Guillaume Munch-Maccagnoni and Gabriel Scherer.
Polarised intermediate representation of lambda calculus with sums.
In LICS 2015: 30th Symposium on Logic In Computer Science,
pages 127--140. IEEE Computer Society Press, 2015.
[ bib |
HAL archive |
At publisher's ]
|
|
[11]
|
Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas
Lampropoulos, and Benjamin C. Pierce.
Foundational property-based testing.
In ITP 2015: 6th conference on Interactive Theorem Proving,
volume 9236 of Lecture Notes in Computer Science, pages 325--343.
Springer, 2015.
[ bib |
HAL archive |
At publisher's ]
|
|
[12]
|
François Pottier and Jonathan Protzenko.
A few lessons from the Mezzo project.
In SNAPL 2015: 1st Summit on Advances in Programming Languages,
volume 32 of LIPIcs, pages 221--237. Schloss Dagstuhl --
Leibniz-Zentrum fuer Informatik, 2015.
[ bib |
At publisher's ]
|
|
[13]
|
François Pottier.
Depth-first search and strong connectivity in Coq.
In David Baelde and Jade Alglave, editors, JFLA 2015:
Vingt-sixièmes journées francophones des langages applicatifs, Le Val
d'Ajol, France, January 2015.
[ bib |
HAL archive ]
|
|
[14]
|
Gabriel Scherer.
Multi-focusing on extensional rewriting with sums.
In TLCA 2015: 13th International Conference on Typed Lambda
Calculi and Applications, volume 38 of LIPIcs, pages 317--331. Schloss
Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2015.
[ bib |
At publisher's ]
|
|
[15]
|
Gabriel Scherer and Didier Rémy.
Full reduction in the face of absurdity.
In ESOP 2015: Programming Languages and Systems, 24th European
Symposium on Programming, volume 9032 of Lecture Notes in Computer
Science, pages 685--709. Springer, 2015.
[ bib |
HAL archive |
At publisher's ]
|
|
[16]
|
Gabriel Scherer and Didier Rémy.
Which simple types have a unique inhabitant?
In ICFP'15: 20th International Conference on Functional
Programming, pages 243--255. ACM Press, 2015.
[ bib |
At publisher's ]
|
|
[1]
|
Umut A. Acar, Arthur Charguéraud, and Mike Rainey.
Theory and practice of chunked sequences.
In European Symposium on Algorithms, ESA 2014, volume 8737 of
Lecture Notes in Computer Science, pages 25--36. Springer, 2014.
[ bib |
HAL archive |
At publisher's ]
|
|
[2]
|
Jade Alglave, Luc Maranget, and Michael Tautschnig.
Herding cats: modelling, simulation, testing, and data-mining for
weak memory.
In PLDI 2014: ACM SIGPLAN Conference on Programming Language
Design and Implementation, page 7. ACM Press, 2014.
Presentation of TOPLAS paper.
[ bib |
HAL archive |
At publisher's ]
|
|
[3]
|
Thibaut Balabonski, Francois Pottier, and Jonathan Protzenko.
Type soundness and race freedom for Mezzo.
In FLOPS 2014: Functional and Logic Programming, volume 8475 of
Lecture Notes in Computer Science, pages 253--269. Springer, 2014.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[4]
|
Thomas Braibant, Jonathan Protzenko, and Gabriel Scherer.
Well-typed generic smart-fuzzing for APIs.
In ML'14 -- ACM SIGPLAN ML Family Workshop, 2014.
[ bib |
HAL archive |
Local copy ]
|
|
[5]
|
Sylvain Conchon, David Declerck, Luc Maranget, and Alain Mebsout.
Vérification de programmes C concurrents avec Cubicle : Enfoncer
les barrières.
In JFLA'14: Journées Francophones des Langages Applicatifs,
Fréjus, France, January 2014.
[ bib |
HAL archive ]
|
|
[6]
|
Julien Cretin and Didier Rémy.
System F with coercion constraints.
In CSL-LICS 2014: Computer Science Logic / Logic In Computer
Science, page article no 34. ACM, 2014.
[ bib |
HAL archive |
At publisher's ]
|
|
[7]
|
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, and Stephan Merz.
Coalescing: Syntactic abstraction for reasoning in first-order modal
logics.
In ARQNL 2014 - Automated Reasoning in Quantified Non-Classical
Logics, 2014.
[ bib |
HAL archive ]
|
|
[8]
|
Robbert Krebbers, Xavier Leroy, and Freek Wiedijk.
Formal C semantics: CompCert and the C standard.
In ITP 2014: Interactive Theorem Proving, number 8558 in
Lecture Notes in Computer Science, pages 543--548. Springer, 2014.
[ bib |
HAL archive |
At publisher's ]
|
|
[9]
|
Gregory Malecha, Adam Chlipala, and Thomas Braibant.
Compositional computational reflection.
In ITP 2014: Interactive Theorem Proving, number 8558 in
Lecture Notes in Computer Science, pages 374--389. Springer, 2014.
[ bib |
At publisher's ]
|
|
[10]
|
François Pottier.
Hindley-Milner elaboration in applicative style.
In ICFP 2014: Proceedings of the 19th International Conference
on Functional Programming, pages 203--212. ACM, 2014.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[11]
|
Thomas Williams, Pierre Évariste Dagand, and Didier Rémy.
Ornaments in practice.
In WGP'14 -- 10th ACM SIGPLAN Workshop on Generic Programming,
2014.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[1]
|
Thibaut Balabonski.
Weak optimality, and the meaning of sharing.
In Proceedings of the 18th International Conference on
Functional Programming (ICFP 2013), pages 263--274. ACM Press, 2013.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[2]
|
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond.
A formally-verified C compiler supporting floating-point
arithmetic.
In ARITH, 21st IEEE International Symposium on Computer
Arithmetic, pages 107--115. IEEE Computer Society Press, 2013.
[ bib |
HAL archive |
At publisher's ]
|
|
[3]
|
Thomas Braibant and Adam Chlipala.
Formal verification of hardware synthesis.
In CAV 2013, 25th International Conference on Computer Aided
Verification, volume 8044 of Lecture Notes in Computer Science, pages
213--228. Springer, 2013.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[4]
|
Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux.
Implementing hash-consed structures in Coq.
In Interactive Theorem Proving, ITP 2013, volume 7998 of
Lecture Notes in Computer Science, pages 477--483. Springer, 2013.
[ bib |
HAL archive |
At publisher's ]
|
|
[5]
|
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and
Olivier Hermant.
Proof certification in Zenon modulo: When Achilles uses deduction
modulo to outrun the tortoise with shorter steps.
In IWIL 2013, 10th International Workshop on the Implementation
of Logics. EasyChair, 2013.
[ bib |
HAL archive ]
|
|
[6]
|
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and
Olivier Hermant.
Zenon Modulo: When Achilles outruns the tortoise using
deduction modulo.
In LPAR 2013, 19th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning, volume 8312 of
Lecture Notes in Computer Science, pages 274--290. Springer, 2013.
[ bib |
HAL archive ]
|
|
[7]
|
Jacques Garrigue and Didier Rémy.
Ambivalent types for principal type inference with GADTs.
In Chung-chien Shan, editor, 11th Asian Symposium on Programming
Languages and Systems, APLAS 2013, volume 8301 of Lecture Notes in
Computer Science, pages 257--272, Melbourne, VIC, Australia, December 2013.
Springer.
[ bib |
HAL archive ]
|
|
[8]
|
François Pottier and Jonathan Protzenko.
Programming with permissions in Mezzo.
In Proceedings of the 18th International Conference on
Functional Programming (ICFP 2013), pages 173--184. ACM Press, 2013.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[9]
|
Gabriel Scherer and Jan Hoffmann.
Tracking data-flow with open closure types.
In LPAR 2013, 19th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning, volume 8312 of
Lecture Notes in Computer Science, pages 710--726. Springer, 2013.
[ bib |
HAL archive ]
|
|
[10]
|
Gabriel Scherer and Didier Rémy.
GADTs meet subtyping.
In European Symposium on Programming, ESOP 2013, volume 7792 of
Lecture Notes in Computer Science, pages 554--573. Springer, 2013.
[ bib |
HAL archive |
At publisher's ]
|
|
[1]
|
Andrew W. Appel, Robert Dockins, and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Journal of Automated Reasoning, 49(3):453--491, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[2]
|
Gregor Gössler, Dana N. Xu, and Alain Girault.
Probabilistic contracts for component-based design.
Formal Methods in System Design, 41(2):211--231, 2012.
[ bib |
HAL archive |
At publisher's ]
|
|
[3]
|
Luc Maranget, Jade Alglave, Susmit Sarkar, and Peter Sewell.
Fences in weak memory models (extended version).
Formal Methods in System Design, 40(2):170--205, 2012.
[ bib |
HAL archive |
At publisher's ]
|
|
[4]
|
Nicolas Pouillard and François Pottier.
A unified treatment of syntax with binders.
Journal of Functional Programming, 22(4--5):614--704, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[5]
|
Didier Rémy and Boris Yakobowski.
A Church-style intermediate language for MLF.
Theoretical Computer Science, 435(1):77--105, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[1]
|
Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc
Pantel, and Jean Souyris.
Formally verified optimizing compilation in ACG-based flight
control software.
In Embedded Real Time Software and Systems (ERTS2 2012). AAAF,
SEE, 2012.
[ bib |
HAL archive ]
|
|
[2]
|
Thomas Braibant and Adam Chlipala.
Formal verification of hardware synthesis.
In The Coq Workshop, 2012.
[ bib |
Local copy ]
|
|
[3]
|
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts,
and Hernán Vanzetto.
TLA + proofs.
In Dimitra Giannakopoulou and Dominique Méry, editors, FM
2012: Formal Methods - 18th International Symposium, volume 7436 of
Lecture Notes in Computer Science, pages 147--154. Springer, 2012.
[ bib |
HAL archive |
At publisher's ]
|
|
[4]
|
Julien Cretin and Didier Rémy.
On the power of coercion abstraction.
In Proceedings of the 39th ACM Symposium on Principles of
Programming Languages (POPL'12), pages 361--372. ACM Press, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[5]
|
Damien Doligez, Mathieu Jaume, and Renaud Rioboo.
Development of secured systems by mixing programs, specifications and
proofs in an object-oriented programming environment: a case study within the
FoCaLiZe environment.
In Proceedings of the 7th Workshop on Programming Languages and
Analysis for Security (PLAS'12), pages 9:1--9:12. ACM Press, 2012.
[ bib |
HAL archive |
At publisher's ]
|
|
[6]
|
Jacques-Henri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In H. Seidl, editor, Programming Languages and Systems -- 21st
European Symposium on Programming, ESOP 2012, volume 7211 of Lecture
Notes in Computer Science, pages 397--416. Springer, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[7]
|
Xavier Leroy.
Mechanized semantics for compiler verification.
In Ranjit Jhala and Atsushi Igarashi, editors, Programming
Languages and Systems, 10th Asian Symposium, APLAS 2012, volume 7705 of
Lecture Notes in Computer Science, pages 386--388. Springer, 2012.
Abstract of invited talk.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[8]
|
Jonathan Protzenko and François Pottier.
Programming with permissions: the Mezzo language.
In ACM SIGPLAN Workshop on ML, 2012.
[ bib |
HAL archive |
Local copy ]
|
|
[9]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
A mechanized semantics for C++ object construction and destruction,
with applications to resource management.
In Proceedings of the 39th ACM Symposium on Principles of
Programming Languages (POPL'12), pages 521--532. ACM Press, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[10]
|
Valentin Robert and Xavier Leroy.
A formally-verified alias analysis.
In Chris Hawblitzel and Dale Miller, editors, Certified Programs
and Proofs -- Second International Conference, CPP 2012, volume 7679 of
Lecture Notes in Computer Science, pages 11--26. Springer, 2012.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[11]
|
Gabriel Scherer and Didier Rémy.
GADTs meet subtyping.
In ACM SIGPLAN Workshop on ML, 2012.
[ bib |
HAL archive |
Local copy ]
|
|
[12]
|
Dana N. Xu.
Hybrid contract checking via symbolic simplification.
In Proceedings of the ACM SIGPLAN Workshop on Partial
Evaluation and Program Manipulation (PEPM'12), pages 107--116. ACM Press,
2012.
[ bib |
Local copy |
At publisher's ]
|
|
[13]
|
Brent Yorgey, Stephanie Weirich, Julien Cretin, José Pedro Magalhães, Simon
Peyton Jones, and Dimitrios Vytiniotis.
Giving Haskell a promotion.
In The Seventh ACM SIGPLAN Workshop on Types in Language Design
and Implementation (TLDI'12), pages 67--78. ACM Press, 2012.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Pietro Abate and Roberto Di Cosmo.
Predicting upgrade failures using dependency analysis.
In Workshops Proceedings of the 27th International Conference on
Data Engineering, ICDE 2011, pages 145--150. IEEE Computer Society Press,
2011.
[ bib |
Local copy ]
|
|
[2]
|
Pietro Abate, Roberto Di Cosmo, Ralf Treinen, and Stefano Zacchiroli.
MPM: a modular package manager.
In Proceedings of the 14th International ACM Sigsoft Symposium
on Component Based Software Engineering, CBSE 2011, pages 179--188. ACM
Press, 2011.
[ bib |
At publisher's ]
|
|
[3]
|
Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean
Souyris.
Towards formally verified optimizing compilation in flight control
software.
In Bringing Theory to Practice: Predictability and Performance
in Embedded Systems (PPES 2011), volume 18 of OpenAccess Series in
Informatics (OASIcs), pages 59--68. Schloss Dagstuhl--Leibniz-Zentrum fuer
Informatik, 2011.
[ bib |
HAL archive |
At publisher's ]
|
|
[4]
|
Pascal Cuoq, Damien Doligez, and Julien Signoles.
Lightweight typed customizable unmarshaling.
In ACM SIGPLAN Workshop on ML. ACM Press, 2011.
[ bib ]
|
|
[5]
|
Roberto Di Cosmo, Olivier Lhomme, and Claude Michel.
Aligning component upgrades.
In Proceedings Second Workshop on Logics for Component
Configuration, volume 65 of Electronic Proceedings in Theoretical
Computer Science, pages 1--11, 2011.
[ bib |
At publisher's ]
|
|
[6]
|
Roberto Di Cosmo and Jérôme Vouillon.
On software component co-installability.
In 19th ACM SIGSOFT Symposium on the Foundations of Software
Engineering (FSE-19) and ESEC'11: 13rd European Software Engineering
Conference (ESEC-13), pages 256--266. ACM Press, 2011.
[ bib |
At publisher's ]
|
|
[7]
|
Xavier Leroy.
Formally verifying a compiler: Why? how? how far?
In Proceedings of CGO 2011, The 9th International Symposium on
Code Generation and Optimization. IEEE, 2011.
Abstract of invited talk.
[ bib |
HAL archive |
At publisher's ]
|
|
[8]
|
Xavier Leroy.
Verified squared: does critical software deserve verified tools?
In Proceedings of the 38th ACM Symposium on Principles of
Programming Languages (POPL'11), pages 1--2. ACM Press, 2011.
Abstract of invited talk.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[9]
|
Alexandre Pilkiewicz and François Pottier.
The essence of monotonic state.
In 6th Workshop on Types in Language Design and Implementation
(TLDI 2011), pages 73--86. ACM Press, 2011.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[10]
|
François Pottier.
A typed store-passing translation for general references.
In Proceedings of the 38th ACM Symposium on Principles of
Programming Languages (POPL'11), pages 147--158. ACM Press, 2011.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[11]
|
Nicolas Pouillard.
Nameless, painless.
In Proceedings of the 16th International Conference on
Functional Programming (ICFP 2011), pages 320--332. ACM Press, 2011.
[ bib |
Local copy |
At publisher's ]
|
|
[12]
|
Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
Formal verification of object layout for C++ multiple inheritance.
In Proceedings of the 38th ACM Symposium on Principles of
Programming Languages (POPL'11), pages 67--80. ACM Press, 2011.
[ bib |
HAL archive |
Local copy |
At publisher's ]
|
|
[1]
|
Julien Cretin and Didier Rémy.
On the Power of Coercion Abstraction.
Research Report RR-7587, INRIA, December 2011.
[ bib |
Local copy |
Pdf ]
|
|
[2]
|
Sylvain Dailler.
Preuve mécanisée de correction et de complexité pour un algorithme
impératif.
Master's thesis, University Paris Diderot, August 2011.
Report on Master's internship.
[ bib ]
|
|
[3]
|
Jacques-Henri Jourdan.
Validation d'analyseurs syntaxiques LR(1): Vers un analyseur
syntaxique certifié pour le compilateur CompCert.
Master's thesis, ENS Paris, August 2011.
Report on Master's internship.
[ bib ]
|
|
[4]
|
Xavier Leroy.
Safety first! (technical perspective).
Communications of the ACM, 54(12):122--122, December 2011.
[ bib |
HAL archive |
At publisher's ]
|
|
[5]
|
Valentin Robert.
Conception, mise en oeuvre et vérification d'une analyse d'alias
pour CompCert, un compilateur C formellement vérifié.
Master's thesis, ENSEIRB, December 2011.
Report on Master's internship.
[ bib ]
|
|
[6]
|
Dana N. Xu.
Hybrid contract checking via symbolic simplification.
Research Report RR-7794, INRIA, November 2011.
[ bib |
Local copy ]
|
|
[1]
|
Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and
Benjamin C. Pierce.
Matching lenses: Alignment and view update.
In Proceedings of the 15th International Conference on
Functional Programming (ICFP 2010), pages 193--204. ACM Press, 2010.
[ bib |
At publisher's ]
|
|
[2]
|
Arthur Charguéraud.
Program verification through characteristic formulae.
In Proceedings of the 15th International Conference on
Functional Programming (ICFP 2010), pages 321--332. ACM Press, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[3]
|
Arthur Charguéraud.
The optimal fixed point combinator.
In Interactive Theorem Proving (ITP 2010), volume 6172 of
Lecture Notes in Computer Science, pages 195--210. Springer, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[4]
|
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz.
Verifying safety properties with the TLA+ proof system.
In Automated Reasoning, 5th International Joint Conference,
IJCAR 2010, volume 6173 of Lecture Notes in Computer Science, pages
142--148. Springer, 2010.
[ bib |
At publisher's ]
|
|
[5]
|
Roberto Di Cosmo and Jaap Boender.
Using strong conflicts to detect quality issues in component-based
complex systems.
In ISEC '10: Proceedings of the 3rd India software engineering
conference, pages 163--172. ACM Press, 2010.
[ bib |
At publisher's ]
|
|
[6]
|
Roberto Di Cosmo and Stefano Zacchiroli.
Feature diagrams as package dependencies.
In Software Product Lines: Going Beyond - 14th International
Conference, SPLC 2010, volume 6287 of Lecture Notes in Computer
Science, pages 476--480. Springer, 2010.
[ bib |
At publisher's ]
|
|
[7]
|
Benoît Montagu.
Experience report: Mechanizing Core F-zip using the locally
nameless approach (extended abstract).
In 5th ACM SIGPLAN Workshop on Mechanizing Metatheory, 2010.
[ bib |
At publisher's ]
|
|
[8]
|
Benoît Montagu and Didier Rémy.
Types abstraits et types existentiels ouverts.
In Éric Cariou, Laurence Duchien, and Yves Ledru, editors,
Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du
Génie de la Programmation et du Logiciel, pages 147--148, Université de
Pau, March 2010.
[ bib |
At publisher's ]
|
|
[9]
|
Nicolas Pouillard and François Pottier.
A fresh look at programming with names and binders.
In Proceedings of the 15th International Conference on
Functional Programming (ICFP 2010), pages 217--228. ACM Press, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[10]
|
Didier Rémy and Boris Yakobowski.
A Church-style intermediate language for MLF.
In Functional and Logic Programming, 10th International
Symposium, FLOPS 2010, volume 6009 of Lecture Notes in Computer
Science, pages 24--39. Springer, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[11]
|
Silvain Rideau and Xavier Leroy.
Validating register allocation and spilling.
In Compiler Construction (CC 2010), volume 6011 of Lecture
Notes in Computer Science, pages 224--243. Springer, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[12]
|
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, and
Bernhard Reus.
A semantic foundation for hidden state.
In Foundations of Software Science and Computation Structures
(FoSSaCS 2010), volume 6014 of Lecture Notes in Computer Science,
pages 2--17. Springer, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[13]
|
Jean-Baptiste Tristan and Xavier Leroy.
A simple, verified validator for software pipelining.
In Proceedings of the 37th ACM Symposium on Principles of
Programming Languages (POPL'10), pages 83--92. ACM Press, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[14]
|
Dana N. Xu, Gregor Gössler, and Alain Girault.
Probabilistic contracts for component-based design.
In Automated Technology for Verification and Analysis (ATVA
2010), volume 6252 of Lecture Notes in Computer Science, pages
325--340. Springer, 2010.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Sandrine Blazy and Xavier Leroy.
Mechanized semantics for the Clight subset of the C language.
Journal of Automated Reasoning, 43(3):263--288, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[2]
|
Zaynah Dargaye and Xavier Leroy.
A verified framework for higher-order uncurrying optimizations.
Higher-Order and Symbolic Computation, 22(3):199--231, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[3]
|
Tom Hirschowitz, Xavier Leroy, and J. B. Wells.
Compilation of extended recursion in call-by-value functional
languages.
Higher-Order and Symbolic Computation, 22(1):3--66, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[4]
|
Didier Le Botlan and Didier Rémy.
Recasting MLF.
Information and Computation, 207(6):726--785, 2009.
[ bib |
DOI |
Local copy |
At publisher's ]
|
|
[5]
|
Xavier Leroy.
Formal verification of a realistic compiler.
Communications of the ACM, 52(7):107--115, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[6]
|
Xavier Leroy.
A formally verified compiler back-end.
Journal of Automated Reasoning, 43(4):363--446, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[7]
|
Xavier Leroy and Hervé Grall.
Coinductive big-step operational semantics.
Information and Computation, 207(2):284--304, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Pietro Abate, Jaap Boender, Roberto Di Cosmo, and Stefano Zacchiroli.
Strong dependencies between software components.
In 3rd International Symposium on Empirical Sofware Engineering
and Measurement, ESEM 2009, pages 89--99. IEEE Computer Society Press,
October 2009.
[ bib |
At publisher's ]
|
|
[2]
|
Sandrine Blazy and Benoît Robillard.
Live-range unsplitting for faster optimal coalescing.
In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on
Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), pages
70--79. ACM Press, 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[3]
|
Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, and
Gilles Muller.
A foundation for flow-based program matching using temporal logic and
model checking.
In Proceedings of the 36th ACM Symposium on Principles of
Programming Languages (POPL'09), pages 114--126. ACM Press, January 2009.
[ bib |
At publisher's ]
|
|
[4]
|
Benoît Montagu and Didier Rémy.
Modeling abstract types in modules with open existential types.
In Proceedings of the 36th ACM Symposium on Principles of
Programming Languages (POPL'09), pages 354--365. ACM Press, January 2009.
[ bib |
Local copy |
At publisher's ]
|
|
[5]
|
Jean-Baptiste Tristan and Xavier Leroy.
Verified validation of Lazy Code Motion.
In Proceedings of the 2009 ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI'09), pages 316--326. ACM Press,
2009.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and
Stephanie Weirich.
Engineering formal metatheory.
In Proceedings of the 35th ACM Symposium on Principles of
Programming Languages (POPL'08), pages 3--15. ACM Press, January 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[2]
|
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, and Pierre Weis.
Trusted software within Focal.
In Pascal Chour, Yves Correc, Olivier Heen, and Ludovic Mé,
editors, Computer & Electronics Security Applications Rendez-vous
(C&SAR 2008), pages 142--158, December 2008.
[ bib |
Local copy ]
|
|
[3]
|
Sandrine Blazy, Benoît Robillard, and Éric Soutif.
Coloration avec préférences: complexité, inégalités valides et
vérification formelle.
In ROADEF'08, 9e congrès de la Société Française de
Recherche Opérationnelle et d'Aide à la Décision, February 2008.
[ bib |
Local copy ]
|
|
[4]
|
Sandrine Blazy, Benoît Robillard, and Éric Soutif.
Vérification formelle d'un algorithme d'allocation de registres par
coloration de graphes.
In Journées Francophones des Langages Applicatifs (JFLA'08),
pages 31--46, Étretat, France, January 2008. INRIA.
[ bib |
Local copy |
At publisher's ]
|
|
[5]
|
Arthur Charguéraud and François Pottier.
Functional translation of a calculus of capabilities.
In Proceedings of the 13th International Conference on
Functional Programming (ICFP'08), pages 213--224. ACM Press, September 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[6]
|
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz.
A TLA+ proof system.
In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz,
editors, Proceedings of the LPAR Workshops: Knowledge Exchange:
Automated Provers and Proof Assistants, and The 7th International Workshop on
the Implementation of Logics, volume 418 of CEUR Workshop
Proceedings. CEUR-WS.org, November 2008.
[ bib |
Local copy ]
|
|
[7]
|
Pascal Cuoq and Damien Doligez.
Hashconsing in an incrementally garbage-collected system: A story of
weak pointers and hashconsing in OCaml 3.10.2.
In 2008 ACM SIGPLAN Workshop on ML, pages 13--22. ACM
Press, September 2008.
[ bib |
At publisher's ]
|
|
[8]
|
J. Nathan Foster, Alexandre Pilkiewicz, and Benjamin C. Pierce.
Quotient lenses.
In Proceedings of the 13th International Conference on
Functional Programming (ICFP'08), pages 383--396. ACM Press, September 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[9]
|
François Pottier.
Hiding local state in direct style: a higher-order anti-frame rule.
In Proceedings of the 23rd Annual IEEE Symposium on Logic In
Computer Science (LICS'08), pages 331--340. IEEE Computer Society Press,
June 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[10]
|
Yann Régis-Gianas and François Pottier.
A Hoare logic for call-by-value functional programs.
In Mathematics of Program Construction, 9th International
Conference, MPC 2008, volume 5133 of Lecture Notes in Computer
Science, pages 305--335. Springer, July 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[11]
|
Jean-Baptiste Tristan and Xavier Leroy.
Formal verification of translation validators: A case study on
instruction scheduling optimizations.
In Proceedings of the 35th ACM Symposium on Principles of
Programming Languages (POPL'08), pages 17--27. ACM Press, January 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[12]
|
Boris Yakobowski.
Le caractère “backquote” à la rescousse -- Factorisation et
réutilisation de code grâce aux variants polymorphes.
In Journées Francophones des Langages Applicatifs (JFLA'08),
pages 63--78, Étretat, France, January 2008. INRIA.
[ bib |
Local copy |
At publisher's ]
|
|
[13]
|
Boris Yakobowski and Didier Rémy.
Graphic type constraints and efficient type inference: from ML to
MLF.
In Proceedings of the 13th International Conference on
Functional Programming (ICFP'08), pages 63--74. ACM Press, September 2008.
[ bib |
Local copy |
At publisher's ]
|
|
[1]
|
Andrew W. Appel and Sandrine Blazy.
Separation logic for small-step Cminor.
In Theorem Proving in Higher Order Logics, 20th Int. Conf.
TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages
5--21. Springer, 2007.
[ bib |
Local copy ]
|
|
[2]
|
Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory (extended
abstract).
In Proc. Int. Workshop on Logical Frameworks and Meta-Languages
(LFMTP'06), volume 174(5) of Electronic Notes in Computer Science,
pages 95--108, 2007.
[ bib |
Local copy |
At publisher's ]
|
|
[3]
|
Sandrine Blazy.
Experiments in validating formal semantics for C.
In Proceedings of the C/C++ Verification Workshop, pages
95--102. Technical report ICIS-R07015, Radboud University Nijmegen, 2007.
[ bib |
Local copy ]
|
|
[4]
|
Sandrine Blazy, Benoît Robillard, and Éric Soutif.
Coloration avec préférences dans les graphes triangulés.
In Journées Graphes et Algorithmes (JGA'07), nov 2007.
[ bib |
Local copy ]
|
|
[5]
|
Richard Bonichon, David Delahaye, and Damien Doligez.
Zenon: an extensible automated theorem prover producing checkable
proofs.
In Logic for Programming, Artificial Intelligence and Reasoning,
14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial
Intelligence, pages 151--165. Springer, 2007.
[ bib |
Local copy ]
|
|
[6]
|
Zaynah Dargaye.
Décurryfication certifiée.
In Journées Francophones des Langages Applicatifs (JFLA'07),
pages 119--134. INRIA, 2007.
[ bib |
Local copy ]
|
|
[7]
|
Zaynah Dargaye and Xavier Leroy.
Mechanized verification of CPS transformations.
In Logic for Programming, Artificial Intelligence and Reasoning,
14th Int. Conf. LPAR 2007, volume 4790 of Lecture Notes in Artificial
Intelligence, pages 211--225. Springer, 2007.
[ bib |
Local copy ]
|
|
[8]
|
Alain Frisch and Haruo Hosoya.
Towards practical typechecking for macro tree transducers.
In Database Programming Languages, 11th International Symposium,
DBPL 2007, volume 4797 of Lecture Notes in Computer Science, pages
246--260. Springer, 2007.
[ bib |
Local copy ]
|
|
[9]
|
Alain Frisch and Keisuke Nakano.
Streaming XML transformations using term rewriting.
In Workshop Programming Language Technologies for XML (PLAN-X
2007), pages 2--13, January 2007.
[ bib |
Local copy ]
|
|
[10]
|
Peng Li, Simon Marlow, Simon Peyton Jones, and Andrew Tolmach.
Lightweight concurrency primitives for GHC.
In Haskell '07: Proceedings of the ACM SIGPLAN workshop on
Haskell, pages 107--118. ACM Press, 2007.
[ bib |
Local copy ]
|
|
[11]
|
François Pottier.
Static name control for FreshML.
In Twenty-Second Annual IEEE Symposium on Logic In Computer
Science (LICS'07), pages 356--365. IEEE Computer Society Press, July 2007.
[ bib |
Local copy |
At publisher's ]
|
|
[12]
|
Didier Rémy and Boris Yakobowski.
A graphical presentation of MLF types with a linear-time
incremental unification algorithm.
In ACM SIGPLAN Workshop on Types in Language Design
and Implementation, pages 27--38. ACM Press, January 2007.
[ bib |
Local copy ]
|
|
[1]
|
Andrew W. Appel and Sandrine Blazy.
Separation logic for small-step Cminor (extended version).
Research report 6138, INRIA, 2007.
[ bib |
Local copy ]
|
|
[2]
|
Arthur Charguéraud.
Proof of imperative programs.
Master's dissertation (mémoire de stage de Master 2), ENS
Lyon, September 2007.
[ bib ]
|
|
[3]
|
Didier Le Botlan and Didier Rémy.
Recasting MLF.
Research report 6228, INRIA, June 2007.
[ bib |
Local copy ]
|
|
[4]
|
Xavier Leroy.
A locally nameless solution to the POPLmark challenge.
Research report 6098, INRIA, January 2007.
[ bib |
Local copy ]
|
|
[5]
|
Benoît Montagu.
Modules de première classe.
Master's dissertation (mémoire de stage de Master 2), École
Polytechnique, September 2007.
[ bib |
Local copy ]
|
|
[6]
|
Tahina Ramananandro.
Vérification formelle d'une implémentation d'un gestionnaire
de mémoire pour un compilateur certifié.
Master's dissertation (mémoire de stage de Master 2), ENS
Paris, September 2007.
[ bib |
Local copy ]
|
|
[1]
|
Yves Bertot, Benjamin Grégoire, and Xavier Leroy.
A structured approach to proving compiler optimizations based on
dataflow analysis.
In Types for Proofs and Programs, Workshop TYPES 2004, volume
3839 of Lecture Notes in Computer Science, pages 66--81. Springer,
2006.
[ bib |
Local copy ]
|
|
[2]
|
Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy.
Formal verification of a C compiler front-end.
In FM 2006: Int. Symp. on Formal Methods, volume 4085 of
Lecture Notes in Computer Science, pages 460--475. Springer, 2006.
[ bib |
Local copy |
At publisher's ]
|
|
[3]
|
Jaap Boender, Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli,
Mario Morgado, David Pinheiro, Ralf Treinen, Paulo Trezentos, and Jérôme
Vouillon.
News from the EDOS project: improving the maintenance of free
software distributions.
In Proceedings of the VIIth International Workshop on Free
Software (IWFS'06), pages 199--207, 2006.
[ bib |
Local copy ]
|
|
[4]
|
Roberto Di Cosmo, Berke Durak, Xavier Leroy, Fabio Mancinelli, and Jérôme
Vouillon.
Maintaining large software distributions: new challenges from the
FOSS era.
In Proceedings of the FRCSS 2006 workshop, volume 12 of
EASST Newsletter, pages 7--20, 2006.
[ bib |
Local copy ]
|
|
[5]
|
Alain Frisch.
OCaml + XDuce.
In Workshop Programming Language Technologies for XML (PLAN-X)
2006, pages 36--48. BRICS Notes series NS-05-6, University of Aarhus,
January 2006.
[ bib ]
|
|
[6]
|
Alain Frisch.
OCaml + XDuce.
In Proceedings of the Eleventh ACM SIGPLAN International
Conference on Functional Programming, pages 192--200. ACM Press, September
2006.
[ bib |
Local copy ]
|
|
[7]
|
Grégoire Henry, Michel Mauny, and Emmanuel Chailloux.
Typer la dé-sérialisation sans sérialiser les types.
In Journées francophones des langages applicatifs, pages
133--146. INRIA, January 2006.
[ bib |
Local copy ]
|
|
[8]
|
Xavier Leroy.
Coinductive big-step operational semantics.
In European Symposium on Programming (ESOP'06), volume 3924 of
Lecture Notes in Computer Science, pages 54--68. Springer, 2006.
[ bib |
Local copy |
At publisher's ]
|
|
[9]
|
Xavier Leroy.
Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant.
In 33rd ACM symposium on Principles of Programming Languages,
pages 42--54. ACM Press, 2006.
[ bib |
Local copy |
At publisher's ]
|
|
[10]
|
Fabio Mancinelli, Roberto Di Cosmo, Jérôme Vouillon, Jaap Boender, Berke
Durak, Xavier Leroy, and Ralf Treinen.
Managing the complexity of large free and open source package-based
software distributions.
In 21st IEEE Int. Conf. on Automated Software Engineering (ASE
2006), pages 199--208. IEEE Computer Society Press, 2006.
[ bib |
Local copy ]
|
|
[11]
|
François Pottier and Yann Régis-Gianas.
Stratified type inference for generalized algebraic data types.
In 33rd ACM symposium on Principles of Programming Languages,
pages 232--244. ACM Press, January 2006.
[ bib |
Local copy ]
|