gallium.bib

@manual{0000-Ocaml-manual,
  title = {The {Objective} {Caml} system, documentation and
                  user's manual -- release 4.01},
  author = {Xavier Leroy and Damien Doligez and Jacques Garrigue
                  and Didier Rémy and Jérôme Vouillon},
  organization = {INRIA},
  month = sep,
  year = 2013,
  url = {http://caml.inria.fr/pub/docs/manual-ocaml-4.01/},
  raweb = {foot}
}
@manual{0000-CompCert-manual,
  title = {The {CompCert C} verified compiler,
                 documentation and user's manual},
  author = {Xavier Leroy},
  organization = {INRIA},
  month = oct,
  year = 2013,
  url = {http://compcert.inria.fr/man/},
  raweb = {foot}
}
@incollection{1993-Remy-records,
  author = {Didier R{\'e}my},
  title = {Type Inference for Records in a Natural Extension of {ML}},
  booktitle = {Theoretical Aspects Of Object-Oriented Programming.
                  Types, Semantics and Language Design},
  publisher = {MIT Press},
  year = 1993,
  editor = {Carl A. Gunter and John C. Mitchell},
  raweb = {foot}
}
@inproceedings{1993-Doligez-Leroy-gc,
  author = {Damien Doligez and Xavier Leroy},
  title = {A concurrent, generational garbage collector
                         for a multithreaded implementation of {ML}},
  booktitle = {Proc. 20th symp. Principles of Programming Languages},
  year = {1993},
  pages = {113--123},
  publisher = {ACM press},
  url = {http://gallium.inria.fr/~xleroy/publi/concurrent-gc.ps.gz},
  raweb = {foot}
}
@inproceedings{1994-Remy-mlart,
  category = 1,
  author = {Didier R{\'e}my},
  title = {Programming Objects with {ML-ART}:
                  An extension to {ML} with Abstract and Record Types},
  booktitle = {Theoretical Aspects of Computer Software},
  publisher = {Springer-Verlag},
  year = 1994,
  editor = {Masami Hagiya and John C. Mitchell},
  series = {Lecture Notes in Computer Science},
  volume = 789,
  pages = {321--346},
  month = apr,
  raweb = {foot}
}
@book{1995-DiCosmo-iso-book,
  author = {Di Cosmo, Roberto},
  title = {Isomorphisms of Types:
from Lambda Calculus to Information Retrieval and Language Design},
  publisher = {Birkhauser},
  year = 1995,
  raweb = {foot}
}
@article{1996-Leroy-generativity,
  author = {Xavier Leroy},
  title = {A syntactic theory of type generativity
                         and sharing},
  year = 1996,
  journal = {Journal of Functional Programming},
  volume = 6,
  number = 5,
  raweb = {foot},
  pages = {667--698},
  url = {http://gallium.inria.fr/~xleroy/publi/syntactic-generativity.ps.gz},
  abstract = {This paper presents a purely syntactic account of type generativity
and sharing -- two key mechanisms in the Standard ML module system
-- and shows its equivalence with the traditional
stamp-based description of these mechanisms. This syntactic
description recasts the Standard ML module system in a more
abstract, type-theoretic framework.}
}
@inproceedings{1996-Rouaix-MMM,
  author = {Fran\c{c}ois Rouaix},
  title = {A {Web} navigator with applets in {Caml}},
  booktitle = {Proceedings of the 5th International {World} {Wide} {Web}
                  Conference, in {Computer} {Networks} and
                  {Telecommunications} {Networking}},
  volume = {28},
  year = {1996},
  publisher = {Elsevier},
  month = {May},
  pages = {1365--1371},
  raweb = {foot}
}
@inproceedings{1997-Remy-Vouillon,
  author = {Didier R{\'e}my and J{\'e}r{\^o}me Vouillon},
  title = {{Objective} {ML}: A simple object-oriented
                         extension to {ML}},
  booktitle = {24th ACM Conference on Principles
                        of Programming Languages},
  year = {1997},
  pages = {40--53},
  publisher = {ACM Press},
  raweb = {foot}
}
@book{1998-Mauny-Cousineau,
  title = {The Functional Approach to Programming},
  author = {Guy Cousineau and Michel Mauny},
  publisher = {Cambridge University Press},
  year = {1998}
}
@article{1999-Remy-Garrigue,
  author = {Jacques Garrigue and Didier R{\'e}my},
  title = {Extending {ML} with semi-explicit higher-order polymorphism},
  journal = {Information \& Computation},
  year = 1999,
  volume = 155,
  number = {1/2},
  pages = {134--169}
}
@book{1999-Weis-Leroy-livre,
  author = {Pierre Weis and Xavier Leroy},
  title = {Le langage {Caml}},
  publisher = {Dunod},
  year = 1999,
  edition = {second edition},
  month = jul,
  url = {http://caml.inria.fr/pub/distrib/books/llc.pdf}
}
@article{2000-Leroy-JFP,
  author = {Xavier Leroy},
  title = {A modular module system},
  journal = {Journal of Functional Programming},
  year = 2000,
  volume = 10,
  number = 3,
  pages = {269--303},
  url = {http://gallium.inria.fr/~xleroy/publi/modular-modules-jfp.ps.gz}
}
@article{2000-Pottier-NJC,
  author = {François Pottier},
  title = {A Versatile Constraint-Based Type Inference System},
  journal = {Nordic Journal of Computing},
  year = 2000,
  volume = 7,
  number = 4,
  pages = {312--347}
}
@inproceedings{2000-Remy-Fournet-Maranget-Laneve-FSTTSC,
  author = {C{\'e}dric Fournet and Luc Maranget and
                  Cosimo Laneve and Didier R{\'e}my},
  title = {Inheritance in the join calculus},
  booktitle = {Foundations of Software Technology and Theoretical Computer
                  Science -- FSTTCS 2000},
  year = 2000,
  volume = 1974,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  raweb = {foot}
}
@article{2001-Pottier-IC,
  author = {François Pottier},
  title = {Simplifying subtyping constraints: a theory},
  journal = {Information and Computation},
  year = 2001,
  volume = 170,
  number = 2,
  pages = {153--183}
}
@inproceedings{2002-Prevosto-Doligez-Hardin,
  author = {Virgile Prevosto and Damien Doligez and Thérèse Hardin},
  title = {Algebraic Structures and Dependent Records},
  booktitle = {Theorem Proving in Higher Order Logics, TPHOLs 2002},
  series = {Lecture Notes in Computer Science},
  volume = 2410,
  publisher = {Springer},
  pages = {298--313},
  year = 2002
}
@article{2002-Prevosto-Doligez-FOC,
  author = {Virgile Prevosto and Damien Doligez},
  title = {Algorithms and Proofs Inheritance in the {FOC} Language},
  journal = {Journal of Automated Reasoning},
  volume = 29,
  number = {3--4},
  pages = {337-363},
  year = 2002
}
@inproceedings{2002-Hirschowitz-Leroy-ESOP,
  author = {Tom Hirschowitz and Xavier Leroy},
  title = {Mixin modules in a call-by-value setting},
  booktitle = {Programming Languages and Systems -- ESOP'2002},
  pages = {6--20},
  year = 2002,
  editor = {D. {Le M\'etayer}},
  volume = 2305,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  url = {http://gallium.inria.fr/~xleroy/publi/mixins-cbv-esop2002.pdf}
}
@inproceedings{2002-Leroy-Gregoire-ICFP,
  author = {Benjamin Gr{\'e}goire and Xavier Leroy},
  title = {A compiled implementation of strong reduction},
  booktitle = {International Conference on Functional Programming 2002},
  pages = {235--246},
  year = 2002,
  url = {http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf},
  publisher = {ACM Press}
}
@article{2002-Leroy-SPE,
  author = {Xavier Leroy},
  title = {Bytecode verification for {Java} smart card},
  journal = {Software Practice \& Experience},
  year = 2002,
  volume = 32,
  pages = {319--340},
  url = {http://gallium.inria.fr/~xleroy/publi/oncard-verifier-spe.pdf}
}
@inproceedings{2002-Pottier-CSFW,
  author = {François Pottier},
  title = {A Simple View of Type-Secure Information Flow in
                  the $\pi$-Calculus},
  booktitle = {Proceedings of the 15th {IEEE} Computer Security Foundations
                  Workshop},
  pages = {320--330},
  year = 2002,
  month = jun
}
@inproceedings{2002-Pottier-Simonet-POPL,
  author = {François Pottier and Vincent Simonet},
  title = {Information Flow Inference for {ML}},
  booktitle = {Proceedings of the 29th {ACM} Symposium on Principles of
                  Programming Languages (POPL'02)},
  pages = {319--330},
  year = 2002,
  month = jan
}
@inproceedings{2002-Pottier-Skalka-TIP,
  author = {Christian Skalka and François Pottier},
  title = {Syntactic Type Soundness for {$HM(X)$}},
  booktitle = {Proceedings of the 2002 Workshop on Types in Programming
                  (TIP'02)},
  year = 2002,
  month = jun
}
@incollection{2002-Remy-APPSEM,
  author = {Didier R{\'{e}}my},
  title = {{U}sing, {U}nderstanding, and {U}nraveling the
                  {OC}aml {L}anguage},
  booktitle = {{A}pplied {S}emantics. Advanced Lectures},
  pages = {413--537},
  publisher = {Springer},
  year = 2002,
  editor = {Gilles Barthe},
  volume = 2395,
  series = {Lecture Notes in Computer Science},
  url = {http://gallium.inria.fr/~remy/cours/appsem/}
}
@inproceedings{2003-Hirschowitz-Leroy-Wells-PPDP,
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  title = {Compilation of extended recursion
                         in call-by-value functional languages},
  booktitle = {International Conference on Principles and
                         Practice of Declarative Programming},
  year = 2003,
  pages = {160--171},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~xleroy/publi/compil-recursion.pdf},
  abstract = {This paper formalizes and proves correct a compilation scheme for
mutually-recursive definitions in call-by-value functional
languages. This scheme supports a wider range of recursive definitions
than standard call-by-value recursive definitions. We formalize our
technique as a translation scheme to a lambda-calculus featuring
in-place update of memory blocks, and prove the translation to be
faithful.}
}
@phdthesis{2003-Gregoire-these,
  author = {Benjamin Grégoire},
  title = {Compilation de termes de preuves},
  school = {University Paris 7},
  year = 2003,
  month = dec
}
@phdthesis{2003-Hirschowitz-these,
  author = {Tom Hirschowitz},
  title = {Modules mixins, modules et récursion étendue
                         en appel par valeur},
  school = {University Paris 7},
  year = 2003,
  month = dec
}
@article{2003-Leroy-JAR,
  author = {Xavier Leroy},
  title = {{Java} bytecode verification: 
                         algorithms and formalizations},
  journal = {Journal of Automated Reasoning},
  year = 2003,
  volume = 30,
  number = {3--4},
  pages = {235--269},
  url = {http://gallium.inria.fr/~xleroy/publi/bytecode-verification-JAR.pdf},
  abstract = {Bytecode verification is a crucial security component for Java
applets, on the Web and on embedded devices such as smart cards.
This paper reviews the various bytecode verification algorithms that have
been proposed, recasts them in a common framework of dataflow analysis, and 
surveys the use of proof assistants to specify bytecode verification and
prove its correctness.}
}
@inproceedings{2003-Leroy-security-survey,
  author = {Xavier Leroy},
  title = {Computer Security from a Programming Language 
                         and Static Analysis Perspective},
  booktitle = {Programming Languages and Systems:
                         12th European Symposium on Programming, ESOP 2003},
  pages = {1--9},
  volume = 2618,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = 2003,
  editor = {P. Degano},
  note = {Extended abstract of invited lecture}
}
@inproceedings{2003-Leroy-Calcagno-Taha,
  author = {Cristiano Calcagno and Walid Taha and
                         Liwen Huang and Xavier Leroy},
  title = {Implementing Multi-stage Languages Using {ASTs},
                         Gensym, and Reflection},
  booktitle = {Generative Programming and Component Engineering
                         (GPCE'03)},
  year = 2003,
  url = {http://www.cs.rice.edu/~taha/publications/conference/gpce03b.pdf},
  abstract = {Abstract. The paper addresses theoretical and practical aspects of
implementing multi-stage languages using abstract syntax trees (ASTs),
gensym, and reflection. We present an operational account of the
correctness of this approach, and report on our experience with a
bytecode compiler called MetaOCaml that is based on this
strategy. Current performance measurements reveal interesting
characteristics of the underlying OCaml compiler, and illustrate why
this strategy can be particularly useful for implementing
domain-specific languages in a typed, functional setting.}
}
@article{2003-Pottier-Filliatre,
  author = {Jean-Christophe Filliâtre and François Pottier},
  title = {Producing All Ideals of a Forest, Functionally},
  journal = {Journal of Functional Programming},
  month = sep,
  year = 2003,
  volume = 13,
  number = 5,
  pages = {945--956},
  url = {http://gallium.inria.fr/~fpottier/publis/filliatre-pottier.ps.gz},
  abstract = {We present functional implementations of Koda and Ruskey's
		  algorithm for generating all ideals of a forest poset as a Gray
		  code. Using a continuation-based approach, we give an extremely
		  concise formulation of the algorithm's core. Then, in a number of
		  steps, we derive a first-order version whose efficiency is
		  comparable to that of a C implementation given by Knuth.}
}
@article{2003-Pottier-Simonet-TOPLAS,
  author = {François Pottier and Vincent Simonet},
  title = {Information Flow Inference for {ML}},
  journal = {ACM Transactions on Programming Languages and Systems},
  year = 2003,
  month = jan,
  volume = 25,
  number = 1,
  pages = {117--158},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-toplas.ps.gz},
  abstract = {This paper presents a type-based information flow analysis for a call-by-value
		  lambda-calculus equipped with references, exceptions and let-polymorphism,
		  which we refer to as Core ML. The type system is constraint-based and has
		  decidable type inference. Its non-interference proof is reasonably
		  light-weight, thanks to the use of a number of orthogonal techniques. First, a
		  syntactic segregation between values and expressions allows a lighter
		  formulation of the type system. Second, non-interference is reduced to subject
		  reduction for a non-standard language extension. Lastly, a semi-syntactic
		  approach to type soundness allows dealing with constraint-based polymorphism
		  separately.}
}
@inproceedings{2003-LeBotlan-Remy-ICFP,
  author = {{Le Botlan}, Didier  and R{\'e}my, Didier},
  title = {{MLF}: Raising {ML} to the power of {System F}},
  booktitle = {Proceedings of the Eighth {ACM SIGPLAN} International
              Conference on Functional Programming},
  publisher = {ACM Press},
  pages = {27--38},
  year = 2003,
  month = aug,
  url = {http://gallium.inria.fr/~remy/work/mlf/icfp.pdf},
  abstract = {
  We propose a type system {MLF} that generalizes {ML} with first-class
  polymorphism as in System~{F}.  Expressions may contain second-order type
  annotations.  Every typable expression admits a principal type, which
  however depends on type annotations.  Principal types capture all other
  types that can be obtained by implicit type instantiation and they can be
  inferred.  All expressions of ML are well-typed without any annotations.
  All expressionsof System~{F} can be mechanically encoded into {MLF} by
  dropping all type abstractions and type applications, and injecting types of
  lambda-abstractions into {MLF} types.  Moreover, only parameters of
  lambda-abstractions that are used polymorphically need to remain annotated.
}
}
@inproceedings{2003-Pottier-LICS,
  author = {François Pottier},
  title = {A Constraint-Based Presentation and Generalization of Rows},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-lics03.ps.gz},
  booktitle = {Eighteenth Annual {IEEE} Symposium on Logic In Computer Science (LICS'03)},
  pages = {331--340},
  address = {Ottawa, Canada},
  month = jun,
  year = {2003},
  abstract = {We study the combination of possibly conditional non-structural subtyping
		  constraints with rows.  We give a new presentation of rows, where row terms
		  disappear; instead, we annotate constraints with \emph{filters}. We argue
		  that, in the presence of subtyping, this approach is simpler and more general.
		  In the case where filters are finite or cofinite sets of row labels, we give a
		  constraint solving algorithm whose complexity is $O(n^3m\log m)$, where $n$ is
		  the size of the constraint and $m$ is the number of row labels that appear in
		  it. We point out that this allows efficient type inference for record
		  concatenation. Furthermore, by varying the nature of filters, we obtain
		  several natural generalizations of rows.}
}
@phdthesis{2004-LeBotlan-these,
  author = {{Le} {Botlan}, Didier},
  title = {{MLF}: Une extension de {ML} avec
                polymorphisme de second ordre
                et instanciation implicite.},
  school = {{\'E}cole Polytechnique},
  year = 2004,
  month = may,
  url = {http://www.inria.fr/rrrt/tu-1071.html},
  abstract = {
  Nous nous intéressons à une extension de ML avec polymorphisme
  de première classe, à la manière du Système~{F}.
  Cette extension, nommée {MLF}, utilise les annotations de types
  d'ordre supérieur données explicitement dans le programme pour inférer
  de manière principale le type le plus général. Toute expression admet
  ainsi un type principal, qui dépend des annotations présentes
  initialement dans le programme.
  \par
  Toute expression de {ML} est typable dans {MLF} sans annotation
  supplémentaire. Les expressions du Système {F} sont encodées de
  manière systématique dans {MLF} en supprimant les abstractions
  et les applications de types, et en traduisant les annotations
  de types dans le langage de types de {MLF}.
  De plus, les paramètres de lambda-abstractions qui ne sont pas utilisés de
  manière polymorphe n'ont pas besoin d'être annotés.
},
  raweb = {foot}
}
@inproceedings{2004-Bonichon-TaMeD,
  author = {Richard Bonichon},
  title = {{TaMeD}: A Tableau Method for Deduction Modulo},
  booktitle = {Automated Reasoning: Second International Joint
               Conference, IJCAR 2004},
  year = {2004},
  pages = {445-459},
  series = {Lecture Notes in Computer Science},
  volume = 3097,
  publisher = {Springer},
  raweb = {foot}
}
@inproceedings{2004-Frisch-Cardelli-icalp,
  author = {Alain Frisch and Luca Cardelli},
  title = {Greedy regular expression matching},
  booktitle = {31st International Colloquium on Automata, Languages and Programming},
  year = {2004},
  month = jul,
  publisher = {Springer},
  pages = {618-629}
}
@inproceedings{2004-Frisch-tcs,
  author = {Alain Frisch},
  title = {Regular tree language recognition with static information},
  booktitle = {3rd IFIP International Conference on
Theoretical Computer Science},
  year = {2004},
  month = aug,
  publisher = {Kluwer Academic Publishers}
}
@phdthesis{2004-Frisch-these,
  author = {Alain Frisch},
  title = {Théorie, conception et réalisation d'un langage de programmation fonctionnel adapté à XML},
  school = {University Paris 7},
  year = 2004,
  month = dec
}
@inproceedings{2004-Gauthier-Pottier,
  author = {Nadji Gauthier and François Pottier},
  title = {Numbering Matters: First-Order Canonical Forms for Second-Order Recursive Types},
  booktitle = {Proceedings of the 2004 {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'04)},
  url = {http://gallium.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf},
  acm = {http://doi.acm.org/10.1145/1016850.1016872},
  publisher = {ACM Press},
  month = sep,
  year = {2004},
  pages = {150--161},
  abstract = {We study a type system equipped with universal types and equirecursive types,
                  which we refer to as $F_\mu$. We show that type equality may be decided in time
                  $O(n\log n)$, an improvement over the previous known bound of $O(n^2)$. In
                  fact, we show that two more general problems, namely entailment of type
                  equations and type unification, may be decided in time $O(n\log n)$, a new
                  result. To achieve this bound, we associate, with every $F_\mu$ type, a
                  \emph{first-order canonical form}, which may be computed in time $O(n\log n)$.
                  By exploiting this notion, we reduce all three problems to equality and
                  unification of \emph{first-order} recursive terms, for which efficient
                  algorithms are known.}
}
@inproceedings{2004-Hirschowitz-Leroy-Wells,
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  title = {Call-by-Value Mixin Modules: Reduction Semantics, 
                  Side Effects, Types},
  booktitle = {European Symposium on Programming},
  volume = 2986,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {64--78},
  year = {2004},
  url = {http://gallium.inria.fr/~xleroy/publi/mixins-mm-esop2004.ps.gz},
  abstract = {Mixin modules are a framework for modular programming
that supports code parameterization, incremental programming via late
binding and redefinitions, and cross-module recursion.  In this paper,
we develop a language of mixin modules that supports call-by-value
evaluation, and formalize a reduction semantics and a sound type
system for this language.}
}
@inproceedings{2004-Hirschowitz-Leroy-Wells-APPSEM,
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  title = {Extended recursive definitions in call-by-value languages,
           with applications to mixin modules and recursive modules},
  booktitle = {Electronic proceedings of the second APPSEM II Workshop},
  city = {Tallin},
  year = {2004},
  month = apr
}
@inproceedings{2004-Pottier-Gauthier-POPL,
  author = {François Pottier and Nadji Gauthier},
  title = {Polymorphic Typed Defunctionalization},
  booktitle = {31st ACM symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  month = jan,
  year = {2004},
  pages = {89--98},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-popl04.pdf},
  abstract = {\emph{Defunctionalization} is a program transformation that aims to turn a
		  higher-order functional program into a first-order one, that is, to eliminate
		  the use of functions as first-class values.  Its purpose is thus identical to
		  that of \emph{closure conversion}. It differs from closure conversion,
		  however, by storing a \emph{tag}, instead of a code pointer, within every
		  closure. Defunctionalization has been used both as a reasoning tool and as a
		  compilation technique.

		  Defunctionalization is commonly defined and studied in the setting of a
		  simply-typed $\lambda$-calculus, where it is shown that semantics and
		  well-typedness are preserved. It has been observed that, in the setting of a
		  polymorphic type system, such as ML or System F, defunctionalization is not
		  type-preserving. In this paper, we show that extending System F with
		  \emph{guarded algebraic data types} allows recovering type preservation. This
		  result allows adding defunctionalization to the toolbox of type-preserving
		  compiler writers.}
}
@phdthesis{2004-Pottier-hdr,
  author = {François Pottier},
  title = {Types et contraintes},
  school = {Université Paris 7},
  month = dec,
  type = {Mémoire d'habilitation à diriger des recherches},
  year = {2004},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-hdr.pdf}
}
@phdthesis{2004-Simonet-these,
  author = {Vincent Simonet},
  title = {Inférence de flots d'information pour {ML}: 
           formalisation et implantation},
  school = {Université Paris 7},
  year = 2004,
  month = mar,
  url = {http://gallium.inria.fr/~simonet/publis/simonet-these.pdf},
  abstract = {This thesis describes the conception of an information flow
    analyser for a language of the ML family, from its theoretical
    foundation to the practical issues.  The first part of the
    dissertation presents the tool that was implemented, Flow Caml,
    and illustrates its use on concrete example.  The second part
    gives a formalization of the type system featured by Flow Caml,
    together with a proof of its correctness.  This is the first type
    system for information flow analysis in a realistic programming
    language that has been formally proved.  Lastly, the third part is
    devoted to the formalization and the proof of an efficient
    algorithm for type inference in the presence of structural
    subtyping and polymorphism.  An instance of this algorithm is used
    to synthesize types in Flow Caml.}
}
@inproceedings{2004-Starynkevitch-OCamlJIT,
  author = {Basile Starynkevitch},
  title = {{OCamlJIT}: a faster Just-In-Time {OCaml} Implementation},
  booktitle = {First MetaOCaml Workshop},
  year = 2004,
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~starynke/starynke_ocamljit_july2004.ps}
}
@inproceedings{2004-Yakobowski-LOPSTR,
  author = {J. B. Wells and Boris Yakobowski},
  title = {Graph-Based Proof Counting and Enumeration with
                  Applications for Program Fragment Synthesis},
  url = {http://www.yakobowski.org/content/term-enumeration-final.pdf},
  abstract = {For use in earlier approaches to automated module
                  interface adaptation, we seek a restricted form of
                  program synthesis.  Given some typing assumptions and
                  a desired result type, we wish to automatically
                  build a number of program fragments of this chosen
                  typing, using functions and values available in the
                  given typing environment.  We call this problem
                  \emph{term enumeration}.  To solve the problem, we
                  use the Curry-Howard correspondence
                  (propositions-as-types, proofs-as-programs) to
                  transform it into a \emph{proof enumeration} problem
                  for an intuitionistic logic calculus.  We formally
                  study proof enumeration and counting in this
                  calculus.  We prove that proof counting is solvable
                  and give an algorithm to solve it.  This in turn
                  yields a proof enumeration algorithm.},
  year = 2004,
  key = {LO{\relax PSTR} '04},
  booktitle = {International Symposium on Logic-based Program Synthesis and Transformation 2004 (LOPSTR 2004)},
  editor = {Sandro Etalle},
  volume = {3049},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}
@mastersthesis{2004-Yakobowski-DEA,
  author = {Boris Yakobowski},
  title = {Étude sémantique d'un langage intermédiaire de type Static Single Assignment},
  type = {{Master's} dissertation (mémoire de stage de {DEA})},
  school = {ENS Cachan},
  year = {2004},
  month = sep,
  url = {http://www.yakobowski.org/content/rapport-dea.pdf}
}
@techreport{2005-Simonet-Pottier-HMG,
  author = {Vincent Simonet and François Pottier},
  title = {Constraint-Based Type Inference for Guarded Algebraic
                 Data Types},
  month = jan,
  year = {2005},
  institution = {INRIA},
  type = {Research Report},
  number = {5462},
  abstract = {\emph{Guarded} algebraic data types subsume the
                 concepts known in the literature as \emph{indexed
                 types}, \emph{guarded recursive datatype constructors},
                 and \emph{first-class phantom types}, and are closely
                 related to \emph{inductive types}. They have the
                 distinguishing feature that, when typechecking a
                 function defined by cases, every branch may be checked
                 under different assumptions about the type variables in
                 scope. This mechanism allows exploiting the presence of
                 dynamic tests in the code to produce extra static type
                 information.\par We propose an extension of the
                 constraint-based type system {HM$(X)$} with deep
                 pattern matching, guarded algebraic data types, and
                 polymorphic recursion. We prove that the type system is
                 sound and that, provided recursive function definitions
                 carry a type annotation, type inference may be reduced
                 to constraint solving. Then, because solving arbitrary
                 constraints is expensive, we further restrict the form
                 of type annotations and prove that this allows
                 producing so-called \emph{tractable} constraints. Last,
                 in the specific setting of equality, we explain how to
                 solve tractable constraints.\par To the best of our
                 knowledge, this is the first \emph{generic} and
                 \emph{comprehensive} account of type inference in the
                 presence of guarded algebraic data types.},
  url = {http://www.inria.fr/rrrt/rr-5462.html}
}
@inproceedings{2005-Frisch-Hosoya-Castagna-popl,
  author = {Haruo Hosoya and Alain Frisch and Giuseppe Castagna},
  title = {Parametric Polymorphism for {XML}},
  booktitle = {32nd ACM symposium on Principles of Programming Languages},
  pages = {50-62},
  year = {2005},
  month = jan,
  publisher = {ACM Press},
  url = {http://www.cduce.org/papers/polyx.ps.gz},
  abstract = {Although several type systems have been investigated for XML,
parametric polymorphism is rarely treated. This well-established
typing discipline can also be useful in XML processing in particular
for programs involving "parametric schemas," i.e., schemas
parameterized over other schemas (e.g., SOAP). The difficulty in
treating polymorphism for XML lies in how to extend the "semantic"
approach used in the mainstream (monomorphic) XML type systems. A
naive extension would be "semantic" quantification over all
substitutions for type variables. However, this approach reduces to an
NEXPTIME-complete problem for which no practical algorithm is known,
and, moreover, the type system obtained in this way is characterized
by a hardly useful expressiveness. In this paper, we propose a
lighter-weight way of extending the semantic approach, where we
interpret type variables as markings in data values for indicating the
parameterized subparts. As a result, we can construct a sensible
polymorphic type system both with a semantic flavor and a set of
practical algorithms needed for typechecking. Most of these algorithms
can be obtained by local modifications to existing ones for a
monomorphic system.}
}
@incollection{2005-Pottier-Remy-ATTAPL,
  author = {Fran{\c{c}}ois Pottier and Didier R{\'{e}}my},
  booktitle = {Advanced Topics in Types and Programming Languages},
  title = {The Essence of {ML} Type Inference},
  pages = {389--489},
  publisher = {MIT Press},
  year = {2005},
  editor = {Benjamin C. Pierce},
  chapter = {10},
  raweb = {refer}
}
@inproceedings{2005-Remy-icfp,
  author = {Didier R{\'e}my},
  title = {Simple, partial type-inference for System {F}
                  based on type-containment},
  booktitle = {Proceedings of the tenth International Conference
                  on Functional Programming},
  year = {2005},
  month = sep,
  publisher = {ACM Press},
  pages = {130--145},
  url = {http://gallium.inria.fr/~remy/publications.html#Remy/fml},
  html = {http://gallium.inria.fr/~remy/work/fml},
  psgz = {http://gallium.inria.fr/~remy/work/fml/fml-icfp.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/work/fml/fml-icfp.pdf}
}
@inproceedings{2005-Dicosmo-Pottier-Remy-tlca,
  author = {Roberto {Di Cosmo} and François Pottier and Didier Rémy},
  title = {Subtyping Recursive Types modulo Associative
                 Commutative Products},
  psgz = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.ps.gz},
  url = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.pdf},
  long = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.ps.gz},
  longpdf = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.pdf},
  booktitle = {Seventh International Conference on Typed Lambda
                 Calculi and Applications (TLCA'05)},
  address = {Nara, Japan},
  month = apr,
  year = {2005},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = {3461},
  pages = {179--193},
  abstract = {This work sets the formal bases for building tools
                 that help retrieve classes in object-oriented
                 libraries. In such systems, the user provides a query,
                 formulated as a set of class interfaces. The tool
                 returns classes in the library that can be used to
                 implement the user's request and automatically builds
                 the required glue code. We propose subtyping of
                 recursive types in the presence of associative and
                 commutative products---that is, subtyping modulo a
                 restricted form of type isomorphisms---as a model of
                 the relation that exists between the user's query and
                 the tool's answers. We show that this relation is a
                 composition of the standard subtyping relation with
                 equality up to associativity and commutativity of
                 products and we present an efficient decision algorithm
                 for it. We also provide an automatic way of
                 constructing coercions between related types.}
}
@phdthesis{2005-Bonniot-these,
  author = {Daniel Bonniot},
  title = {Typage modulaire des multi-m{\'e}thodes},
  school = {{\'E}cole des Mines de Paris},
  year = 2005,
  month = nov
}
@inproceedings{2005-Frisch-Castagna-Colazzo,
  author = {Giuseppe Castagna and Dario Colazzo and Alain Frisch},
  title = {Error Mining for Regular Expression Patterns},
  booktitle = {9th Italian Conference on Theoretical Computer Science},
  year = {2005},
  month = oct,
  pages = {160-172},
  abstract = {In the design of type systems for XML programming
  languages based on regular expression types and patterns the focus
  has been over result analysis, with the main aim of statically
  checking that a transformation always yields data of an expected
  output type. While being crucial for correct program composition,
  result analysis is not sufficient to guarantee that patterns used in
  the transformation are correct. In this paper we motivate the need
  of static detection of incorrect patterns, and provide a formal
  characterization based on pattern matching operational semantics,
  together with locally exact type analysis techniques to statically
  detect them.}
}
@article{2005-Hirschowitz-Leroy-TOPLAS,
  author = {Tom Hirschowitz and Xavier Leroy},
  title = {Mixin modules in a call-by-value setting},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = 27,
  number = 5,
  pages = {857--881},
  year = 2005,
  url = {http://gallium.inria.fr/~xleroy/publi/mixins-cbv-toplas.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1086642.1086644},
  abstract = {The ML module system provides powerful parameterization facilities,
but lacks the ability to split mutually recursive definitions across
modules, and does not provide enough facilities for incremental
programming.  A promising approach to solve these issues is Ancona and
Zucca's mixin modules calculus CMS.  However, the straightforward
way to adapt it to ML fails, because it allows arbitrary recursive
definitions to appear at any time, which ML does not support.  In
this paper, we enrich CMS with a refined type system that controls
recursive definitions through the use of dependency graphs.  We then
develop a separate compilation scheme, directed by
dependency graphs, that translate mixin modules down to a CBV
lambda-calculus extended with a non-standard let rec construct}
}
@inproceedings{2005-Blazy-Leroy-ICFEM,
  author = {Sandrine Blazy and Xavier Leroy},
  title = {Formal verification of a memory model for
                         {C}-like imperative languages},
  booktitle = {International Conference on
                         Formal Engineering Methods (ICFEM 2005)},
  year = 2005,
  volume = 3785,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {280--299},
  url = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11576280_20},
  abstract = {
This paper presents a formal verification with the Coq proof assistant
of a memory model for C-like imperative languages. This model defines
the memory layout and the operations that manage the memory. The model
has been specified at two levels of abstraction and implemented as
part of an ongoing certification in Coq of a moderately-optimising C
compiler. Many properties of the memory have been verified in the
specification. They facilitate the definition of precise formal
semantics of C pointers. A certified OCaml code implementing the
memory model has been automatically extracted from the
specifications.}
}
@inproceedings{2005-Leroy-EDOS,
  author = {
Serge Abiteboul and
Ciarán Bryce and
Roberto {Di Cosmo} and
Klaus R. Dittrich and
Stéfane Fermigier and
Stéphane Laurière and
Frédéric Lepied and
Xavier Leroy and
Tova Milo and
Eleonora Panto and
Radu Pop and
Assaf Sagi and
Yotam Shtossel and
Florent Villard and
Boris Vrdoljak},
  title = {EDOS: Environment for the Development and
                         Distribution of Open Source Software},
  booktitle = {First International Conference on Open Source Systems
                         (OSS 2005)},
  year = 2005,
  url = {http://oss2005.case.unibz.it/Papers/37.pdf},
  abstract = {
The open-source software community is now
comprised of a very large and growing number of
contributors and users. The GNU/Linux operating system for
instance has an estimated 18 million users worldwide and its
contributing developers can be counted by thousands. The
critical mass of contributors taking part in various opensource
projects has helped to ensure high quality for open
source software. However, despite the achievements of the
open-source software industry, there are issues in the
production of large scale open-source software (OSS) such as
the GNU/Linux operating system that have to be addressed as
the numbers of users, of contributors, and of available
applications grow. EDOS is a European project supported by
IST started October 2004 and ending in 2007, whose
objective is to provide a new generation of methodologies,
theoretical models, technical tools and quality models
specifically tailored to OSS engineering and to software
distribution over the Internet.}
}
@article{2005-Pottier-Skalka-Smith,
  author = {François Pottier and Christian Skalka and Scott
                 Smith},
  title = {A Systematic Approach to Static Access Control},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-skalka-smith-toplas.ps.gz},
  month = mar,
  year = {2005},
  volume = {27},
  number = {2},
  journal = {ACM Transactions on Programming Languages and
                 Systems},
  abstract = {The Java Security Architecture includes a dynamic mechanism for
enforcing access control checks, the so-called stack inspection
process. While the architecture has several appealing features, access
control checks are all implemented via dynamic method calls. This is a
highly non-declarative form of specification which is hard to read,
and which leads to additional run-time overhead. This paper develops
type systems which can statically guarantee the success of these
checks. Our systems allow security properties of programs to be
clearly expressed within the types themselves, which thus serve as
static declarations of the security policy. We develop these systems
using a systematic methodology: we show that the security-passing
style translation, proposed by Wallach, Appel and Felten as a dynamic
implementation technique, also gives rise to static security-aware
type systems, by composition with conventional type systems. To define
the latter, we use the general HM(X) framework, and easily construct
several constraint- and unification-based type systems.}
}
@inproceedings{2005-Pottier-Regis-Gianas-Typed-LR,
  author = {François Pottier and Yann {Régis-Gianas}},
  title = {Towards efficient, typed {LR} parsers},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.pdf},
  month = sep,
  year = {2005},
  booktitle = {ACM Workshop on ML},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {148(2)},
  pages = {155--180},
  abstract = {The LR parser generators that are bundled with many
functional programming language implementations produce code that is
untyped, needlessly inefficient, or both. We show that, using
generalized algebraic data types, it is possible to produce parsers
that are well-typed (so they cannot unexpectedly crash or fail) and
nevertheless efficient. This is a pleasing result as well as an
illustration of the new expressiveness offered by generalized
algebraic data types.}
}
@mastersthesis{2005-Dargaye,
  author = {Zaynah Dargaye},
  title = {Éléments de preuve pour un compilateur certifié de {C}},
  school = {Universit\'e Paris 7},
  year = {2005},
  type = {Master's thesis}
}
@inproceedings{2005-Frisch-Castagna-GentleIntroduction,
  author = {Giuseppe Castagna and Alain Frisch},
  title = {A Gentle Introduction to Semantic Subtyping},
  booktitle = {International Conference on Principles and Practice of Declarative Programming},
  pages = {198-199},
  note = {Abstract of invited lecture},
  year = {2005},
  month = jul,
  publisher = {ACM Press}
}
@article{2005-Prevosto-Delahaye-Jaume-coqdess,
  author = {David Delahaye and Mathieu Jaume and Virgile Prevosto},
  title = {Coq, un outil pour l'enseignement},
  journal = {Technique et Science Informatique},
  year = 2005,
  volume = 24,
  number = 9,
  pages = {1139-1160}
}
@inproceedings{2005-Pottier-AlphaCaml,
  author = {François Pottier},
  title = {An overview of {C$\alpha$ml}},
  month = sep,
  year = {2005},
  booktitle = {ACM Workshop on ML},
  pages = {27--52},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {148(2)},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-alphacaml.pdf},
  abstract = {C$\alpha$ml is a tool that turns a so-called ``binding
specification'' into an Objective Caml compilation unit. A binding
specification resembles an algebraic data type declaration, but also
includes information about names and binding. C$\alpha$ml is meant to
help writers of interpreters, compilers, or other
programs-that-manipulate-programs deal with $\alpha$-conversion in a
safe and concise style. This paper presents an overview of
C$\alpha$ml's binding specification language and of the code that
C$\alpha$ml produces.}
}
@inproceedings{2005-Yakobowski-APPSEMII,
  author = {Didier R\'emy and Boris Yakobowski},
  title = {{MLF} with Graphs},
  booktitle = {Proceedings 3rd APPSEM II Worshop},
  year = 2005,
  month = {sept}
}
@inproceedings{2006-Durak-Leroy-ASE06,
  title = {Managing the Complexity of Large Free and
                         Open Source Package-Based Software Distributions},
  author = {Fabio Mancinelli and Roberto {Di Cosmo} and
                         Jérôme Vouillon and Jaap Boender and Berke Durak
                         and Xavier Leroy and Ralf Treinen},
  booktitle = {21st IEEE Int. Conf. on Automated Software Engineering
                         (ASE 2006)},
  pages = {199--208},
  publisher = {IEEE Computer Society Press},
  year = 2006,
  url = {http://doi.ieeecomputersociety.org/10.1109/ASE.2006.49}
}
@inproceedings{2006-Durak-Leroy-FRCSS06,
  title = {Maintaining large software distributions:
                         new challenges from the {FOSS} era},
  author = {Roberto {Di Cosmo} and Berke Durak and Xavier Leroy
                         and Fabio Mancinelli and Jérôme Vouillon},
  booktitle = {Proceedings of the FRCSS 2006 workshop},
  series = {EASST Newsletter},
  volume = {12},
  pages = {7--20},
  year = 2006,
  url = {http://gallium.inria.fr/~xleroy/publi/edos-frcss06.pdf},
  abstract = {In the mainstream adoption of free and open source software (FOSS),
distribution editors play a crucial role: they package, integrate and
distribute a wide variety of software, written in a variety of
languages, for a variety of purposes of unprecedented breadth.
Ensuring the quality of a FOSS distribution is a technical and
engineering challenge, owing to the size and complexity of these
distributions (tens of thousands of software packages). A number of
original topics for research arise from this challenge. This paper is
a gentle introduction to this new research area, and strives to
clearly and formally identify many of the desirable properties that
must be enjoyed by these distributions to ensure an acceptable quality
level.}
}
@inproceedings{2006-Durak-Leroy-WFS06,
  author = {Jaap Boender and Roberto {Di Cosmo} and
                         Berke Durak and Xavier Leroy and
                         Fabio Mancinelli and Mario Morgado
                         and David Pinheiro and Ralf Treinen
                         and Paulo Trezentos and Jérôme Vouillon},
  title = {News from the {EDOS} project:
                         improving the maintenance of
                         free software distributions},
  booktitle = {Proceedings of the VIIth International Workshop on Free Software (IWFS'06)},
  pages = {199--207},
  mon = apr,
  year = 2006,
  city = {Porto Alegre, Brasil},
  url = {http://www.edos-project.org/xwiki/bin/download/Main/Publications/wsl06.pdf}
}
@inproceedings{2006-Frisch-planx,
  author = {Alain Frisch},
  title = {{OCaml} + {XDuce}},
  booktitle = {Workshop Programming Language Technologies for XML (PLAN-X) 2006},
  year = {2006},
  pages = {36--48},
  publisher = {BRICS Notes series NS-05-6, University of Aarhus},
  month = jan
}
@inproceedings{2006-Leroy-Bertot-Gregoire,
  author = {Yves Bertot and Benjamin Grégoire and Xavier Leroy},
  title = {A structured approach to proving compiler
                         optimizations based on dataflow analysis},
  booktitle = {Types for Proofs and Programs, Workshop TYPES 2004},
  year = 2006,
  volume = 3839,
  pages = {66-81},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  url = {http://gallium.inria.fr/~xleroy/publi/proofs_dataflow_optimizations.pdf},
  abstract = {
This paper reports on the correctness proof of compiler optimizations
based on data-flow analysis.  We formulate the optimizations and
analyses as instances of a general framework for data-flow analyses and
transformations, and prove that the optimizations preserve the
behavior of the compiled programs.  This development is a part of a
larger effort of certifying an optimizing compiler by proving semantic
equivalence between source and compiled code.}
}
@inproceedings{2006-Leroy-compcert,
  author = {Xavier Leroy},
  title = {Formal certification of a compiler back-end, or:
                   programming a compiler with a proof assistant},
  booktitle = {33rd ACM symposium on Principles of Programming Languages},
  year = 2006,
  publisher = {ACM Press},
  pages = {42--54},
  url = {http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1111037.1111042},
  abstract = {This paper reports on the development and formal certification (proof
of semantic preservation) of a compiler from Cminor (a C-like
imperative language) to PowerPC assembly code, using the Coq proof
assistant both for programming the compiler and for proving its
correctness.  Such a certified compiler is useful in the context of
formal methods applied to the certification of critical software: the
certification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as well.}
}
@inproceedings{2006-Leroy-coindsem,
  author = {Xavier Leroy},
  title = {Coinductive big-step operational semantics},
  booktitle = {European Symposium on Programming (ESOP'06)},
  year = 2006,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 3924,
  pages = {54-68},
  url = {http://gallium.inria.fr/~xleroy/publi/coindsem.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/11693024_5},
  abstract = {This paper illustrates the use of co-inductive definitions and proofs
in big-step operational semantics, enabling the latter to describe
diverging evaluations in addition to terminating evaluations. We show
applications to proofs of type soundness and to proofs of semantic
preservation for compilers.  (See
\verb|http://gallium.inria.fr/~xleroy/publi/coindsem/|
for the Coq on-machine formalization of these results.)}
}
@inproceedings{2006-Leroy-Blazy-Dargaye,
  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
  title = {Formal Verification of a {C} Compiler Front-End},
  booktitle = {FM 2006: Int. Symp. on Formal Methods},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 4085,
  year = 2006,
  pages = {460--475},
  url = {http://gallium.inria.fr/~xleroy/publi/cfront.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/11813040_31},
  raweb = {foot},
  abstract = {This paper presents the formal verification of a compiler front-end
that translates a subset of the C language into the Cminor
intermediate language.  The semantics of the source and target
languages as well as the translation between them have been written in
the specification language of the Coq proof assistant. The proof of
observational semantic equivalence between the source and generated
code has been machine-checked using Coq.  An executable compiler was
obtained by automatic extraction of executable Caml code from the Coq
specification of the translator, combined with a certified compiler
back-end generating PowerPC assembly code from Cminor, described in
previous work.}
}
@techreport{2006-Leroy-Appel-listmachine-tr,
  author = {Appel, Andrew W.  and  Leroy, Xavier},
  title = {A list-machine benchmark for mechanized metatheory},
  year = {2006},
  institution = {INRIA},
  number = {5914},
  type = {Research report},
  url = {http://www.inria.fr/rrrt/rr-5914.html},
  abstract = {We propose a benchmark to compare theorem-proving systems
on their ability to express proofs of compiler correctness.
In contrast to the first POPLmark, we emphasize the connection
of proofs to compiler implementations, and we point out
that much can be done without binders or alpha-conversion.
We propose specific criteria for evaluating the utility
of mechanized metatheory systems; we have constructed
solutions in both Coq and Twelf metatheory, and
we draw conclusions about those two systems in particular.}
}
@incollection{2006-Mauny-Chailloux-EncycloVuibert,
  author = {Emmanuel Chailloux and Michel Mauny},
  publisher = {Éditions Vuibert},
  booktitle = {Encyclopédie des systèmes d'information},
  title = {Programmation fonctionnelle},
  pages = {1016--1027},
  year = 2006
}
@inproceedings{2006-Mauny-Henry-Chailloux-JFLA,
  author = {Grégoire Henry and Michel Mauny and Emmanuel Chailloux},
  title = {Typer la dé-sérialisation sans sérialiser les types},
  booktitle = {Journées francophones des langages applicatifs},
  year = {2006},
  month = jan,
  pages = {133--146},
  url = {http://jfla.inria.fr/2006/actes/PDF/09_henry.pdf},
  publisher = {INRIA}
}
@inproceedings{2006-Pottier-Regis-Gianas-GADTs,
  author = {François Pottier and Yann Régis-Gianas},
  title = {Stratified type inference for generalized algebraic
                 data types},
  booktitle = {33rd ACM symposium on Principles of Programming Languages},
  pages = {232--244},
  month = jan,
  year = {2006},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf},
  abstract = {We offer a solution to the type inference problem for an extension of
Hindley and Milner's type system with generalized algebraic data
types. Our approach is in two strata. The bottom stratum is a core
language that marries type inference in the style of Hindley and
Milner with type checking for generalized algebraic data types. This
results in an extremely simple specification, where case constructs
must carry an explicit type annotation and type conversions must be
made explicit. The top stratum consists of (two variants of) an
independent shape inference algorithm. This algorithm accepts a source
term that contains some explicit type information, propagates this
information in a local, predictable way, and produces a new source
term that carries more explicit type information. It can be viewed as
a preprocessor that helps produce some of the type annotations
required by the bottom stratum. It is proven sound in the sense that
it never inserts annotations that could contradict the type derivation
that the programmer has in mind.}
}
@inproceedings{2006-Frisch-icfp,
  author = {Alain Frisch},
  title = {{OCaml} + {XDuce}},
  booktitle = {Proceedings of the Eleventh {ACM SIGPLAN} 
               International Conference on Functional Programming},
  pages = {192--200},
  year = 2006,
  month = sep,
  publisher = {ACM Press},
  url = {http://doi.acm.org/10.1145/1159803.1159829}
}
@mastersthesis{2006-Tristan-MPRI,
  author = {Jean-Baptiste Tristan},
  title = {Certification d'un validateur de transformations},
  type = {{Master's} dissertation (mémoire de stage de {Master 2})},
  school = {ENS Paris},
  year = {2006},
  month = sep,
  url = {http://gallium.inria.fr/~tristan/rapport.pdf}
}
@article{2006-Pottier-Gauthier-HOSC,
  author = {François Pottier and Nadji Gauthier},
  title = {Polymorphic Typed Defunctionalization and
                 Concretization},
  journal = {Higher-Order and Symbolic Computation},
  volume = {19},
  number = {1},
  pages = {125--162},
  month = mar,
  year = {2006},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf},
  abstract = {Defunctionalization is a program transformation that eliminates
functions as first-class values. We show that defunctionalization can
be viewed as a type-preserving transformation of an extension of with
guarded algebraic data types into itself. We also suggest that
defunctionalization is an instance of concretization, a more general
technique that allows eliminating constructs other than functions. We
illustrate this point by presenting two new type-preserving
transformations that can be viewed as instances of concretization. One
eliminates Rémy-style polymorphic records; the other eliminates the
dictionary records introduced by the standard compilation scheme for
Haskell's type classes.}
}
@phdthesis{2006-Bonichon-these,
  author = {Richard Bonichon},
  title = {Tableaux et D{\'e}duction Modulo},
  school = {University Paris 6},
  year = 2006,
  month = dec
}
@inproceedings{2007-Blazy-Appel-Cminor-sos,
  author = {Andrew W. Appel and Sandrine Blazy},
  title = {Separation logic for small-step {Cminor}},
  booktitle = {Theorem Proving in Higher Order Logics, 20th
                         Int. Conf. TPHOLs 2007},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4732,
  pages = {5--21},
  year = 2007,
  mon = sep,
  url = {http://www.ensiie.fr/~blazy/AppelBlazy07.pdf},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2007-Blazy-C-semantics,
  author = {Sandrine Blazy},
  title = {Experiments in validating formal semantics for {C}},
  booktitle = {Proceedings of the C/C++ Verification Workshop},
  pages = {95--102},
  year = 2007,
  mon = jul,
  url = {http://www.ensiie.fr/~blazy/C07Blazy.pdf},
  publisher = {Technical report ICIS-R07015, Radboud University Nijmegen},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@mastersthesis{2007-Chargueraud-M2,
  author = {Arthur Charguéraud},
  title = {Proof of imperative programs},
  type = {{Master's} dissertation (m\'{e}moire de stage de {Master 2})},
  school = {ENS Lyon},
  year = 2007,
  month = sep
}
@inproceedings{2007-Dargaye-JFLA,
  author = {Zaynah Dargaye},
  title = {Décurryfication certifiée},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'07)},
  pages = {119--134},
  publisher = {INRIA},
  year = {2007},
  url = {http://gallium.inria.fr/~dargaye/publications/certdec.pdf},
  x-international-audience = {no},
  x-proceedings = {yes}
}
@inproceedings{2007-Dargaye-Leroy-LPAR,
  author = {Zaynah Dargaye and Xavier Leroy},
  title = {Mechanized verification of {CPS} transformations},
  booktitle = {Logic for Programming,
                     Artificial Intelligence and Reasoning,
                     14th Int. Conf. LPAR 2007},
  year = 2007,
  series = {Lecture Notes in Artificial Intelligence},
  volume = 4790,
  publisher = {Springer},
  pages = {211--225},
  url = {http://gallium.inria.fr/~xleroy/publi/cps-dargaye-leroy.pdf},
  abstract = {
Transformation to continuation-passing style (CPS) is often performed
by optimizing compilers for functional programming languages.  As part
of the development and proof of correctness of a compiler for the
mini-ML functional language, we have mechanically verified the
correctness of two CPS transformations for a call-by-value
$\lambda$-calculus with $n$-ary functions, recursive functions, data
types and pattern-matching.  The transformations generalize Plotkin's
original call-by-value transformation and Danvy and Nielsen's
optimized transformation, respectively.  We used the Coq proof
assistant to formalize the transformations and conduct and check the
proofs.  Originalities of this work include the use of big-step
operational semantics to avoid difficulties with administrative
redexes, and of two-sorted de Bruijn indices to avoid difficulties
with $\alpha$-conversion.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2007-Doligez-Bonichon-Delahaye,
  author = {Richard Bonichon and David Delahaye and Damien Doligez},
  title = {{Zenon}: an Extensible Automated Theorem Prover Producing Checkable Proofs},
  booktitle = {Logic for Programming,
                     Artificial Intelligence and Reasoning,
                     14th Int. Conf. LPAR 2007},
  year = 2007,
  series = {Lecture Notes in Artificial Intelligence},
  volume = 4790,
  publisher = {Springer},
  pages = {151--165},
  url = {http://focal.inria.fr/zenon/zenlpar07.pdf},
  abstract = {
We present Zenon, an automated theorem prover for first order
classical logic (with equality), based on the tableau method. Zenon is
intended to be the dedicated prover of the Focal environment, an
object-oriented algebraic specification and proof system, which is
able to produce OCaml code for execution and Coq code for
certification. Zenon can directly generate Coq proofs (proof
scripts or proof terms), which can be reinserted in the Coq
specifications produced by Focal. Zenon can also be extended,
which makes specific (and possibly local) automation possible
in Focal.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@techreport{2007-Leroy-POPLmark,
  author = {Xavier Leroy},
  title = {A locally nameless solution to the {POPLmark} challenge},
  year = {2007},
  month = jan,
  institution = {INRIA},
  number = {6098},
  type = {Research report},
  url = {http://hal.inria.fr/inria-00123945},
  abstract = {
The POPLmark challenge is a collective experiment intended to assess
the usability of theorem provers and proof assistants in the context
of fundamental research on programming languages.  In this report,
we present a solution to the challenge, developed with the Coq proof
assistant, and using the ``locally nameless'' presentation of terms with
binders introduced by McKinna, Pollack, Gordon, and McBride.}
}
@inproceedings{2007-Leroy-Appel-listmachine-lfmtp,
  author = {Appel, Andrew W.  and  Leroy, Xavier},
  title = {A list-machine benchmark for mechanized metatheory
                       (extended abstract)},
  booktitle = {Proc. Int. Workshop on Logical
                       Frameworks and Meta-Languages (LFMTP'06)},
  year = {2007},
  series = {Electronic Notes in Computer Science},
  volume = {174(5)},
  pages = {95--108},
  url = {http://gallium.inria.fr/~xleroy/publi/listmachine-lfmtp.pdf},
  urlpublisher = {http://dx.doi.org/10.1016/j.entcs.2007.01.020},
  abstract = {Short version of \cite{2006-Leroy-Appel-listmachine-tr}.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2007-Frisch-planx,
  author = {Alain Frisch and Keisuke Nakano},
  title = {Streaming {XML} Transformations Using Term Rewriting},
  booktitle = {Workshop Programming Language Technologies for XML (PLAN-X 2007)},
  year = {2007},
  month = jan,
  pages = {2--13},
  url = {http://www.plan-x-2007.org/plan-x-2007.pdf},
  x-international-audience = {yes},
  x-proceedings = {no}
}
@inproceedings{2007-Frisch-DBPL,
  author = {Alain Frisch and Haruo Hosoya},
  title = {Towards Practical Typechecking for Macro Tree Transducers},
  booktitle = {Database Programming Languages,
                  11th International Symposium, DBPL 2007},
  year = 2007,
  series = {Lecture Notes in Computer Science},
  volume = 4797,
  pages = {246--260},
  publisher = {Springer},
  url = {http://dx.doi.org/10.1007/978-3-540-75987-4_17},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@mastersthesis{2007-Montagu-M2,
  author = {Benoît Montagu},
  title = {Modules de première classe},
  type = {{Master's} dissertation (m\'{e}moire de stage de {Master 2})},
  school = {École Polytechnique},
  year = 2007,
  month = sep,
  url = {http://gallium.inria.fr/~montagu/publications/2007/modules.pdf}
}
@article{2007-Simonet-Pottier-hmg-toplas,
  author = {Vincent Simonet and François Pottier},
  title = {A Constraint-Based Approach to Guarded Algebraic Data Types},
  month = jan,
  year = {2007},
  journal = {ACM Transactions on Programming Languages and
                 Systems},
  volume = {29},
  number = {1},
  pages = {article no. 1},
  url = {http://gallium.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.ps.gz},
  urlpublisher = {http://doi.acm.org/10.1145/1180475.1180476},
  abstract = {We study {HMG$(X)$}, an extension of the
                 constraint-based type system {HM$(X)$} with deep
                 pattern matching, polymorphic recursion, and guarded
                 algebraic data types. Guarded algebraic data types
                 subsume the concepts known in the literature as indexed
                 types, guarded recursive datatype constructors,
                 (first-class) phantom types, and equality qualified
                 types, and are closely related to inductive types.
                 Their characteristic property is to allow every branch
                 of a case construct to be typechecked under different
                 assumptions about the type variables in scope. We prove
                 that {HMG$(X)$} is sound and that, provided recursive
                 definitions carry a type annotation, type inference can
                 be reduced to constraint solving. Constraint solving is
                 decidable, at least for some instances of $X$, but
                 prohibitively expensive. Effective type inference for
                 guarded algebraic data types is left as an issue for
                 future research.},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  raweb = {foot}
}
@inproceedings{2007-Pottier-pure-freshml,
  author = {François Pottier},
  title = {Static Name Control for {FreshML}},
  month = jul,
  year = {2007},
  booktitle = {Twenty-Second Annual {IEEE} Symposium on Logic In
                 Computer Science (LICS'07)},
  publisher = {IEEE Computer Society Press},
  pages = {356--365},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml.ps.gz},
  urlpublisher = {http://dx.doi.org/10.1109/LICS.2007.44},
  abstract = {FreshML extends ML with constructs for declaring and
                 manipulating abstract syntax trees that involve names
                 and statically scoped binders. It is impure: name
                 generation is an observable side effect. In practice,
                 this means that FreshML allows writing programs that
                 create fresh names and unintentionally fail to bind
                 them. Following in the steps of early work by Pitts and
                 Gabbay, this paper defines Pure FreshML, a subset of
                 FreshML equipped with a static proof system that
                 guarantees purity. Pure FreshML relies on a rich
                 binding specification language, on user-provided
                 assertions, expressed in a logic that allows reasoning
                 about values and about the names that they contain, and
                 on a conservative, automatic decision procedure for
                 this logic. It is argued that Pure FreshML can express
                 non-trivial syntax-manipulating algorithms.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@mastersthesis{2007-Ramananandro,
  author = {Tahina Ramananandro},
  title = {V\'{e}rification formelle d'une impl\'{e}mentation d'un gestionnaire
           de m\'{e}moire pour un compilateur certifi\'{e}},
  type = {{Master's} dissertation (m\'{e}moire de stage de {Master 2})},
  school = {ENS Paris},
  year = {2007},
  month = sep,
  url = {http://www.eleves.ens.fr/~ramanana/travail/gc}
}
@inproceedings{2007-Remy-Yakobowski-TLDI,
  author = {Didier R{\'e}my and Boris Yakobowski},
  title = {A graphical presentation of {MLF} types with
                  a linear-time incremental unification algorithm.},
  booktitle = {{ACM} {SIGPLAN} Workshop on {T}ypes in {L}anguage {D}esign
                  and {I}mplementation},
  url = {http://gallium.inria.fr/~remy/project/mlf/mlf-graphic-types.pdf},
  year = 2007,
  month = jan,
  publisher = {ACM Press},
  pages = {27--38},
  abstract = {
MLF is a language that extends ML and System F and combines the benefits
of both. We propose a dag representation of MLF types that superposes a
term-dag, encoding the underlying term-structure with sharing, and a
binding tree encoding the binding-structure. Compared to the original
definition, this representation is more canonical as it factors out most
of the notational details; it is also closely related to first-order
terms. Moreover, it permits a simpler and more direct definition of type
instance that combines type instance on first-order term-dags, simple
operations on dags, and a control that allows or rejects potential
instances. Using this representation, we build a linear-time unification
algorithm for MLF types, which we prove sound and complete with respect
to the specification. 
},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@unpublished{2006-Remy-Yakobowski-TLDI-long,
  author = {Didier R{\'e}my and Boris Yakobowski},
  title = {A graphical presentation of {MLF} types with
                  a linear-time incremental unification algorithm.},
  url = {http://gallium.inria.fr/~remy/publications.html#Remy/mlf-graphic-types},
  html = {http://gallium.inria.fr/~remy/project/mlf},
  psgz = {http://gallium.inria.fr/~remy/project/mlf/mlf-graphic-types.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/project/mlf/mlf-graphic-types.pdf},
  year = 2006,
  month = sep,
  note = {Extended version of the TLDI'07 article},
  abstract = {
MLF is a language that extends ML and System F and combines the benefits
of both. We propose a dag representation of MLF types that superposes a
term-dag, encoding the underlying term-structure with sharing, and a
binding tree encoding the binding-structure. Compared to the original
definition, this representation is more canonical as it factors out most
of the notational details; it is also closely related to first-order
terms. Moreover, it permits a simpler and more direct definition of type
instance that combines type instance on first-order term-dags, simple
operations on dags, and a control that allows or rejects potential
instances. Using this representation, we build an incremental linear-time
unification algorithm for MLF types, which we prove sound and complete
with respect to the specification. 
}
}
@techreport{2007-Lebotlan-Remy-recasting-mlf-RR,
  author = {Le Botlan, Didier  and  R{\'{e}}my, Didier},
  title = {Recasting {MLF}},
  year = {2007},
  month = jun,
  institution = {INRIA},
  number = {6228},
  type = {Research report},
  url = {http://hal.inria.fr/inria-00156628},
  abstract = {The language MLF has been proposed as an alternative to System F
that permits partial type inference a la ML.  It differs from
System F by its types and type-instance relation. Unfortunately,
the definition of type instance is only syntactic, and not
underpined by some underlying semantics. It has so far only been
justified a posteriori by the type soundness result.

In this work, we revisit MLF following a more progressive
approach stepping on System F.  We argue that System F is not a
well-suited language for ML-style type inference because it
fails to factorize some closely related typing derivations. We
solve this problem in Curry's style MLF by enriching types with
a new form of quantification that may represent a whole
collection of System F types.  This permits a natural
interpretation of MLF types as sets of System-F types and
pulling back the instance relation from set inclusion on the
interpretations. We also give an equivalent syntactic definition
of the type-instance, presented as a set of inference rules.

We derive a Church's style version of MLF by further refining
types so as to distinguish between user-provided and inferred
type information.  The resulting language is more canonical than
the one originally proposed. We show an embedding of ML in MLF
and an encoding of System F into MLF.  Besides, as MLF is more
expressive than System F, an encoding of MLF is given towards an
extension of System F with local binders.}
}
@article{2007-Blazy-C-chronique,
  author = {Sandrine Blazy},
  title = {Comment gagner confiance en {C} ?},
  journal = {Technique et Science Informatiques},
  year = {2007},
  volume = {26},
  number = {9},
  pages = {1195-1200},
  url = {http://www.ensiie.fr/~blazy/TSI07Blazy.pdf},
  x-international-audience = {no},
  x-editorial-board = {yes}
}
@inproceedings{2007-Blazy-JGA,
  author = {Sandrine Blazy and Benoît Robillard and Éric Soutif},
  title = {Coloration avec préférences dans les graphes triangulés},
  booktitle = {Journées Graphes et Algorithmes (JGA'07)},
  year = {2007},
  month = {nov},
  url = {http://www.ensiie.fr/~blazy/JGA07.pdf},
  x-international-audience = {no},
  x-proceedings = {no}
}
@techreport{2007-Blazy-Appel-Cminor-sosRR,
  author = {Andrew W. Appel and Sandrine Blazy},
  title = {Separation logic for small-step {Cminor} (extended version)},
  year = 2007,
  mon = mar,
  institution = {INRIA},
  number = {6138},
  type = {Research report},
  url = {http://hal.inria.fr/inria-00134699/}
}
@phdthesis{2007-Regis-Gianas,
  author = {Yann Régis-Gianas},
  title = {Des types aux assertions logiques: Preuve automatique ou assistée de propriétés sur les programmes fonctionnels},
  school = {University Paris Diderot (Paris~7)},
  month = nov,
  year = 2007,
  url = {http://www.pps.jussieu.fr/~yrg/research/papers/phd-yann.regis-gianas.pdf},
  note = {English title: From types to logical assertions: automated or assisted proof of properties over functional programs}
}
@inproceedings{2007-Tolmach-GHC,
  author = {Peng Li and Simon Marlow and Simon {Peyton Jones} and Andrew Tolmach},
  title = {Lightweight concurrency primitives for {GHC}},
  booktitle = {Haskell '07: Proceedings of the ACM SIGPLAN workshop on Haskell},
  year = {2007},
  pages = {107--118},
  url = {http://doi.acm.org/10.1145/1291201.1291217},
  publisher = {ACM Press},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2008-Blazy-JFLA,
  author = {Sandrine Blazy and Benoît Robillard and Éric Soutif},
  title = {Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'08)},
  year = 2008,
  address = {Étretat, France},
  month = jan,
  pages = {31--46},
  url = {http://www.ensiie.fr/~blazy/JFLABRS08.pdf},
  urlpublisher = {http://hal.inria.fr/inria-00202713/},
  publisher = {INRIA},
  x-international-audience = {no},
  x-proceedings = {yes}
}
@phdthesis{2008-Blazy-HDR,
  author = {Sandrine Blazy},
  title = {Sémantiques formelles},
  type = {Habilitation à diriger les recherches},
  school = {Université Évry Val d'Essone},
  year = 2008,
  month = oct,
  url = {http://tel.archives-ouvertes.fr/tel-00336576/},
  note = {English title: Formalized semantics}
}
@inproceedings{2008-Blazy-ROADEF,
  author = {Sandrine Blazy and Benoît Robillard and Éric Soutif},
  title = {Coloration avec préférences: complexité,
                         inégalités valides et vérification formelle},
  booktitle = {ROADEF'08, 9e congrès de la Société Française de
                         Recherche Opérationnelle et d'Aide à la Décision},
  year = {2008},
  month = feb,
  url = {http://hal.inria.fr/inria-00260712},
  x-international-audience = {no},
  x-proceedings = {yes}
}
@inproceedings{2008-Chargueraud-POPL,
  author = {Brian Aydemir and Arthur Charguéraud and 
                  Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
  title = {Engineering Formal Metatheory},
  booktitle = {Proceedings of the 35th {ACM} Symposium on Principles of
                  Programming Languages (POPL'08)},
  pages = {3--15},
  publisher = {ACM Press},
  year = 2008,
  month = jan,
  url = {http://www.chargueraud.org/arthur/research/2007/binders/binders_popl_08.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1328897.1328443},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@inproceedings{2008-Chargueraud-Pottier-ICFP,
  author = {Arthur Charguéraud and François Pottier},
  title = {Functional Translation of a Calculus of Capabilities},
  booktitle = {Proceedings of the 13th International Conference on Functional Programming (ICFP'08)},
  year = 2008,
  month = sep,
  publisher = {ACM Press},
  pages = {213--224},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilities.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1411204.1411235},
  raweb = {refer},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@article{2008-Doligez-Berthouly-Doligez-Tanner-Saladin-Bonfils-Richner,
  author = {Blandine Doligez and Anne Berthouly and
                         Damien Doligez and Marion Tanner and Verena Saladin
                         and Danielle Bonfils and Heinz Richner},
  title = {Spatial scale of local breeding habitat quality and adjustment of breeding decisions in a wild tit population},
  journal = {Ecology},
  issn = {0012-9658},
  volume = 89,
  number = 5,
  pages = {1436--1444},
  year = 2008,
  urlpublisher = {http://www.esajournals.org/doi/abs/10.1890/07-0113.1},
  abstract = {
Experimental studies provide evidence that, in spatially and temporally
heterogeneous environments, individuals track variation in breeding
habitat quality to adjust breeding decisions to local conditions.
However, most experiments consider environmental variation at one
spatial scale only, while the ability to detect the influence of a
factor depends on the scale of analysis. We show that different
breeding decisions by adults are based on information about habitat
quality at different spatial scales. We manipulated (increased or
decreased) local breeding habitat quality through food availability
and parasite prevalence at a small (territory) and a large (patch)
scale simultaneously in a wild population of great tits. Females
laid earlier in high-quality large-scale patches, but laying date
did not depend on small-scale territory quality. Conversely,
offspring sex ratio was higher (i.e. male-biased) in high-quality
small scale territories, but did not depend on large-scale patch
quality. Clutch size and territory occupancy probability did not
depend on our experimental manipulation of habitat quality, but
territories located at the edge of patches were more likely to be
occupied than central territories. These results suggest that
integrating different decisions taken by breeders according to
environmental variation at different spatial scales is required
to understand patterns of breeding strategies adjustment.},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {CH}
}
@inproceedings{2008-Doligez-Cuoq-weak,
  author = {Pascal Cuoq and Damien Doligez},
  title = {Hashconsing in an Incrementally Garbage-Collected System: A Story of Weak Pointers and Hashconsing in {OCaml} 3.10.2},
  booktitle = {2008 {ACM} {SIGPLAN} Workshop on {ML}},
  pages = {13--22},
  urlpublisher = {http://doi.acm.org/10.1145/1411304.1411308},
  publisher = {ACM Press},
  year = 2008,
  month = sep,
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2008-Doligez-et-al-focal,
  author = {Philippe Ayrault and Matthieu Carlier and David Delahaye
            and Catherine Dubois and Damien Doligez and Lionel Habib
            and Th\'er\`ese Hardin and Mathieu Jaume and Charles Morisset
            and Fran\c{c}ois Pessaux and Renaud Rioboo and Pierre Weis},
  title = {Trusted Software within {Focal}},
  booktitle = {Computer \& Electronics Security Applications Rendez-vous
               (C\&SAR 2008)},
  year = 2008,
  editor = {Pascal Chour and Yves Correc and Olivier Heen and Ludovic M\'e},
  pages = {142--158},
  month = dec,
  url = {http://www-spi.lip6.fr/~jaume/cesar.pdf},
  x-proceedings = {yes},
  x-international-audience = {no}
}
@article{2008-Leroy-Blazy-memory-model,
  author = {Xavier Leroy and Sandrine Blazy},
  title = {Formal verification of a {C}-like memory model
                 and its uses for verifying program transformations},
  journal = {Journal of Automated Reasoning},
  volume = 41,
  number = 1,
  pages = {1--31},
  url = {http://gallium.inria.fr/~xleroy/publi/memory-model-journal.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-008-9099-0},
  year = 2008,
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2008-Leroy-Rideau-Serpette-pmov,
  author = {Laurence Rideau and Bernard Paul Serpette and
                  Xavier Leroy},
  title = {Tilting at windmills with {Coq}:
                 Formal verification of a compilation algorithm
                 for parallel moves},
  journal = {Journal of Automated Reasoning},
  volume = 40,
  number = 4,
  pages = {307--326},
  url = {http://gallium.inria.fr/~xleroy/publi/parallel-move.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-007-9096-8},
  year = 2008,
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@mastersthesis{2008-Pilkiewicz-M2,
  author = {Alexandre Pilkiewicz},
  title = {Towards a foundational type system for complexity analysis},
  type = {{Master's} dissertation (m\'{e}moire de stage de {Master 2})},
  school = {École Polytechnique},
  year = 2008,
  month = nov
}
@inproceedings{2008-Pilkiewicz-ICFP,
  author = {J. Nathan Foster and Alexandre Pilkiewicz
                         and Benjamin C. Pierce},
  title = {Quotient Lenses},
  booktitle = {Proceedings of the 13th International Conference on Functional Programming (ICFP'08)},
  year = 2008,
  month = sep,
  publisher = {ACM Press},
  pages = {383--396},
  url = {http://www.cis.upenn.edu/~jnfoster/papers/quotient-lenses.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1411204.1411257},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@inproceedings{2008-Pottier-antiframe,
  author = {François Pottier},
  title = {Hiding local state in direct style: a higher-order anti-frame rule},
  year = {2008},
  month = jun,
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-antiframe-2008.pdf},
  urlpublisher = {http://dx.doi.org/10.1109/LICS.2008.16},
  booktitle = {Proceedings of the 23rd Annual {IEEE} Symposium on Logic In
                 Computer Science (LICS'08)},
  publisher = {IEEE Computer Society Press},
  pages = {331-340},
  raweb = {refer},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2008-Regis-Gianas-Pottier,
  author = {Yann {Régis-Gianas} and François Pottier},
  title = {A {Hoare} logic for
                         call-by-value functional programs},
  booktitle = {Mathematics of Program Construction,
                         9th International Conference, MPC 2008},
  year = {2008},
  month = jul,
  pages = {305--335},
  series = {Lecture Notes in Computer Science},
  volume = 5133,
  publisher = {Springer},
  url = {http://gallium.inria.fr/~fpottier/publis/pottier-regis-gianas-hoarefp.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-540-70594-9_17},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2008-Tristan-Leroy-POPL,
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  title = {Formal verification of translation validators:
                 A case study on instruction scheduling optimizations},
  booktitle = {Proceedings of the 35th {ACM} Symposium on Principles of
                  Programming Languages (POPL'08)},
  pages = {17--27},
  publisher = {ACM Press},
  year = 2008,
  month = jan,
  url = {http://gallium.inria.fr/~xleroy/publi/validation-scheduling.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1328897.1328444},
  abstract = {Translation validation consists of transforming a program and a
posteriori validating it in order to detect a modification of its
semantics. This approach can be used in a verified compiler, provided
that validation is formally proved to be correct. We present two such
validators and their Coq proofs of correctness.  The validators are
designed for two instruction scheduling optimizations: list
scheduling and trace scheduling.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2008-Yakobowski-JFLA,
  author = {Boris Yakobowski},
  title = {Le caractère ``backquote'' à la rescousse --
     {F}actorisation et réutilisation de code grâce aux variants polymorphes},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'08)},
  year = 2008,
  address = {Étretat, France},
  month = jan,
  pages = {63--78},
  url = {http://gallium.inria.fr/~yakobows/jfla08.html},
  urlpublisher = {http://hal.inria.fr/inria-00202817/},
  publisher = {INRIA},
  x-international-audience = {no},
  x-proceedings = {yes}
}
@inproceedings{2008-Yakobowski-Remy-icfp,
  author = {Boris Yakobowski and Didier Rémy},
  title = {Graphic Type Constraints and Efficient Type Inference:
                   from {ML} to {MLF}},
  booktitle = {Proceedings of the 13th International Conference on Functional Programming (ICFP'08)},
  year = 2008,
  month = sep,
  publisher = {ACM Press},
  pages = {63--74},
  url = {http://gallium.inria.fr/~remy/mlf/mlf-type-inference.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1411204.1411216},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@phdthesis{2008-Yakobowski-these,
  author = {Boris Yakobowski},
  title = {Graphical types and constraints: second-order polymorphism and
  inference},
  school = {University Paris Diderot (Paris 7)},
  year = {2008},
  url = {http://tel.archives-ouvertes.fr/tel-00357708/},
  month = dec
}
@inproceedings{2008-Doligez-et-al-tla,
  author = {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport
            and Stephan Merz},
  title = {A {TLA}+ Proof System},
  booktitle = {Proceedings of the {LPAR} Workshops: Knowledge Exchange:
               Automated Provers and Proof Assistants, and The 7th
               International Workshop on the Implementation of Logics},
  year = 2008,
  editor = {Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B.
            and Schulz, S.},
  month = nov,
  place = {Doha, Qatar},
  series = {{CEUR} Workshop Proceedings},
  volume = {418},
  publisher = {CEUR-WS.org},
  url = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-418/paper2.pdf},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-pays = {US}
}
@article{2009-Blazy-Leroy-Clight,
  author = {Sandrine Blazy and Xavier Leroy},
  title = {Mechanized semantics for the {Clight}
                         subset of the {C} language},
  year = 2009,
  journal = {Journal of Automated Reasoning},
  url = {http://gallium.inria.fr/~xleroy/publi/Clight.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3},
  volume = 43,
  number = 3,
  pages = {263-288},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@inproceedings{2009-Blazy-Robillard,
  author = {Sandrine Blazy and Benoît Robillard},
  title = {Live-range Unsplitting for Faster Optimal Coalescing},
  booktitle = {Proceedings of the ACM SIGPLAN/SIGBED 2009
                         conference on Languages,
                         Compilers, and Tools for Embedded Systems
                         (LCTES 2009)},
  pages = {70--79},
  publisher = {ACM Press},
  year = 2009,
  url = {http://www.ensiie.fr/~blazy/LCTES09.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1542452.1542462},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@phdthesis{2009-Dargaye-these,
  author = {Zaynah Dargaye},
  title = {Vérification formelle d'un compilateur optimisant pour langages fonctionnels},
  school = {University Paris Diderot (Paris 7)},
  month = jul,
  year = 2009,
  url = {http://tel.archives-ouvertes.fr/tel-00452440/},
  note = {English title: Formal verification of an optimizing compiler for functional languages}
}
@article{2009-Dargaye-Leroy-uncurrying,
  author = {Zaynah Dargaye and Xavier Leroy},
  title = {A verified framework for higher-order uncurrying optimizations},
  journal = {Higher-Order and Symbolic Computation},
  url = {http://gallium.inria.fr/~xleroy/publi/higher-order-uncurrying.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10990-010-9050-z},
  year = 2009,
  volume = 22,
  number = 3,
  pages = {199--231},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@inproceedings{2009-DiCosmo-ESEM,
  author = {Pietro Abate and
               Jaap Boender and
               Roberto {Di Cosmo} and
               Stefano Zacchiroli},
  title = {Strong Dependencies between Software Components},
  booktitle = {3rd International Symposium on Empirical Sofware Engineering and Measurement, ESEM 2009},
  year = {2009},
  month = oct,
  pages = {89-99},
  publisher = {IEEE Computer Society Press},
  urlpublisher = {http://dx.doi.org/10.1109/ESEM.2009.5316017},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@article{2009-DiCosmo-LaRecherche,
  author = {Roberto {Di Cosmo}},
  title = {La science du logiciel libre},
  journal = {La Recherche},
  note = {Les cahiers de l'INRIA},
  year = {2009},
  month = dec,
  volume = 436,
  url = {http://www.lescahiersinria.com/sites/default/files/inria-n436-dec09.pdf},
  x-international-audience = {no},
  x-editorial-board = {no},
  x-scientific-popularization = {yes},
  refereed = {no}
}
@article{2009-DiCosmo-ScienceEtAvenir,
  author = {Roberto {Di Cosmo}},
  title = {Offrons aux jeunes les cl\'es du pouvoir et de la libert\'e},
  journal = {Science et Avenir},
  year = {2009},
  month = sep,
  volume = 751,
  pages = {42-45},
  x-international-audience = {no},
  x-editorial-board = {no},
  x-scientific-popularization = {yes},
  refereed = {no},
  urlpublisher = {http://sciencesetavenirmensuel.nouvelobs.com/hebdo/sea/p751/articles/a407123-.html}
}
@inproceedings{2009-Doligez-etal-popl,
  author = {Julien Brunel and Damien Doligez and
             Ren\'{e} Rydhof Hansen and Julia L. Lawall and
             Gilles Muller},
  title = {A Foundation for Flow-Based Program Matching 
           Using Temporal Logic and Model Checking},
  booktitle = {Proceedings of the 36th {ACM} Symposium on Principles of
               Programming Languages (POPL'09)},
  publisher = {ACM Press},
  year = 2009,
  month = jan,
  urlpublisher = {http://doi.acm.org/10.1145/1480881.1480897},
  pages = {114-126},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {DK}
}
@article{2009-LeBotlan-Remy-recasting-mlf,
  author = {Le Botlan, Didier and R{\'{e}}my, Didier},
  title = {Recasting {MLF}},
  journal = {Information and Computation},
  volume = {207},
  number = {6},
  pages = {726--785},
  year = {2009},
  issn = {0890-5401},
  doi = {10.1016/j.ic.2008.12.006},
  urlpublisher = {http://dx.doi.org/10.1016/j.ic.2008.12.006},
  url = {http://gallium.inria.fr/~remy/mlf/recasting-mlf-RR.pdf},
  abstract = {The language MLF is a proposal for a new type system that
  supersedes both ML and System F, allows for efficient, predictable, and
  complete type inference for partially annotated terms.  In this work, we
  revisit the definition of MLF, following a more progressive approach and
  focusing on the design-space and expressiveness.  We introduce a
  Curry-style version iMLF of MLF and provide an interpretation of iMLF
  types as instantiation-closed sets of System-F types, from which we derive
  the definition of type instance in iMLF.  We give equivalent syntactic
  definition of the type-instance, presented as a set of inference rules.
  We also show an encoding of iMLF into the closure of Curry-style System F
  by let-expansion.  We derive the Church-style version eMLF by refining
  types of iMLF so as to distinguish between given and inferred
  polymorphism.  We show an embedding of ML in eMLF and a straightforward
  encoding of System F into eMLF.},
  raweb = {refer},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2009-Leroy-Grall,
  author = {Xavier Leroy and Hervé Grall},
  title = {Coinductive big-step operational semantics},
  journal = {Information and Computation},
  volume = 207,
  number = 2,
  pages = {284--304},
  year = 2009,
  url = {http://gallium.inria.fr/~xleroy/publi/coindsem-journal.pdf},
  urlpublisher = {http://dx.doi.org/10.1016/j.ic.2007.12.004},
  abstract = {Using a call-by-value functional language as an example, this article
illustrates the use of coinductive definitions and proofs in big-step
operational semantics, enabling it to describe diverging evaluations
in addition to terminating evaluations.  We formalize the connections
between the coinductive big-step semantics and the standard small-step
semantics, proving that both semantics are equivalent.  We then study
the use of coinductive big-step semantics in proofs of type soundness
and proofs of semantic preservation for compilers.
A methodological originality of this paper is that all results
have been proved using the Coq proof assistant.  We explain the
proof-theoretic presentation of coinductive definitions and proofs
offered by Coq, and show that it facilitates the discovery and the
presentation of the results.},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2009-Leroy-Compcert-backend,
  author = {Xavier Leroy},
  title = {A formally verified compiler back-end},
  journal = {Journal of Automated Reasoning},
  volume = 43,
  number = 4,
  pages = {363--446},
  year = 2009,
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
  raweb = {refer},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2009-Leroy-Compcert-CACM,
  author = {Xavier Leroy},
  title = {Formal verification of a realistic compiler},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.},
  raweb = {refer},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2009-Leroy-Hirschowitz-Wells,
  author = {Tom Hirschowitz and Xavier Leroy and J. B. Wells},
  title = {Compilation of extended recursion
                         in call-by-value functional languages},
  journal = {Higher-Order and Symbolic Computation},
  volume = 22,
  number = 1,
  pages = {3--66},
  year = 2009,
  url = {http://gallium.inria.fr/~xleroy/publi/letrec-cbv.pdf},
  urlpublisher = { http://dx.doi.org/10.1007/s10990-009-9042-z},
  abstract = {This paper formalizes and proves correct a compilation scheme for
 mutually-recursive definitions in call-by-value functional
 languages.  This scheme supports a wider range of recursive
 definitions than previous methods.  We formalize our technique as a
 translation scheme to a lambda-calculus featuring in-place update of
 memory blocks, and prove the translation to be correct.},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {GB}
}
@inproceedings{2009-Montagu-Remy-fzip,
  author = {Beno{\^\i}t Montagu and Didier R{\'e}my},
  title = {Modeling Abstract Types in Modules with Open Existential Types},
  booktitle = {Proceedings of the 36th {ACM} Symposium on Principles of
               Programming Languages (POPL'09)},
  publisher = {ACM Press},
  year = 2009,
  month = jan,
  x-international-audience = {yes},
  x-proceedings = {yes},
  pages = {354-365},
  url = {http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1480881.1480926}
}
@phdthesis{2009-Tristan-these,
  author = {Jean-Baptiste Tristan},
  title = {Formal verification of translation validators},
  school = {University Paris Diderot (Paris 7)},
  month = nov,
  year = 2009,
  url = {http://tel.archives-ouvertes.fr/tel-00437582/}
}
@inproceedings{2009-Tristan-Leroy-LCM,
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  title = {Verified Validation of {Lazy} {Code} {Motion}},
  booktitle = {Proceedings of the 2009 ACM SIGPLAN Conference on
                         Programming Language Design and Implementation
                         (PLDI'09)},
  year = 2009,
  pages = {316--326},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~xleroy/publi/validation-LCM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1542476.1542512},
  abstract = { Translation validation establishes a posteriori the
  correctness of a run of a compilation pass or other program
  transformation.  In this paper, we develop an efficient translation
  validation algorithm for the Lazy Code Motion (LCM) optimization.
  LCM is an interesting challenge for validation because it is a
  global optimization that moves code across loops.  Consequently,
  care must be taken not to move computations that may fail before
  loops that may not terminate.  Our validator includes a specific
  check for anticipability to rule out such incorrect moves.
  We present a mechanically-checked proof of correctness of the
  validation algorithm, using the Coq proof assistant.
  Combining our validator with an unverified implementation of LCM, we
  obtain a LCM pass that is provably semantics-preserving and 
  was integrated in the CompCert formally verified compiler.},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@mastersthesis{2009-Herms-master,
  author = {Paolo Herms},
  title = {{P}artial {T}ype {I}nference with {H}igher-{O}rder {T}ypes},
  school = {University of Pisa},
  year = {2009},
  type = {Master's thesis},
  month = jul,
  url = {http://gallium.inria.fr/~remy/mlf/herms@master2009.pdf}
}
@inproceedings{2010-Pottier-hidden-state,
  author = {Jan Schwinghammer and Hongseok Yang and Lars Birkedal
                 and François Pottier and Bernhard Reus},
  title = {A Semantic Foundation for Hidden State},
  booktitle = {Foundations of Software Science and Computation Structures
                  (FoSSaCS 2010)},
  year = {2010},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 6014,
  pages = {2--17},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url = {http://gallium.inria.fr/~fpottier/publis/sfhs.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-12032-9_2},
  abstract = {We present the first complete soundness proof of the
                 anti-frame rule, a recently proposed proof rule for
                 capturing information hiding in the presence of
                 higher-order store. Our proof involves solving a
                 non-trivial recursive domain equation. It helps
                 identify some of the key ingredients for soundness, and
                 thereby suggests how one might hope to relax some of
                 the restrictions imposed by the rule.},
  x-pays = {DK,DE,GB}
}
@inproceedings{2010-Chargueraud-fixpoint,
  author = {Arthur Charguéraud},
  title = {The Optimal Fixed Point Combinator},
  booktitle = {Interactive Theorem Proving (ITP 2010)},
  publisher = {Springer},
  volume = 6172,
  series = {Lecture Notes in Computer Science},
  pages = {195-210},
  year = 2010,
  url = {http://www.chargueraud.org/arthur/research/2010/fix/},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-14052-5_15},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2010-Chargueraud-cfml,
  author = {Arthur Chargu{\'e}raud},
  title = {Program Verification Through Characteristic Formulae},
  booktitle = {Proceedings of the 15th International Conference on Functional Programming (ICFP 2010)},
  year = {2010},
  publisher = {ACM Press},
  pages = {321--332},
  urlpublisher = {http://doi.acm.org/10.1145/1863543.1863590},
  url = {http://arthur.chargueraud.org/research/2010/cfml/},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@phdthesis{2010-Chargueraud-these,
  author = {Arthur Chargu{\'e}raud},
  title = {Characteristic Formulae for Mechanized Program Verification},
  school = {Universit{\'e} Paris Diderot (Paris 7)},
  year = {2010},
  month = dec,
  url = {http://arthur.chargueraud.org/research/2010/thesis/}
}
@inproceedings{2010-Cretin-lenses,
  title = {Matching Lenses: Alignment and View Update},
  author = {Davi M. J. Barbosa and Julien Cretin and Nate Foster and Michael Greenberg and Benjamin C. Pierce},
  booktitle = {Proceedings of the 15th International Conference on Functional Programming (ICFP 2010)},
  year = {2010},
  publisher = {ACM Press},
  pages = {193--204},
  urlpublisher = {http://doi.acm.org/10.1145/1863543.1863572},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@mastersthesis{2010-Cretin-master,
  author = {Julien Cretin},
  title = {A generalization of {F}-eta with abstraction over retyping functions},
  school = {{\'E}cole {P}olytechnique},
  year = {2010},
  type = {Master's thesis},
  month = dec,
  url = {http://gallium.inria.fr/~jcretin/papers/master_thesis.pdf}
}
@article{2010-Dicosmo-IsosIntersection,
  author = {Mariangiola Dezani-Ciancaglini and
               Roberto {Di Cosmo} and
               Elio Giovannetti and
               Makoto Tatsuta},
  title = {On isomorphisms of intersection types},
  journal = {ACM Transactions on Computational Logic},
  volume = {11},
  number = {4},
  pages = {Article No. 25},
  year = {2010},
  urlpublisher = {http://doi.acm.org/10.1145/1805950.1805955},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-pays = {IT,JP}
}
@inproceedings{2010-Dicosmo-ISEC,
  author = {Di Cosmo, Roberto and Boender, Jaap},
  title = {Using strong conflicts to detect quality issues in component-based complex systems},
  booktitle = {ISEC '10: Proceedings of the 3rd India software engineering conference},
  year = {2010},
  pages = {163--172},
  location = {Mysore, India},
  urlpublisher = {http://doi.acm.org/10.1145/1730874.1730905},
  publisher = {ACM Press},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2010-Dicosmo-SPLC,
  author = {Roberto {Di Cosmo} and
               Stefano Zacchiroli},
  title = {Feature Diagrams as Package Dependencies},
  booktitle = {Software Product Lines: Going Beyond - 14th International
               Conference, SPLC 2010},
  year = {2010},
  pages = {476-480},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6287},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-15579-6_40},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2010-Doligez-TLA+,
  author = {Kaustuv Chaudhuri and Damien Doligez
            and Leslie Lamport and Stephan Merz},
  title = {Verifying Safety Properties With the {TLA+} Proof System},
  booktitle = {Automated Reasoning,
               5th International Joint Conference, IJCAR 2010},
  pages = {142--148},
  volume = {6173},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = 2010,
  raweb = {refer},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-14203-1_12},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@incollection{2010-Leroy-Marktoberdorf,
  author = {Xavier Leroy},
  title = {Mechanized semantics},
  booktitle = {Logics and languages for reliability and security},
  editors = {J. Esparza and B. Spanfelner and O. Grumberg},
  series = {NATO Science for Peace and Security Series D: Information and Communication Security},
  volume = 25,
  pages = {195--224},
  publisher = {IOS Press},
  year = {2010},
  url = {http://gallium.inria.fr/~xleroy/courses/Marktoberdorf-2009/notes.pdf},
  urlpublisher = {http://dx.doi.org/10.3233/978-1-60750-100-8-195}
}
@article{2010-Leroy-LaRecherche,
  author = {Xavier Leroy},
  title = {Comment faire confiance à un compilateur?},
  journal = {La Recherche},
  note = {Les cahiers de l'INRIA},
  year = {2010},
  month = apr,
  volume = 440,
  url = {http://gallium.inria.fr/~xleroy/publi/cahiers-inria-2010.pdf},
  urlpublisher = {http://www.lescahiersinria.com/sites/default/files/inria-n440-avril10.pdf},
  x-international-audience = {no},
  x-editorial-board = {no},
  x-scientific-popularization = {yes},
  refereed = {no}
}
@inproceedings{2010-Montagu-GDR-GPL,
  author = {Benoît Montagu and Didier Rémy},
  title = {Types abstraits et types existentiels ouverts},
  booktitle = {Actes des deuxièmes journées nationales du Groupement
                  De Recherche CNRS du Génie de la Programmation et du
                  Logiciel},
  year = 2010,
  pages = {147--148},
  editor = {Éric Cariou and Laurence Duchien and Yves Ledru},
  address = {Université de Pau},
  month = mar,
  urlpublisher = {http://gdr-gpl.imag.fr/},
  x-international-audience = {no},
  x-proceedings = {yes}
}
@inproceedings{2010-Montagu-WMM,
  author = {Benoît Montagu},
  title = {Experience report: {Mechanizing} {Core} {F-zip} using the locally nameless approach (extended abstract)},
  booktitle = {5th ACM SIGPLAN Workshop on Mechanizing Metatheory},
  urlpublisher = {http://www.cis.upenn.edu/~bcpierce/wmm/wmm10/montagu.pdf},
  year = 2010,
  x-international-audience = {yes},
  x-proceedings = {no}
}
@phdthesis{2010-Montagu-these,
  author = {Benoît Montagu},
  title = {Programmer avec des modules de première classe dans
                  un langage noyau pourvu de sous-typage, sortes
                  singletons et types existentiels ouverts},
  school = {École Polytechnique},
  year = 2010,
  url = {http://tel.archives-ouvertes.fr/tel-00550331/},
  month = dec,
  raweb = {foot},
  note = {English title: Programming with first-class modules
                  in a core language with subtyping, singleton kinds
                  and open existential types}
}
@inproceedings{2010-Pouillard-Pottier-fresh-look,
  author = {Nicolas Pouillard and François Pottier},
  title = {A fresh look at programming with names and binders},
  booktitle = {Proceedings of the 15th International Conference on Functional Programming (ICFP 2010)},
  year = {2010},
  publisher = {ACM Press},
  pages = {217--228},
  urlpublisher = {http://doi.acm.org/10.1145/1863543.1863575},
  url = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-fresh-look.pdf},
  longpdf = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-fresh-look-x.pdf},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2010-Remy-Yakobowski-xMLF,
  author = {Didier R\'emy and Boris Yakobowski},
  title = {A {Church}-Style Intermediate Language for {MLF}},
  booktitle = {Functional and Logic Programming, 10th International Symposium,  FLOPS 2010},
  year = 2010,
  pages = {24--39},
  volume = 6009,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url = {http://gallium.inria.fr/~remy/mlf/xmlf.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-12251-4_4},
  abstract = {MLF is a type system that seamlessly merges ML-style implicit but
second-class polymorphism with System F explicit first-class
polymorphism. We present xMLF, a Church-style version of MLF with full
type information that can easily be maintained during reduction. All
parameters of functions are explicitly typed and both type abstraction
and type instantiation are explicit. However, type instantiation in xMLF
is more general than type application in System F.  We equip xMLF with a
small-step reduction semantics that allows  reduction in any context and
show that this relation is confluent and type preserving.  We also show
that both subject reduction and progress hold for weak-reduction
strategies, including call-by-value with the value-restriction. We
exhibit a type preserving encoding of MLF into xMLF,  which ensures type
soundness for the most general version of MLF. We observe that  xMLF is
a calculus of retyping functions at the type level.}
}
@inproceedings{2010-Rideau-Leroy-regalloc,
  author = {Silvain Rideau and Xavier Leroy},
  title = {Validating register allocation and spilling},
  booktitle = {Compiler Construction (CC 2010)},
  year = 2010,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 6011,
  pages = {224--243},
  url = {http://gallium.inria.fr/~xleroy/publi/validation-regalloc.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@mastersthesis{2010-Scherer-master,
  author = {Gabriel Scherer},
  title = {{E}xtending {MLF} with Higher-Order Types},
  school = {{\'E}cole {N}ormale {S}up{\'e}rieure, {P}aris},
  year = {2010},
  type = {Master's thesis},
  month = aug,
  url = {http://gallium.inria.fr/~remy/mlf/scherer@master2010:mlfomega.pdf}
}
@inproceedings{2010-Tristan-Leroy-softpipe,
  author = {Jean-Baptiste Tristan and Xavier Leroy},
  title = {A simple, verified validator for software pipelining},
  booktitle = {Proceedings of the 37th {ACM} Symposium on Principles of
               Programming Languages (POPL'10)},
  pages = {83--92},
  publisher = {ACM Press},
  year = 2010,
  url = {http://gallium.inria.fr/~xleroy/publi/validation-softpipe.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1706299.1706311},
  x-international-audience = {yes},
  x-proceedings = {yes},
  raweb = {refer}
}
@inproceedings{2010-Xu-Goessler-Girault,
  author = {Dana N. Xu and Gregor G{\"o}ssler and Alain Girault},
  title = {Probabilistic Contracts for Component-based Design},
  booktitle = {Automated Technology for Verification
     and Analysis (ATVA 2010)},
  year = 2010,
  url = {http://gallium.inria.fr/~naxu/research/atva10.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-15643-4_24},
  pages = {325--340},
  volume = {6252},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@techreport{2010-Xu-Geossler-Girault-INRIA,
  hal_id = {inria-00507785},
  url = {http://hal.inria.fr/inria-00507785/en/},
  title = { {P}robabilistic {C}ontracts for {C}omponent-based {D}esign},
  author = {{X}u, {D}ana N. and {G}{\"o}ssler, {G}regor and {G}irault, {A}lain},
  abstract = {{W}e define a probabilistic contract framework for describing and analysing component-based embedded systems, based on the theory of {I}nteractive {M}arkov {C}hains ({IMC}). {A} contract specifies the assumptions a component makes on its context and the guarantees it provides. {P}robabilistic transitions allow for uncertainty in the component behavior, e.g., to model observed black-box behavior (internal choice) or reliability. {A}n interaction model specifies how components interact. {W}e provide the ingredients for a component-based design flow, including (1) contract satisfaction and refinement, (2) parallel composition of contracts over disjoint, interacting components, and (3) conjunction of contracts describing different requirements over the same component. {C}ompositional design is enabled by congruence of refinement.},
  language = {{A}nglais},
  affiliation = {{GALLIUM} - {INRIA} {R}ocquencourt - {INRIA} - {POP} {ART} - {INRIA} {R}h{\^o}ne-{A}lpes / {LIG} {L}aboratoire d'{I}nformatique de {G}renoble - {INRIA} - {I}nstitut {N}ational {P}olytechnique de {G}renoble - {INPG} - {U}niversit{\'e} {J}oseph {F}ourier - {G}renoble {I} - {U}niversit{\'e} {P}ierre {M}end{\`e}s-{F}rance - {G}renoble {II} - {CNRS} : {UMR}5217 },
  type = {Research Report},
  institution = {INRIA},
  number = {{RR}-7328},
  day = {31},
  month = jul,
  year = {2010}
}
@techreport{2011-Cretin-Remy,
  author = {Cretin, Julien and R{\'e}my, Didier},
  title = {{O}n the {P}ower of {C}oercion {A}bstraction},
  type = {Research Report},
  pages = {59},
  year = {2011},
  month = dec,
  institution = {INRIA},
  number = {RR-7587},
  url = {http://hal.inria.fr/inria-00582570/en/},
  pdf = {http://hal.inria.fr/inria-00582570/PDF/RR-7587.pdf}
}
@mastersthesis{2011-Dailler-master,
  author = {Sylvain Dailler},
  title = {Preuve mécanisée de correction et de complexité pour un
           algorithme impératif},
  year = {2011},
  month = aug,
  type = {Master's thesis},
  school = {University Paris Diderot},
  note = {Report on Master's internship}
}
@inproceedings{2011-DiCosmo-ATZ,
  author = {Pietro Abate and
               Roberto {Di Cosmo} and
               Ralf Treinen and
               Stefano Zacchiroli},
  title = {{MPM}: a modular package manager},
  pages = {179--188},
  urlpublisher = {http://doi.acm.org/10.1145/2000229.2000255},
  booktitle = {Proceedings of the 14th International ACM Sigsoft Symposium
               on Component Based Software Engineering, CBSE 2011},
  publisher = {ACM Press},
  x-international-audience = {yes},
  x-proceedings = {yes},
  year = {2011}
}
@inproceedings{2011-DiCosmo-Abate,
  author = {Pietro Abate and
               Roberto {Di Cosmo}},
  title = {Predicting upgrade failures using dependency analysis},
  pages = {145--150},
  url = {http://dx.doi.org/10.1109/ICDEW.2011.5767626},
  booktitle = {Workshops Proceedings of the 27th International Conference
               on Data Engineering, ICDE 2011},
  publisher = {IEEE Computer Society Press},
  x-international-audience = {yes},
  x-proceedings = {yes},
  year = {2011}
}
@inproceedings{2011-DiCosmo-LM,
  author = {Roberto {Di Cosmo} and
               Olivier Lhomme and
               Claude Michel},
  title = {Aligning component upgrades},
  pages = {1--11},
  urlpublisher = {http://dx.doi.org/10.4204/EPTCS.65.1},
  booktitle = {Proceedings Second Workshop on Logics for Component Configuration},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {65},
  x-international-audience = {yes},
  x-proceedings = {yes},
  year = {2011}
}
@inproceedings{2011-DiCosmo-Vouillon,
  author = {Roberto {Di Cosmo} and
               J{\'e}r{\^o}me Vouillon},
  title = {On software component co-installability},
  pages = {256--266},
  urlpublisher = {http://doi.acm.org/10.1145/2025113.2025149},
  booktitle = {19th ACM SIGSOFT Symposium on the Foundations
               of Software Engineering (FSE-19) and ESEC'11: 13rd European
               Software Engineering Conference (ESEC-13)},
  publisher = {ACM Press},
  x-international-audience = {yes},
  x-proceedings = {yes},
  year = {2011}
}
@article{2011-DiCosmo-RPPZ11,
  author = {Roberto {Di Cosmo} and
               Davide {Di Ruscio} and
               Patrizio Pelliccione and
               Alfonso Pierantonio and
               Stefano Zacchiroli},
  title = {Supporting software evolution in component-based {FOSS} systems},
  journal = {Science of Computer Programming},
  volume = {76},
  number = {12},
  year = {2011},
  pages = {1144--1160},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {IT},
  urlpublisher = {http://dx.doi.org/10.1016/j.scico.2010.11.001}
}
@inproceedings{2011-Doligez-Cuoq-Signoles,
  author = {Pascal Cuoq and Damien Doligez and Julien Signoles},
  title = {Lightweight typed customizable unmarshaling},
  booktitle = {ACM SIGPLAN Workshop on ML},
  year = 2011,
  publisher = {ACM Press},
  x-international-audience = {yes},
  x-proceedings = {no}
}
@mastersthesis{2011-Jourdan-master,
  author = {Jacques-Henri Jourdan},
  title = {Validation d'analyseurs syntaxiques {LR(1)}:
       Vers un analyseur syntaxique certifié pour le compilateur {CompCert}},
  year = {2011},
  month = aug,
  type = {Master's thesis},
  school = {ENS Paris},
  note = {Report on Master's internship}
}
@inproceedings{2011-Leroy-FFPS,
  author = {Ricardo {Bedin França} and Denis Favre-Felix and Xavier Leroy
            and Marc Pantel and Jean Souyris},
  title = {Towards Formally Verified Optimizing Compilation in Flight Control Software},
  booktitle = {Bringing Theory to Practice: Predictability and Performance in Embedded Systems (PPES 2011)},
  pages = {59--68},
  series = {OpenAccess Series in Informatics (OASIcs)},
  volume = 18,
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  year = {2011},
  url = {http://hal.archives-ouvertes.fr/inria-00551370/},
  urlpublisher = {http://dx.doi.org/10.4230/OASIcs.PPES.2011.59},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2011-Leroy-POPL,
  author = {Xavier Leroy},
  title = {Verified squared: does critical software deserve verified tools?},
  note = {Extended abstract of invited talk},
  booktitle = {Proceedings of the 38th {ACM} Symposium on Principles of
               Programming Languages (POPL'11)},
  pages = {1--2},
  year = 2011,
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~xleroy/publi/popl11-invited-talk.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/1926385.1926387},
  refereed = {no},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes}
}
@inproceedings{2011-Leroy-CGO,
  author = {Xavier Leroy},
  title = {Formally verifying a compiler: Why? How? How far?},
  note = {Abstract of invited talk},
  booktitle = {Proceedings of CGO 2011, The 9th International Symposium
               on Code Generation and Optimization},
  year = {2011},
  urlpublisher = {http://dx.doi.org/10.1109/CGO.2011.5764668},
  publisher = {IEEE},
  refereed = {no},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes}
}
@article{2011-Leroy-CACM-TP,
  author = {Xavier Leroy},
  title = {Safety first! (technical perspective)},
  journal = {Communications of the ACM},
  volume = {54},
  number = {12},
  pages = {122--122},
  month = dec,
  year = {2011},
  urlpublisher = {http://doi.acm.org/10.1145/2043174.2043196},
  publisher = {ACM Press},
  refereed = {no},
  x-international-audience = {yes},
  x-editorial-board = {no}
}
@inproceedings{2011-Pottier-fork,
  author = {François Pottier},
  title = {A typed store-passing translation for general references},
  year = {2011},
  booktitle = {Proceedings of the 38th {ACM} Symposium on Principles of
               Programming Languages (POPL'11)},
  publisher = {ACM Press},
  pages = {147--158},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork.pdf},
  longpdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork-x.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/1926385.1926403},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2011-Pilkiewicz-Pottier-monotonicity,
  author = {Alexandre Pilkiewicz and François Pottier},
  title = {The essence of monotonic state},
  booktitle = {6th Workshop on Types in Language Design and Implementation (TLDI 2011)},
  year = {2011},
  pages = {73--86},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~fpottier/publis/pilkiewicz-pottier-monotonicity.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/1929553.1929565},
  x-international-audience = {yes},
  x-proceedings = {yes},
  abstract = {We extend a static type-and-capability system with new
                 mechanisms for expressing the promise that a certain
                 abstract value evolves monotonically with time; for
                 enforcing this promise; and for taking advantage of
                 this promise to establish non-trivial properties of
                 programs. These mechanisms are independent of the
                 treatment of mutable state, but combine with it to
                 offer a flexible account of ``monotonic state''.}
}
@inproceedings{2011-Pouillard-ICFP,
  author = {Nicolas Pouillard},
  title = {Nameless, Painless},
  booktitle = {Proceedings of the 16th International Conference on Functional Programming (ICFP 2011)},
  pages = {320--332},
  year = 2011,
  publisher = {ACM Press},
  url = {http://nicolaspouillard.fr/publis/nameless-painless.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/2034773.2034817},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2011-Ramananandro-DosReis-Leroy,
  author = {Tahina Ramananandro and Gabriel {Dos Reis} and Xavier Leroy},
  title = {Formal verification of object layout for {C++} multiple inheritance},
  year = 2011,
  booktitle = {Proceedings of the 38th {ACM} Symposium on Principles of
               Programming Languages (POPL'11)},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~xleroy/publi/cpp-object-layout.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/1926385.1926395},
  pages = {67--80},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@mastersthesis{2011-Robert-master,
  author = {Valentin Robert},
  title = {Conception, mise en oeuvre et vérification d'une analyse d'alias pour {CompCert}, un compilateur {C} formellement vérifié},
  year = {2011},
  month = dec,
  type = {Master's thesis},
  school = {ENSEIRB},
  note = {Report on Master's internship}
}
@techreport{2011-Xu,
  author = {Xu, Dana N.},
  title = {Hybrid Contract Checking via Symbolic Simplification},
  type = {Research Report},
  pages = {69},
  year = {2011},
  month = nov,
  institution = {INRIA},
  number = {RR-7794},
  url = {http://hal.inria.fr/hal-00644156/en}
}
@inproceedings{2012-Braibant-Chlipala-CoqW,
  author = {Thomas Braibant and Adam Chlipala},
  title = {Formal verification of hardware synthesis},
  booktitle = {The Coq Workshop},
  year = 2012,
  url = {http://gallium.inria.fr/~braibant/data/braibant-talk-coq-workshop-2012.pdf},
  x-international-audience = {yes},
  x-proceedings = {no},
  x-pays = {US}
}
@inproceedings{2012-Cretin-Remy,
  author = {Julien Cretin and Didier Rémy},
  title = {On the Power of Coercion Abstraction},
  booktitle = {Proceedings of the 39th {ACM} Symposium on Principles of
               Programming Languages (POPL'12)},
  pages = {361--372},
  year = 2012,
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~jcretin/papers/conf.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/2103656.2103699},
  urlhal = {http://hal.inria.fr/hal-00650910},
  raweb = {refer},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2012-Doligez-etal-tla,
  author = {Denis Cousineau and
               Damien Doligez and
               Leslie Lamport and
               Stephan Merz and
               Daniel Ricketts and
               Hern{\'a}n Vanzetto},
  title = {{TLA} + Proofs},
  editor = {Dimitra Giannakopoulou and
               Dominique M{\'e}ry},
  booktitle = {FM 2012: Formal Methods - 18th International Symposium},
  year = {2012},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7436},
  pages = {147-154},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-32759-9_14},
  urlhal = {http://hal.inria.fr/hal-00726631},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-pays = {US},
  raweb = {foot}
}
@inproceedings{2012-Doligez-jaume-rioboo,
  author = {Doligez, Damien and Jaume, Mathieu and Rioboo, Renaud},
  title = {Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the {FoCaLiZe} environment},
  booktitle = {Proceedings of the 7th Workshop on Programming Languages and Analysis for Security (PLAS'12)},
  year = {2012},
  isbn = {978-1-4503-1441-1},
  location = {Beijing, China},
  pages = {9:1--9:12},
  articleno = {9},
  urlpublisher = {http://doi.acm.org/10.1145/2336717.2336726},
  publisher = {ACM Press},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2012-Jourdan-Pottier-Leroy,
  author = {Jacques-Henri Jourdan and François Pottier and Xavier Leroy},
  title = {Validating {LR(1)} Parsers},
  booktitle = {Programming Languages and Systems -- 21st European Symposium on Programming, ESOP 2012},
  editor = {H. Seidl},
  url = {http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
  year = 2012,
  pages = {397--416},
  series = {Lecture Notes in Computer Science},
  volume = 7211,
  publisher = {Springer},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2012-Leroy-BFBFFPS,
  author = {Ricardo {Bedin França} and Sandrine Blazy and Denis Favre-Felix
            and Xavier Leroy and Marc Pantel and Jean Souyris},
  title = {Formally verified optimizing compilation in {ACG}-based
           flight control software},
  booktitle = {Embedded Real Time Software and Systems (ERTS2 2012)},
  organization = {AAAF, SEE},
  year = 2012,
  url = {http://hal.inria.fr/hal-00653367/},
  x-international-audience = {yes},
  x-proceedings = {no}
}
@article{2012-Leroy-Appel-Dockins-listmachine,
  author = {Andrew W. Appel and Robert Dockins and Xavier Leroy},
  title = {A list-machine benchmark for mechanized metatheory},
  journal = {Journal of Automated Reasoning},
  year = 2012,
  volume = 49,
  number = 3,
  pages = {453--491},
  url = {http://gallium.inria.fr/~xleroy/publi/listmachine-journal.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-011-9226-1},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {US}
}
@techreport{2012-Leroy-Appel-Blazy-Stewart,
  author = {Xavier Leroy and Andrew W. Appel and Sandrine Blazy and Gordon Stewart},
  title = {The {CompCert} Memory Model, Version 2},
  institution = {INRIA},
  type = {Research report},
  number = {RR-7987},
  year = {2012},
  month = jun,
  url = {http://hal.inria.fr/hal-00703441},
  x-pays = {US}
}
@inproceedings{2012-Leroy-APLAS,
  author = {Xavier Leroy},
  title = {Mechanized Semantics for Compiler Verification},
  note = {Abstract of invited talk},
  booktitle = {Programming Languages and Systems, 10th Asian Symposium, APLAS 2012},
  editor = {Ranjit Jhala and Atsushi Igarashi},
  year = {2012},
  pages = {386--388},
  series = {Lecture Notes in Computer Science},
  volume = 7705,
  publisher = {Springer},
  url = {http://gallium.inria.fr/~xleroy/publi/mechanized-semantics-aplas-cpp-2012.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35182-2_27},
  refereed = {no},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-invited-conference = {yes}
}
@phdthesis{2012-Pouillard-phd,
  author = {Nicolas Pouillard},
  title = {Une approche unifiante pour programmer s{\^u}rement avec de la syntaxe du premier ordre contenant des lieurs / Namely, Painless: A unifying approach to safe programming with first-order syntax with binders},
  year = 2012,
  month = jan,
  school = {Université Paris Diderot (Paris 7)},
  url = {http://nicolaspouillard.fr/publis/namely-painless-defense-version.pdf},
  urlhal = {http://tel.archives-ouvertes.fr/tel-00759059}
}
@article{2012-Pouillard-Pottier,
  author = {Nicolas Pouillard and François Pottier},
  title = {A unified treatment of syntax with binders},
  journal = {Journal of Functional Programming},
  volume = {22},
  number = {4--5},
  pages = {614--704},
  year = {2012},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  raweb = {refer},
  url = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-unified.pdf},
  urlpublisher = {http://dx.doi.org/10.1017/S0956796812000251}
}
@inproceedings{2012-Protzenko-Pottier,
  author = {Jonathan Protzenko and Fran\c{c}ois Pottier},
  title = {Programming with permissions: the {Mezzo} language},
  booktitle = {ACM SIGPLAN Workshop on ML},
  url = {http://www.lexifi.com/ml2012/full1.pdf},
  year = 2012,
  x-international-audience = {yes},
  x-proceedings = {no}
}
@phdthesis{2012-Ramananandro-phd,
  author = {Tahina Ramananandro},
  title = {Machine-checked Formal Semantics and Verified Compilation
           for {C++} Objects},
  year = 2012,
  month = jan,
  school = {Université Paris Diderot (Paris 7)},
  url = {http://gallium.inria.fr/~tramanan/cxx/},
  urlhal = {http://tel.archives-ouvertes.fr/tel-00769044}
}
@inproceedings{2012-Ramananandro-DosReis-Leroy-construction,
  author = {Tahina Ramananandro and Gabriel {Dos Reis} and Xavier Leroy},
  title = {A Mechanized Semantics for {C++} Object Construction and Destruction,
           with Applications to Resource Management},
  booktitle = {Proceedings of the 39th {ACM} Symposium on Principles of
               Programming Languages (POPL'12)},
  pages = {521--532},
  year = 2012,
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~xleroy/publi/cpp-construction.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/2103656.2103718},
  urlhal = {http://hal.inria.fr/hal-00674663},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US}
}
@inproceedings{2012-Garrigue-Remy,
  author = {Jacques Garrigue and Didier R\'emy},
  title = {Tracing ambiguity in {GADT} type inference},
  booktitle = {ACM SIGPLAN Workshop on ML},
  url = {http://www.lexifi.com/ml2012/full7.pdf},
  year = 2012,
  x-international-audience = {yes},
  x-proceedings = {no},
  x-pays = {JP}
}
@article{2012-Remy-Yakobowski-xMLF,
  author = {R{\'e}my, Didier and Yakobowski, Boris},
  title = {A {Church}-Style Intermediate Language for {MLF}},
  journal = {Theoretical Computer Science},
  year = {2012},
  volume = 435,
  number = 1,
  pages = {77--105},
  url = {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski:xmlf@tcs2011.pdf},
  urlpublisher = {http://dx.doi.org/10.1016/j.tcs.2012.02.026},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  abstract = {MLF is a type system that seamlessly merges ML-style implicit but
  second-class polymorphism with System-F explicit first-class
  polymorphism. We present xMLF, a Church-style version of MLF with full type
  information that can easily be maintained during reduction. All parameters
  of functions are explicitly typed and both type abstraction and type
  instantiation are explicit. However, type instantiation in xMLF is more
  general than type application in System F. We equip xMLF with a small-step
  reduction semantics that allows reduction in any context and show that this
  relation is confluent and type preserving. We also show that both subject
  reduction and progress hold for weak-reduction strategies, including
  call-by-value with the value-restriction.}
}
@inproceedings{2012-Robert-Leroy,
  author = {Valentin Robert and Xavier Leroy},
  title = {A Formally-Verified Alias Analysis},
  pages = {11-26},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35308-6_5},
  editor = {Chris Hawblitzel and Dale Miller},
  booktitle = {Certified Programs and Proofs -- Second International Conference, CPP 2012},
  year = 2012,
  series = {Lecture Notes in Computer Science},
  volume = 7679,
  publisher = {Springer},
  url = {http://gallium.inria.fr/~xleroy/publi/alias-analysis.pdf},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2012-Scherer-Remy-MLW,
  author = {Gabriel Scherer and Didier R\'emy},
  title = {{GADTs} meet subtyping},
  booktitle = {ACM SIGPLAN Workshop on ML},
  url = {http://www.lexifi.com/ml2012/full14.pdf},
  year = 2012,
  x-international-audience = {yes},
  x-proceedings = {no}
}
@techreport{2012-Scherer-Remy-TR,
  url = {http://hal.inria.fr/hal-00744292},
  title = {{GADT} meet Subtyping},
  author = {Scherer, Gabriel and R{\'e}my, Didier},
  institution = {INRIA},
  type = {Research report},
  number = {RR-8114},
  year = {2012},
  month = oct
}
@article{2012-Xu-Gossler-Girault,
  author = {Gregor G{\"o}ssler and
               Dana N. Xu and
               Alain Girault},
  title = {Probabilistic contracts for component-based design},
  journal = {Formal Methods in System Design},
  volume = {41},
  number = {2},
  year = {2012},
  pages = {211--231},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  urlpublisher = {http://dx.doi.org/10.1007/s10703-012-0162-4},
  urlhal = {http://hal.inria.fr/hal-00747620}
}
@techreport{2012-Xu-Gossler-Girault-TR,
  author = {G{\"o}ssler, Gregor and Dana N. Xu and Girault, Alain},
  title = {Probabilistic Contracts for Component-based Design},
  type = {Research Report},
  year = {2012},
  month = jul,
  institution = {INRIA},
  number = {RR-7328},
  url = {http://hal.inria.fr/hal-00715750}
}
@inproceedings{2012-Xu-PEPM,
  author = {Dana N. Xu},
  title = {Hybrid contract checking via symbolic simplification},
  booktitle = {Proceedings of the {ACM} SIGPLAN Workshop on Partial Evaluation and
               Program Manipulation (PEPM'12)},
  year = 2012,
  pages = {107--116},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~naxu/research/hcc.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/2103746.2103767},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{2012-Yorgey-Weirich-Cretin-Magalhaes-Jones-Vytiniotis,
  author = {Brent Yorgey and Stephanie Weirich and Julien Cretin and {José Pedro} Magalhães and Simon {Peyton Jones} and Dimitrios Vytiniotis},
  title = {Giving {Haskell} a Promotion},
  booktitle = {The Seventh ACM SIGPLAN Workshop on
               Types in Language Design and Implementation (TLDI'12)},
  year = 2012,
  pages = {67--78},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~jcretin/papers/fc-kind-poly.pdf},
  urlpublisher = {http://dx.doi.org/10.1145/2103786.2103795},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-pays = {US,GB,NL}
}
@inproceedings{2013-Boldo-Jourdan-Leroy-Melquiond,
  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
  urlhal = {http://hal.inria.fr/hal-00743090},
  urlpublisher = {http://dx.doi.org/10.1109/ARITH.2013.30},
  year = 2013,
  booktitle = {ARITH, 21st IEEE International Symposium on Computer Arithmetic},
  pages = {107-115},
  publisher = {IEEE Computer Society Press},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@article{2013-Pottier-ssphs,
  author = {François Pottier},
  title = {Syntactic soundness proof of a type-and-capability system with hidden state},
  journal = {Journal of Functional Programming},
  volume = {23},
  number = {1},
  pages = {38--144},
  urlpublisher = {http://dx.doi.org/10.1017/S0956796812000366},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-ssphs.pdf},
  urlhal = {http://hal.inria.fr/hal-00877589},
  year = {2013},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}
@article{2013-Pottier-sikmhs,
  author = {Jan Schwinghammer and Lars Birkedal and François
                 Pottier and Bernhard Reus and Kristian St{\o}vring and
                 Hongseok Yang},
  title = {A step-indexed {Kripke} Model of Hidden State},
  journal = {Mathematical Structures in Computer Science},
  volume = 23,
  number = 1,
  pages = {1--54},
  year = {2013},
  url = {http://gallium.inria.fr/~fpottier/publis/sikmhs.pdf},
  urlpublisher = {http://dx.doi.org/10.1017/S0960129512000035},
  urlhal = {http://hal.inria.fr/hal-00772757},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {DE,DK,GB}
}
@inproceedings{2013-Scherer-Remy,
  author = {Scherer, Gabriel and R{\'e}my, Didier},
  title = {{GADTs} meet subtyping},
  booktitle = {European Symposium on Programming, ESOP 2013},
  pages = {554-573},
  series = {Lecture Notes in Computer Science},
  volume = 7792,
  publisher = {Springer},
  year = 2013,
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-37036-6_30},
  urlhal = {http://hal.archives-ouvertes.fr/hal-00772993},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2013-Balabonski-ICFP,
  author = {Thibaut Balabonski},
  title = {Weak Optimality, and the Meaning of Sharing},
  booktitle = {Proceedings of the 18th International Conference on Functional Programming (ICFP 2013)},
  year = {2013},
  pages = {263--274},
  publisher = {ACM Press},
  urlpublisher = {http://dx.doi.org/10.1145/2500365.2500606},
  url = {http://gallium.inria.fr/~balabons/Recherche/Balabonski-ICFP13.pdf},
  urlhal = {http://hal.inria.fr/hal-00907056},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2013-Pottier-Protzenko,
  author = {François Pottier and Jonathan Protzenko},
  title = {Programming with permissions in {Mezzo}},
  booktitle = {Proceedings of the 18th International Conference on Functional Programming (ICFP 2013)},
  year = {2013},
  pages = {173--184},
  publisher = {ACM Press},
  urlpublisher = {http://dx.doi.org/10.1145/2500365.2500598},
  url = {http://gallium.inria.fr/~fpottier/publis/pottier-protzenko-mezzo.pdf},
  urlhal = {http://hal.inria.fr/hal-00877590},
  abstract = {We present the design of Mezzo, a programming language
                 in the ML tradition, which places strong emphasis on
                 the control of aliasing and access to mutable memory. A
                 balance between simplicity and expressiveness is
                 achieved by marrying a static discipline of permissions
                 and a dynamic mechanism of adoption and abandon.},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@unpublished{2012-Mezzo-draft-tutorial,
  author = {François Pottier and Jonathan Protzenko},
  title = {An introduction to {Mezzo}},
  note = {Unpublished draft},
  month = sep,
  year = {2012},
  url = {http://gallium.inria.fr/~fpottier/publis/mezzo-tutorial.pdf}
}
@inproceedings{2013-Braibant-Chlipala-FeSi,
  author = {Thomas Braibant and Adam Chlipala},
  title = {Formal Verification of Hardware Synthesis},
  booktitle = {CAV 2013, 25th International Conference on Computer Aided Verification},
  year = 2013,
  pages = {213--228},
  volume = {8044},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  url = {http://gallium.inria.fr/~braibant/fe-si/},
  urlhal = {http://hal.archives-ouvertes.fr/hal-00776876},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-39799-8_14},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2013-Braibant-Jourdan-Monniaux,
  author = {Thomas Braibant and Jacques-Henri Jourdan and David Monniaux},
  title = {Implementing hash-consed structures in {Coq}},
  booktitle = {Interactive Theorem Proving, ITP 2013},
  year = 2013,
  pages = {477-483},
  volume = {7998},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-642-39634-2_36},
  urlhal = {http://hal.archives-ouvertes.fr/hal-00816672},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2013-Scherer-Hoffmann,
  title = {Tracking Data-Flow with Open Closure Types},
  author = {Gabriel Scherer and Jan Hoffmann},
  booktitle = {LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  year = {2013},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 8312,
  pages = {710-726},
  urlhal = {http://hal.inria.fr/hal-00911656},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@techreport{2013-Scherer-Hoffmann-TR,
  urlhal = {http://hal.inria.fr/hal-00851658},
  title = {Tracking Data-Flow with Open Closure Types},
  author = {Scherer, Gabriel and Hoffmann, Jan},
  number = {RR-8345},
  type = {Research Report},
  institution = {Inria},
  urlhal = {http://hal.inria.fr/hal-00851658},
  year = 2013,
  month = aug
}
@inproceedings{2013-Garrigue-Remy-aplas,
  author = {Jacques Garrigue and Didier R{\'e}my},
  title = {Ambivalent Types for Principal Type Inference with
                  {GADTs}},
  x-proceedings = {yes},
  x-international-audience = {yes},
  year = 2013,
  editor = {Shan, Chung-chien},
  volume = 8301,
  series = {Lecture Notes in Computer Science},
  pages = {257-272},
  address = {Melbourne, VIC, Australia},
  month = dec,
  booktitle = {11th Asian Symposium on Programming Languages and Systems, APLAS 2013},
  publisher = {Springer},
  urlhal = {http://hal.inria.fr/hal-00914560}
}
@inproceedings{2013-Doligez-IWIL,
  title = {Proof Certification in {Zenon} Modulo: When {Achilles} Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps},
  author = {David Delahaye and Damien Doligez and Frédéric Gilbert and Pierre Halmagrand and Olivier Hermant},
  booktitle = { IWIL 2013, 10th International Workshop on the Implementation of Logics},
  year = {2013},
  publisher = {EasyChair},
  urlhal = {http://hal.inria.fr/hal-00909784},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@inproceedings{2013-Doligez-LPAR,
  title = {{Zenon} {Modulo}: When {Achilles} Outruns the Tortoise using Deduction Modulo},
  author = {David Delahaye and Damien Doligez and Frédéric Gilbert and Pierre Halmagrand and Olivier Hermant},
  booktitle = {LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  year = {2013},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 8312,
  pages = {274-290},
  urlhal = {http://hal.inria.fr/hal-00909688},
  x-proceedings = {yes},
  x-international-audience = {yes}
}
@unpublished{2013-Acar,
  author = {Acar, Umut and Chargu{\'e}raud, Arthur and Muller, Stefan and Rainey, Mike},
  title = {Atomic Read-Modify-Write Operations are Unnecessary for Shared-Memory Work Stealing},
  year = {2013},
  month = sep,
  urlhal = {http://hal.inria.fr/hal-00910130}
}
@phdthesis{2014-Cretin-phd,
  author = {Julien Cretin},
  title = {Erasable coercions: a unified approach to type systems},
  year = 2014,
  month = jan,
  school = {Université Paris Diderot (Paris 7)},
  url = {http://phd.ia0.fr/},
  urlhal = {http://tel.archives-ouvertes.fr/tel-00940511}
}
@techreport{2014-Cretin-Remy-TR,
  author = {Cretin, Julien and R{\'e}my, Didier},
  title = {System {F} with Coercion Constraints},
  type = {Research Report},
  pages = {36},
  year = {2014},
  month = jan,
  institution = {INRIA},
  number = {RR-8456},
  urlhal = {http://hal.inria.fr/hal-00934408}
}
@inproceedings{2014-Malecha-Chlipala-Braibant,
  author = {Gregory Malecha and Adam Chlipala and Thomas Braibant},
  title = {Compositional Computational Reflection},
  booktitle = {Interactive Theorem Proving, ITP 2014},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = 2014,
  note = {Accepted, to appear in July}
}
@inproceedings{2014-Krebbers-Leroy-Wiedijk,
  author = {Robbert Krebbers and Xavier Leroy and Freek Wiedijk},
  title = {Formal {C} semantics: {CompCert} and the {C} standard},
  booktitle = {Interactive Theorem Proving, ITP 2014},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = 2014,
  note = {Accepted, to appear in July}
}
@inproceedings{2014-Balabonski-Pottier-Protzenko,
  title = {Type Soundness and Race Freedom for {Mezzo}},
  author = {Thibaut Balabonski and Francois Pottier and Jonathan Protzenko},
  booktitle = {Functional and Logic Programming (FLOPS 2014)},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = 2014,
  url = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo.pdf},
  note = {Accepted, to appear in June}
}
@incollection{2014-Leroy-Appel-Blazy-Stewart,
  author = {Leroy, Xavier and Andrew W. Appel and Blazy, Sandrine and Stewart, Gordon},
  title = {The {CompCert} memory model},
  year = {2014},
  month = mar,
  booktitle = {Program Logics for Certified Compilers},
  editor = {Appel, Andrew W.},
  publisher = {Cambridge University Press},
  pages = {237--271}
}
@inproceedings{2014-Cretin-Remy,
  author = {Julien Cretin and Didier Rémy},
  title = {System {F} with Coercion Constraints},
  booktitle = {Computer Science Logic / Logic In Computer Science (CSL-LICS 2014)},
  year = 2014,
  month = jul,
  note = {To appear}
}

This file was generated by bibtex2html 1.97.