Publications de l'équipe GALLIUM

2012

Articles dans des revues avec comité de lecture

Titre

Probabilistic contracts for component-based design

Auteurs

Gregor Goessler; Dana Xu; Alain Girault

Détail

Formal Methods in System Design, Springer, 2012, 41 (2), pp. 211-231

Accès au bibtex

Communications avec actes

Titre

On the Power of Coercion Abstraction

Auteurs

Julien Cretin; Didier Rémy

Détail

POPL 2012: 39th ACM SIGPLAN-SIGACT Symposium on Principle Of Programming Languages, Jan 2012, Philadelphia, United States. ACM, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Accès au bibtex

Titre

A mechanized semantics for C++ object construction and destruction, with applications to resource management

Auteurs

Tahina Ramananandro ; Gabriel Dos Reis ; Xavier Leroy

Détail

POPL '12 - 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2012, Philadelphia, PA, United States. pp. 521-532

Accès au texte intégral et bibtex

Titre

TLA+ Proofs

Auteurs

Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz ; Daniel Ricketts; Hernán Vanzetto

Détail

Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, 7436, pp. 147-154, Lecture Notes in Computer Science

Accès au bibtex

Communications sans actes

Titre

Formally verified optimizing compilation in ACG-based flight control software

Auteurs

Ricardo Bedin França; Sandrine Blazy ; Denis Favre-Felix; Xavier Leroy ; Marc Pantel ; Jean Souyris

Détail

ERTS2 2012: Embedded Real Time Software and Systems, Feb 2012, Toulouse, France.

Accès au texte intégral et bibtex

Titre

TLA+ Proofs

Auteurs

Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz ; Daniel Ricketts; Hernán Vanzetto

Détail

AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p.

Accès au bibtex

Rapports

Titre

GADT meet Subtyping

Auteurs

Gabriel Scherer ; Didier Rémy

Détail

[Research Report], 2012, pp. 33. RR-8114

Accès au texte intégral et bibtex

Titre

Probabilistic Contracts for Component-based Design

Auteurs

Gregor Gössler; Dana Xu; Alain Girault

Détail

[Research Report], 2012. RR-7328

Accès au texte intégral et bibtex

Titre

The CompCert Memory Model, Version 2

Auteurs

Xavier Leroy ; Andrew Appel ; Sandrine Blazy ; Gordon Stewart

Détail

[Research Report], 2012, pp. 26. RR-7987

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic

Auteurs

Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond

Détail

Oct. 2012

Accès au texte intégral et bibtex

2011

Articles dans des revues avec comité de lecture

Titre

A list-machine benchmark for mechanized metatheory

Auteurs

Andrew Appel ; Robert Dockins ; Xavier Leroy

Détail

Journal of Automated Reasoning, Springer, 2011

Accès au texte intégral et bibtex

Communications avec actes

Titre

Towards Formally Verified Optimizing Compilation in Flight Control Software

Auteurs

Ricardo Bedin França; Denis Favre-Felix; Xavier Leroy; Marc Pantel; Jean Souyris

Détail

Philipp Lucas and Lothar Thiele and Benoit Triquet and Theo Ungerer and Reinhard Wilhelm. Predictability and Performance in Embedded Systems : PPES 2011, Mar 2011, Grenoble, France. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Bringing Theory to Practice: Predictability and Performance in Embedded Systems, 18, pp. 59-68, OpenAccess Series in Informatics (OASIcs)

Accès au texte intégral et bibtex

Titre

Formal verification of object layout for C++ multiple inheritance

Auteurs

Tahina Ramananandro ; Gabriel Dos Reis ; Xavier Leroy

Détail

POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2011, Austin, TX, United States. ACM Press, pp. 67-79

Accès au texte intégral et bibtex

Rapports

Titre

On the Power of Coercion Abstraction

Auteurs

Julien Cretin; Didier Rémy

Détail

[Research Report], 2011, pp. 59. RR-7587

Accès au texte intégral et bibtex

Titre

Hybrid Contract Checking via Symbolic Simplification

Auteurs

Na Xu

Détail

[Research Report], 2011. RR-7794

Accès au texte intégral et bibtex

2010

Articles de vulgarisation scientifique

Titre

Comment faire confiance à un compilateur ?

Auteurs

Xavier Leroy

Détail

La Recherche Les Cahiers de l'Inria, Societé d' éditions scientifiques, 2010, Cancer la révolution, 440 avril 2010

Accès au texte intégral et bibtex

Communications avec actes

Titre

Validating register allocation and spilling

Auteurs

Silvain Rideau; Xavier Leroy

Détail

Compiler Construction 2010, Mar 2010, Paphos, Cyprus. Springer, Compiler Construction 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, 6011, pp. 224-243, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A simple, verified validator for software pipelining

Auteurs

Jean-Baptiste Tristan; Xavier Leroy

Détail

ACM. 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Jan 2010, Madrid, Spain.

Accès au texte intégral et bibtex

Titre

The TLA+ Proof System: Building a Heterogeneous Verification Platform

Auteurs

Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz

Détail

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, Theoretical Aspects of Computing - ICTAC 2010, 6255, pp. 44, Lecture Notes in Computer Science

Accès au bibtex

Titre

Probabilistic Contracts for Component-Based Design

Auteurs

Dana N. Xu; Gregor Goessler; Alain Girault

Détail

the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sep 2010, Singapore, Singapore. Springer, pp. 325-340

Accès au bibtex

Titre

Verifying Safety Properties With the TLA+ Proof System

Auteurs

Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz

Détail

Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, Automated Reasoning 5th International Joint Conference, IJCAR 2010 Edinburgh, UK, July 16-19, 2010 Proceedings, 6173, pp. 142-148, Lecture Notes in Artificial Intelligence

Accès au texte intégral et bibtex

Chapitres d'ouvrages scientifiques

Titre

Mechanized semantics

Auteurs

Xavier Leroy

Détail

J. Esparza and B. Spanfelner and O. Grumberg. Logics and languages for reliability and security, 25, IOS Press, pp. 195-224, Mar. 2010, NATO Science for Peace and Security Series D: Information and Communication Security

Accès au texte intégral et bibtex

Rapports

Titre

Probabilistic Contracts for Component-based Design

Auteurs

Dana Xu; Gregor Goessler; Alain Girault

Détail

[Research Report], 2010. RR-7328

Accès au texte intégral et bibtex

Thèses

Titre

Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts

Auteurs

Benoît Montagu

Détail

Ecole Polytechnique X, Dec. 2010. English

Accès au texte intégral et bibtex

2009

Articles dans des revues avec comité de lecture

Titre

A formally verified compiler back-end

Auteurs

Xavier Leroy

Détail

Journal of Automated Reasoning, Springer, 2009, 43 (4), pp. 363-446

Accès au texte intégral et bibtex

Titre

Compilation of extended recursion in call-by-value functional languages

Auteurs

Tom Hirschowitz; Xavier Leroy; J. B. Wells

Détail

Higher-Order and Symbolic Computation, 2009, 22 (1), pp. 3-66

Accès au texte intégral et bibtex

Titre

Recasting MLF

Auteurs

Didier Le Botlan; Didier Rémy

Détail

Information and Computation, ScienceDirect, 2009, Volume 207, Issue 6, June 2009, Pages 726-785, 207 (6), pp. 726-785

Accès au texte intégral et bibtex

Titre

Coinductive big-step operational semantics

Auteurs

Xavier Leroy; Hervé Grall

Détail

Information and Computation, Elsevier, 2009, 207 (2), pp. 284-304

Accès au texte intégral et bibtex

Titre

Mechanized semantics for the Clight subset of the C language

Auteurs

Sandrine Blazy; Xavier Leroy

Détail

Journal of Automated Reasoning, Springer, 2009, 43 (3), pp. 263-288

Accès au texte intégral et bibtex

Communications avec actes

Titre

Verified Validation of Lazy Code Motion

Auteurs

Jean-Baptiste Tristan; Xavier Leroy

Détail

ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), Jun 2009, Dublin, Ireland. ACM, pp. 316-326

Accès au texte intégral et bibtex

Titre

Register allocation by graph coloring under full live-range splitting

Auteurs

Sandrine Blazy; Benoît Robillard

Détail

ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded systems (LCTES'2009), Jun 2009, Dublin, Ireland.

Accès au texte intégral et bibtex

Thèses

Titre

Machines d'Eilenberg Effectives

Auteurs

Benoit Razet

Détail

Université Paris-Diderot - Paris VII, Nov. 2009. French

Accès au texte intégral et bibtex

Titre

Formal verification of translation validators

Auteurs

Jean-Baptiste Tristan

Détail

Université Paris-Diderot - Paris VII, Nov. 2009. French

Accès au texte intégral et bibtex

Titre

Vérification formelle d'un compilateur optimisant pour langages fonctionnels

Auteurs

Zaynah Dargaye

Détail

Université Paris-Diderot - Paris VII, Jul. 2009. French

Accès au texte intégral et bibtex

2008

Articles dans des revues avec comité de lecture

Titre

Formal verification of a C-like memory model and its uses for verifying program transformations

Auteurs

Xavier Leroy; Sandrine Blazy

Détail

Journal of Automated Reasoning, Springer, 2008, 41 (1), pp. 1-31

Accès au texte intégral et bibtex

Titre

Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves

Auteurs

Laurence Rideau; Bernard Serpette; Xavier Leroy

Détail

Journal of Automated Reasoning, Springer, 2008, 40 (4), pp. 307-326

Accès au texte intégral et bibtex

Communications avec actes

Titre

Le caractère ` à la rescousse -- Factorisation et réutilisation de code grâce aux variants polymorphes

Auteurs

Boris Yakobowski

Détail

JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp. 63-78

Accès au texte intégral et bibtex

Titre

Coloration avec préférences : complexité, inégalités valides et vérification formelle

Auteurs

Benoît Robillard; Sandrine Blazy; Eric Soutif

Détail

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

Accès au texte intégral et bibtex

Titre

Formal verification of translation validators: A case study on instruction scheduling optimizations

Auteurs

Jean-Baptiste Tristan; Xavier Leroy

Détail

35th ACM Symposium on Principles of Programming Languages (POPL 2008), Jan 2008, San Francisco, United States. ACM Press, pp. 17-27

Accès au texte intégral et bibtex

Titre

A Hoare Logic for Call-by-Value Functional Programs

Auteurs

Yann Regis-Gianas; François Pottier

Détail

MPC 08 - Proceedings of the Ninth International Conference on Mathematics of Program Construction, Jul 2008, Marseille, France. Springer, 5133, pp. 305-335, Lecture notes in computer scinece

Accès au bibtex

Communications sans actes

Titre

A TLA+ Proof System

Auteurs

Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz

Détail

Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar.

Accès au texte intégral et bibtex

Directions d'ouvrages

Titre

Actes de la conférence JFLA2008 (Journées Francophones des Langages Applicatifs)

Auteurs

Sandrine Blazy

Détail

INRIA. INRIA, pp. 173, 2008, 2-7261-1295-1

Accès au texte intégral et bibtex

Thèses

Titre

Types et contraintes graphiques - polymorphisme de second ordre et inférence

Auteurs

Boris Yakobowski

Détail

informatique. Université Paris-Diderot - Paris VII, Dec. 2008. English

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking

Auteurs

Julien Brunel; Damien Doligez; René Hansen; Julia Lawall; Gilles Muller

Détail

Jul. 2008, EMN 08/2/INFO. pp16

Accès au texte intégral et bibtex

2007

Articles dans des revues sans comité de lecture

Titre

Comment gagner confiance en C ?

Auteurs

Sandrine Blazy

Détail

Revue Technique et Science Informatiques (TSI), Lavoisier, 2007, numéro spécial "Langages applicatifs", 26 (9), pp. 1195-1200

Accès au texte intégral et bibtex

Communications avec actes

Titre

Separation Logic for Small-step Cminor

Auteurs

Andrew W. Appel; Sandrine Blazy

Détail

Springer-Verlag. 20th Int. Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Sep 2007, Kaiserslautern, Germany. 4732, pp. 5-21, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Mechanized verification of CPS transformations

Auteurs

Zaynah Dargaye; Xavier Leroy

Détail

Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, Oct 2007, Erevan, Armenia. Springer, Logic for Programming, Artificial Intelligence and Reasoning, 14th Int. Conf. LPAR 2007, 4790, pp. 211-225, Lecture Notes in Artificial Intelligence

Accès au texte intégral et bibtex

Titre

Experiments in validating formal semantics for C

Auteurs

Sandrine Blazy

Détail

C/C++ Verification Workshop, 2007, Oxford, United Kingdom. pp. 95-102

Accès au texte intégral et bibtex

Titre

Coloration avec préférences dans les graphes triangulés

Auteurs

Sandrine Blazy; Benoît Robillard; Eric Soutif

Détail

Journées Graphes et algorithmes (JGA'07), Nov 2007, Paris, France. pp. 32

Accès au bibtex

Titre

Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs

Auteurs

Richard Bonichon; David Delahaye; Damien Doligez

Détail

Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. Springer, Logic for Programming, Artificial Intelligence, and Reasoning, 4790, pp. 151-165, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

Décurryfication certifiée

Auteurs

Zaynah Dargaye

Détail

Pierre-Etienne Moreau et Sandrine Blazy. Journées Francophones des Langages Applicatifs (JFLA 2007), Jan 2007, Aix-les-Bains, France. INRIA, pp. 119-134

Accès au texte intégral et bibtex

Rapports

Titre

A locally nameless solution to the POPLmark challenge

Auteurs

Xavier Leroy

Détail

[Research Report], 2007, pp. 54. RR-6098

Accès au texte intégral et bibtex

Titre

Towards Practical Typechecking for Macro Tree Transducers

Auteurs

Alain Frisch; Haruo Hosoya

Détail

[Research Report], 2007, pp. 28. RR-6107

Accès au texte intégral et bibtex

Documents sans référence de publication

Titre

Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves

Auteurs

Laurence Rideau; Bernard Serpette; Xavier Leroy

Détail

Oct. 2007

Accès au texte intégral et bibtex

2006

Communications avec actes

Titre

Formal certification of a compiler back-end, or: programming a compiler with a proof assistant

Auteurs

Xavier Leroy

Détail

33rd Symposium Principles of Programming Languages (POPL 2006), Jan 2006, Charleston, SC, United States. ACM Press, pp. 42-54

Accès au texte intégral et bibtex

Titre

A list-machine benchmark for mechanized metatheory (extended abstract)

Auteurs

Andrew W. Appel; Xavier Leroy

Détail

Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006), 174/5, pp. 95-108, Electronic Notes in Theoretical Computer Science

Accès au texte intégral et bibtex

Titre

Coinductive big-step operational semantics

Auteurs

Xavier Leroy

Détail

Peter Sestoft. European Symposium on Programming (ESOP 2006), Mar 2006, Vienne, Austria. Springer, Programming Languages and Systems. 15th European Symposium on Programming, ESOP 2006, 3924, pp. 42-54, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Titre

A structured approach to proving compiler optimizations based on dataflow analysis

Auteurs

Yves Bertot; Benjamin Grégoire; Xavier Leroy

Détail

Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. Springer, Types for Proofs and Programs International Workshop, TYPES 2004, Revised Selected Papers, 3839, pp. 66-81, 2006, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

Rapports

Titre

A list-machine benchmark for mechanized metatheory

Auteurs

Andrew W. Appel; Xavier Leroy

Détail

[Research Report], 2006. RR-5914

Accès au texte intégral et bibtex

2005

Articles dans des revues avec comité de lecture

Titre

Mixin modules in a call-by-value setting

Auteurs

Tom Hirschowitz; Xavier Leroy

Détail

ACM Transactions on Programming Languages and Systems, 2005, 27 (5), pp. 857 - 881

Accès au texte intégral et bibtex

Communications avec actes

Titre

Error Mining for Regular Expression Patterns

Auteurs

Giuseppe Castagna; Dario Colazzo; Alain Frisch

Détail

2005. Springer, pp. 160-172, n. 3701, LNCS

Accès au bibtex

Titre

Parametric Polymorphism for XML

Auteurs

Haruo Hosoya; Alain Frisch; Giuseppe Castagna

Détail

2005. ACM Press, pp. 50-62

Accès au bibtex

Titre

EDOS: Environment for the Development and Distribution of Open Source Software

Auteurs

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

Détail

OSS 2005 - The First International Conference on Open Source Systems, Jul 2005, Genova, Italy.

Accès au bibtex

Conférences invitées

Titre

A gentle introduction to semantic subtyping

Auteurs

Giuseppe Castagna; Alain Frisch

Détail

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. Joint ICALP-PPDP keynote talk

Accès au bibtex

2004

Communications avec actes

Titre

Call-by-value mixin modules: Reduction semantics, side effects, types

Auteurs

Tom Hirschowitz; Xavier Leroy; J. B. Wells

Détail

European Symposium on Programming, 2004, Barcelona, Spain. Springer, 2986, pp. 64-78, Lecture Notes in Computer Science

Accès au texte intégral et bibtex

2002

Communications avec actes

Titre

Mixin modules in a call-by-value setting

Auteurs

Tom Hirschowitz; Xavier Leroy

Détail

European Symposium on Programming, 2002, Grenoble, France. Springer, 2305, pp. 207-236, Lecture Notes in Computer Science

Accès au texte intégral et bibtex