@manual{0000-Ocaml-manual,
title = {The {Objective} {Caml} system, documentation and
user's manual -- release 4.06},
author = {Xavier Leroy and Damien Doligez and Jacques Garrigue
and Didier Rémy and Jérôme Vouillon},
organization = {INRIA},
month = nov,
year = 2017,
url = {http://caml.inria.fr/pub/docs/manual-ocaml-4.06/},
urlhal = {https://hal.inria.fr/hal-00930213},
raweb = {foot}
}
@manual{0000-CompCert-manual,
title = {The {CompCert C} verified compiler,
documentation and user's manual},
author = {Xavier Leroy},
organization = {INRIA},
month = aug,
year = 2017,
url = {http://compcert.inria.fr/man/},
urlhal = {https://hal.inria.fr/hal-01091802},
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}
}
@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}
}
@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
}
@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
}
@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,
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}
}
@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},
url = {http://gallium.inria.fr/~remy/ftp/objective-ml!popl97.pdf},
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}
}
@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},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-ic01.ps.gz},
raweb = {foot}
}
@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},
urlpublisher = {http://dx.doi.org/10.1023/A:1025055424017},
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.},
raweb = {foot}
}
@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},
urlpublisher = {http://dx.doi.org/10.1145/596980.596983},
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.},
raweb = {foot}
}
@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.
}
}
@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}
}
@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}
}
@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.},
raweb = {foot}
}
@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},
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}
}
@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},
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,
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}
}
@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},
urlhal = {https://hal.inria.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 = {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},
urlhal = {https://hal.inria.fr/hal-01076682},
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},
urlhal = {https://hal.inria.fr/hal-01091800},
publisher = {IEEE},
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},
urlhal = {https://hal.inria.fr/hal-01091803},
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},
urlhal = {https://hal.inria.fr/hal-01081187},
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},
urlhal = {https://hal.inria.fr/hal-01081193},
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},
urlhal = {https://hal.inria.fr/hal-00674174},
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},
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},
urlhal = {https://hal.inria.fr/hal-00773654},
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},
urlhal = {https://hal.inria.fr/hal-01077321},
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,
urlhal = {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},
urlhal = {https://hal.inria.fr/hal-00674176},
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},
urlhal = {https://hal.inria.fr/hal-01079337},
urlpublisher = {http://dx.doi.org/10.1007/978-3-642-35182-2_27},
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},
urlhal = {https://hal.inria.fr/hal-00772721}
}
@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},
urlhal = {https://hal.inria.fr/hal-01092204},
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},
urlhal = {https://hal.inria.fr/hal-01093845},
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},
urlhal = {https://hal.inria.fr/hal-01093719},
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},
urlhal = {https://hal.inria.fr/hal-00773109},
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},
urlhal = {https://hal.inria.fr/hal-01093816},
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}
}
@article{2012-Maranget-ASS,
title = {Fences in weak memory models (extended version)},
author = {Maranget, Luc and Alglave, Jade and Sarkar, Susmit and Sewell, Peter},
urlhal = {https://hal.inria.fr/hal-01081419},
journal = {{Formal Methods in System Design}},
publisher = {{Springer Verlag (Germany)}},
volume = {40},
number = {2},
pages = {170--205},
year = {2012},
urlpublisher = {http://dx.doi.org/10.1007/s10703-011-0135-z}
}
@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.},
raweb = {refer},
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 = {ITP 2014: Interactive Theorem Proving},
pages = {374-389},
series = {Lecture Notes in Computer Science},
number = 8558,
publisher = {Springer},
year = 2014,
urlpublisher = {http://dx.doi.org/10.1007/978-3-319-08970-6_24}
}
@inproceedings{2014-Krebbers-Leroy-Wiedijk,
author = {Robbert Krebbers and Xavier Leroy and Freek Wiedijk},
title = {Formal {C} semantics: {CompCert} and the {C} standard},
booktitle = {ITP 2014: Interactive Theorem Proving},
series = {Lecture Notes in Computer Science},
pages = {543--548},
publisher = {Springer},
number = 8558,
year = 2014,
urlhal = {http://hal.inria.fr/hal-00981212},
urlpublisher = {http://dx.doi.org/10.1007/978-3-319-08970-6_36}
}
@inproceedings{2014-Balabonski-Pottier-Protzenko,
title = {Type Soundness and Race Freedom for {Mezzo}},
author = {Thibaut Balabonski and Francois Pottier and Jonathan Protzenko},
booktitle = {FLOPS 2014: Functional and Logic Programming},
series = {Lecture Notes in Computer Science},
volume = {8475},
publisher = {Springer},
pages = {253-269},
urlpublisher = {http://dx.doi.org/10.1007/978-3-319-07151-0_16},
urlhal = {https://hal.inria.fr/hal-01081194},
year = 2014,
url = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo.pdf}
}
@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},
urlhal = {https://hal.inria.fr/hal-00905435}
}
@inproceedings{2014-Cretin-Remy,
author = {Julien Cretin and Didier Rémy},
title = {System {F} with Coercion Constraints},
booktitle = {CSL-LICS 2014: Computer Science Logic / Logic In Computer Science},
year = 2014,
urlpublisher = {http://dx.doi.org/10.1145/2603088.2603128},
urlhal = {https://hal.inria.fr/hal-01093239},
pages = {article no 34},
publisher = {ACM},
raweb = {refer}
}
@article{2014-Alglave-Maranget-Tautschnig,
author = {Jade Alglave and
Luc Maranget and
Michael Tautschnig},
title = {Herding cats: modelling, simulation, testing, and data-mining
for weak memory},
journal = {ACM Transactions on Programming Languages and Systems},
volume = 36,
number = 2,
year = 2014,
pages = {article no 7},
url = {http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/toplas14.pdf},
urlpublisher = {http://dx.doi.org/10.1145/2627752},
urlhal = {https://hal.inria.fr/hal-01081364},
raweb = {refer}
}
@inproceedings{2014-Alglave-Maranget-Tautschnig-PLDI,
author = {Jade Alglave and
Luc Maranget and
Michael Tautschnig},
title = {Herding cats: modelling, simulation, testing, and data-mining
for weak memory},
pages = {7},
urlpublisher = {http://dx.doi.org/10.1145/2594291.2594347},
urlhal = {https://hal.inria.fr/hal-01081413},
booktitle = {PLDI 2014: ACM SIGPLAN Conference on Programming Language Design and Implementation},
publisher = {ACM Press},
year = {2014},
note = {Presentation of TOPLAS paper}
}
@article{Dagand-McBride-2014,
author = {Pierre-{\'E}variste Dagand and
Conor McBride},
title = {Transporting functions across ornaments},
journal = {Journal of Functional Programming},
volume = {24},
number = {2-3},
year = {2014},
pages = {316-383},
urlpublisher = {http://dx.doi.org/10.1017/S0956796814000069},
urlhal = {https://hal.inria.fr/hal-00922581}
}
@inproceedings{2014-Pottier-ICFP,
author = {François Pottier},
title = {{Hindley-Milner} elaboration in applicative style},
booktitle = {ICFP 2014: Proceedings of the 19th International Conference on Functional Programming},
year = {2014},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf},
urlpublisher = {http://dx.doi.org/10.1145/2628136.2628145},
urlhal = {https://hal.inria.fr/hal-01081233},
publisher = {ACM},
pages = {203-212}
}
@inproceedings{2014-Acar-Chargueraud-Rainey-ESA,
author = {Umut A. Acar and
Arthur Chargu{\'{e}}raud and
Mike Rainey},
title = {Theory and Practice of Chunked Sequences},
booktitle = {European Symposium on Algorithms, ESA 2014},
year = {2014},
pages = {25--36},
publisher = {Springer},
urlpublisher = {http://dx.doi.org/10.1007/978-3-662-44777-2_3},
urlhal = {https://hal.inria.fr/hal-01087245},
series = {Lecture Notes in Computer Science},
volume = {8737}
}
@article{2014-Braibant-Jourdan-Monniaux,
author = {Thomas Braibant and Jacques-Henri Jourdan and David Monniaux},
title = {Implementing hash-consed structures in {Coq}},
journal = {Journal of Automated Reasoning},
year = 2014,
pages = {271-304},
volume = 53,
number = 3,
urlpublisher = {http://dx.doi.org/10.1007/s10817-014-9306-0},
urlhal = {https://hal.inria.fr/hal-00881085}
}
@inproceedings{2014-Doligez-KLLM,
title = {Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics},
author = {Doligez, Damien and Kriener, Jael and Lamport, Leslie and Libal, Tomer and Merz, Stephan},
urlhal = {https://hal.inria.fr/hal-01063512},
booktitle = {ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics},
year = {2014}
}
@phdthesis{2014-Protzenko-phd,
author = {Jonathan Protzenko},
title = {Mezzo, a typed language for safe effectful concurrent programs},
year = 2014,
month = sep,
school = {Université Paris Diderot (Paris 7)},
url = {http://pauillac.inria.fr/~protzenk/these/},
urlhal = {https://hal.inria.fr/tel-01086106}
}
@inproceedings{2014-Williams-Dagand-Remy,
author = {Thomas Williams and Pierre-Évariste Dagand and Didier Rémy},
title = {Ornaments in Practice},
booktitle = {WGP'14 -- 10th ACM SIGPLAN Workshop on Generic Programming},
url = {http://gallium.inria.fr/~remy/ornaments/ornaments_may2014.pdf},
urlhal = {http://hal.inria.fr/hal-01081547},
urlpublisher = {http://dx.doi.org/10.1145/2633628.2633631},
year = 2014
}
@inproceedings{2014-Braibant-Protzenko-Scherer,
author = {Thomas Braibant and Jonathan Protzenko and Gabriel Scherer},
title = {Well-typed generic smart-fuzzing for {APIs}},
booktitle = {ML'14 -- ACM SIGPLAN ML Family Workshop},
url = {https://sites.google.com/site/mlworkshoppe/fuzzing.pdf},
urlhal = {https://hal.inria.fr/hal-01094006},
year = 2014
}
@inproceedings{2014-Conchon-DMM,
title = {{V{\'e}rification de programmes C concurrents avec Cubicle : Enfoncer les barri{\`e}res}},
author = {Conchon, Sylvain and Declerck, David and Maranget, Luc and Mebsout, Alain},
urlhal = {https://hal.inria.fr/hal-01088655},
booktitle = {{JFLA'14: Journ\'ees Francophones des Langages Applicatifs}},
address = {Fr{\'e}jus, France},
year = {2014},
month = jan
}
@techreport{2014-Acar-Chargueraud-Rainey-TR,
title = {{Data Structures and Algorithms for Robust and Fast Parallel Graph Search}},
author = {Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
urlhal = {https://hal.inria.fr/hal-01089125},
type = {Technical Report},
institution = {{Inria}},
year = {2014},
month = dec
}
@article{2015-Boldo-Jourdan-Leroy-Melquiond,
title = {Verified Compilation of Floating-Point Computations},
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
journal = {Journal of Automated Reasoning},
year = 2015,
volume = 54,
number = 2,
pages = {135--163},
url = {http://gallium.inria.fr/~xleroy/publi/floating-point-compcert.pdf},
urlpublisher = {http://dx.doi.org/10.1007/s10817-014-9317-x},
urlhal = {https://hal.inria.fr/hal-00862689}
}
@inproceedings{jourdan:hal-01078386,
author = {Jacques-Henri Jourdan and Vincent Laporte and
Sandrine Blazy and Xavier Leroy and David Pichardie},
title = {A Formally-Verified {C} Static Analyzer},
booktitle = {POPL'15: 42nd {ACM} Symposium on Principles of
Programming Languages},
publisher = {ACM Press},
year = 2015,
month = jan,
raweb = {refer},
url = {http://gallium.inria.fr/~xleroy/publi/verasco-popl2015.pdf},
urlhal = {https://hal.inria.fr/hal-01078386},
urlpublisher = {http://dx.doi.org/10.1145/2676726.2676966},
pages = {247-259}
}
@inproceedings{dagand:hal-01099138,
title = {{Normalization by realizability also evaluates}},
author = {Dagand, Pierre-Évariste and Scherer, Gabriel},
booktitle = {{JFLA 2015: Vingt-sixièmes Journées Francophones des Langages Applicatifs}},
address = {Le Val d'Ajol, France},
editor = {David Baelde and Jade Alglave},
year = {2015},
month = jan,
urlhal = {https://hal.inria.fr/hal-01099138},
hal_id = {hal-01099138},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {no},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{pottier:hal-01096354,
title = {Depth-First Search and Strong Connectivity in {Coq}},
author = {Pottier, François},
booktitle = {{JFLA 2015: Vingt-sixièmes journées francophones des langages applicatifs}},
address = {Le Val d'Ajol, France},
editor = {David Baelde and Jade Alglave},
year = {2015},
month = jan,
urlhal = {https://hal.inria.fr/hal-01096354},
hal_id = {hal-01096354},
hal_version = {v1},
x-proceedings = {yes},
x-international-audience = {no},
x-editorial-board = {yes},
x-invited-conference = {no},
x-scientific-popularization = {no}
}
@inproceedings{bozman:hal-01099134,
title = {{ocp-memprof: un profileur m{\'e}moire pour OCaml}},
author = {Bozman, {\c C}agdas and Henry, Gr{\'e}goire and Iguernelala, Mohamed and Le Fessant, Fabrice and Mauny, Michel},
urlhal = {https://hal.inria.fr/hal-01099134},
booktitle = {{JFLA 2015: Vingt-sixièmes journées francophones des langages applicatifs}},
address = {Le Val d'Ajol, France},
editor = {David Baelde and Jade Alglave},
year = {2015},
month = jan
}
@inproceedings{scherer:hal-01095390,
author = {Gabriel Scherer and
Didier R{\'{e}}my},
title = {Full Reduction in the Face of Absurdity},
booktitle = {ESOP 2015: Programming Languages and Systems, 24th European Symposium on Programming},
series = {Lecture Notes in Computer Science},
volume = {9032},
pages = {685--709},
publisher = {Springer},
year = {2015},
urlpublisher = {http://dx.doi.org/10.1007/978-3-662-46669-8_28},
urlhal = {https://hal.inria.fr/hal-01095390}
}
@inproceedings{2015-Scherer-Remy-ICFP,
title = {Which simple types have a unique inhabitant?},
author = {Gabriel Scherer and Didier R\'emy},
booktitle = {ICFP'15: 20th International Conference on Functional Programming},
publisher = {ACM Press},
year = 2015,
pages = {243--255},
urlpublisher = {http://dx.doi.org/10.1145/2784731.2784757},
raweb = {foot}
}
@inproceedings{2015-Chargueraud-Pottier,
title = {Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation},
author = {Arthur Charguéraud and François Pottier},
booktitle = {ITP 2015: 6th conference on Interactive Theorem Proving},
year = 2015,
url = {http://www.chargueraud.org/research/2015/complexity/uf.pdf},
series = {Lecture Notes in Computer Science},
volume = 9236,
pages = {137--153},
publisher = {Springer},
urlpublisher = {http://dx.doi.org/10.1007/978-3-319-22102-1_9}
}
@inproceedings{2015-Munch-M-Scherer,
title = {Polarised Intermediate Representation of Lambda Calculus with Sums},
author = {Munch-Maccagnoni, Guillaume and Scherer, Gabriel},
urlhal = {https://hal.inria.fr/hal-01160579},
booktitle = {LICS 2015: 30th Symposium on Logic In Computer Science},
year = {2015},
pages = {127--140},
publisher = {IEEE Computer Society Press},
urlpublisher = {http://dx.doi.org/10.1109/LICS.2015.22}
}
@inproceedings{2015-Scherer-TLCA,
author = {Gabriel Scherer},
title = {Multi-Focusing on Extensional Rewriting with Sums},
booktitle = {TLCA 2015: 13th International Conference on Typed Lambda Calculi and Applications},
series = {LIPIcs},
volume = {38},
pages = {317--331},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
year = {2015},
urlpublisher = {http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.317}
}
@inproceedings{2015-Denes-ITP,
title = {Foundational Property-Based Testing},
author = {Paraskevopoulou, Zoe and Hritcu, Catalin and D{\'e}n{\`e}s, Maxime and Lampropoulos, Leonidas and Pierce, Benjamin C.},
urlhal = {https://hal.inria.fr/hal-01162898},
booktitle = {ITP 2015: 6th conference on Interactive Theorem Proving},
series = {Lecture Notes in Computer Science},
volume = 9236,
pages = {325--343},
publisher = {Springer},
urlpublisher = {http://dx.doi.org/10.1007/978-3-319-22102-1_22},
year = {2015}
}
@inproceedings{2015-Denes-SP,
author = {Arthur Azevedo de Amorim and
Maxime D{\'{e}}n{\`{e}}s and
Nick Giannarakis and
Catalin Hritcu and
Benjamin C. Pierce and
Antal Spector{-}Zabusky and
Andrew Tolmach},
title = {Micro-Policies: Formally Verified, Tag-Based Security Monitors},
booktitle = {SP 2015: {IEEE} Symposium on Security and Privacy},
pages = {813--830},
publisher = {{IEEE} Computer Society},
year = {2015},
urlpublisher = {http://dx.doi.org/10.1109/SP.2015.55}
}
@inproceedings{2015-Acar-Chargueraud-Rainey-SC,
title = {A Work-Efficient Algorithm for Parallel Unordered Depth-First Search},
author = {Umut Acar and Arthur Charguéraud and Mike Rainey},
booktitle = {SC 2015: International Conference for High Performance Computing, Networking, Storage and Analysis},
pages = {67:1--67:12},
publisher = {{ACM}},
year = {2015},
month = nov,
urlpublisher = {http://doi.acm.org/10.1145/2807591.2807651}
}
@inproceedings{2015-Bury-Delahaye-Doligez-HH,
title = {Automated Deduction in the {B} Set Theory using Typed Proof Search and Deduction Modulo},
author = {Bury, Guillaume and Delahaye, David and Doligez, Damien and Halmagrand, Pierre and Hermant, Olivier},
urlhal = {https://hal.inria.fr/hal-01204701},
booktitle = {LPAR 2015: 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
year = {2015},
month = nov,
volume = 9450,
series = {Lecture Notes in Computer Science},
publisher = {Springer}
}
@inproceedings{2015-DoligezFHM15,
author = {Damien Doligez and
Christ{\`{e}}le Faure and
Th{\'{e}}r{\`{e}}se Hardin and
Manuel Maarek},
title = {Avoiding Security Pitfalls with Functional Programming: {A} Report
on the Development of a Secure {XML} Validator},
booktitle = {ICSE 2015: 37th {IEEE/ACM} International Conference on Software Engineering},
pages = {209--218},
publisher = {{IEEE}},
year = {2015},
month = apr,
urlpublisher = {http://dx.doi.org/10.1109/ICSE.2015.149}
}
@inproceedings{2015-Pottier-Protzenko-SNAPL,
author = {Fran{\c{c}}ois Pottier and Jonathan Protzenko},
title = {A Few Lessons from the {Mezzo} Project},
booktitle = {SNAPL 2015: 1st Summit on Advances in Programming Languages},
series = {LIPIcs},
volume = {32},
pages = {221--237},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
year = {2015},
urlpublisher = {http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.221}
}
@inproceedings{2015-Lefessant-ACGTZ,
author = {Pietro Abate and
Roberto Di Cosmo and
Louis Gesbert and
Fabrice Le Fessant and
Ralf Treinen and
Stefano Zacchiroli},
title = {Mining Component Repositories for Installability Issues},
booktitle = {MSR: 12th {IEEE/ACM} Working Conference on Mining Software Repositories},
pages = {24--33},
publisher = {{IEEE}},
year = {2015},
urlpublisher = {http://dx.doi.org/10.1109/MSR.2015.10}
}
@inproceedings{2016-Leroy-BKSPF,
author = {Xavier Leroy and Sandrine Blazy and Daniel K\"astner
and Bernhard Schommer and Markus Pister and Christian Ferdinand},
title = {CompCert -- A Formally Verified Optimizing Compiler},
booktitle = {ERTS 2016: Embedded Real Time Software and Systems},
publisher = {SEE},
year = 2016,
url = {http://gallium.inria.fr/~xleroy/publi/erts2016_compcert.pdf},
urlhal = {http://hal.inria.fr/hal-01238879}
}
@inproceedings{flur:hal-01244776,
title = {Modelling the {ARMv8} Architecture, Operationally: Concurrency and {ISA}},
author = {Flur, Shaked and Gray, Kathryn E. and Pulte, Christopher and Sarkar, Susmit and Sezgin, Ali and Maranget, Luc and Deacon, Will and Sewell, Peter},
urlhal = {https://hal.inria.fr/hal-01244776},
booktitle = {POPL 2016: ACM Symposium on Principles of Programming Languages},
year = {2016},
publisher = {ACM Press}
}
@article{2016-Balabonski-Pottier-Protzenko,
author = {Thibaut Balabonski and François Pottier and Jonathan Protzenko},
title = {The design and formalization of {Mezzo}, a permission-based programming language},
journal = {ACM Transactions on Programming Languages and Systems},
volume = 38,
number = 4,
pages = {14:1--14:94},
year = 2016,
url = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf},
urlpublisher = {http://doi.acm.org/10.1145/2837022},
urlhal = {https://hal.inria.fr/hal-01246534}
}
@phdthesis{2016-Scherer-phd,
author = {Gabriel Scherer},
title = {Which types have a unique inhabitant? Focusing on pure program equivalence},
year = 2016,
month = mar,
school = {Université Paris Diderot (Paris 7)},
url = {http://www.ccs.neu.edu/home/gasche/phd_thesis/scherer-thesis.pdf},
urlhal = {https://tel.archives-ouvertes.fr/tel-01309712}
}
@phdthesis{2016-Jourdan-phd,
author = {Jacques-Henri Jourdan},
title = {Verasco: a Formally Verified {C} Static Analyzer},
year = 2016,
month = may,
school = {Université Paris Diderot (Paris 7)},
url = {https://jhjourdan.mketjh.fr/thesis_jhjourdan.pdf},
urlhal = {https://hal.inria.fr/tel-01327023}
}
@inproceedings{2016-Svendsen-Sieczkowski-Birkedal,
author = {Kasper Svendsen and
Filip Sieczkowski and
Lars Birkedal},
title = {Transfinite Step-Indexing: Decoupling Concrete and Logical Steps},
booktitle = {ESOP 2016: Programming Languages and Systems, 25th European Symposium on Programming},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {727--751},
publisher = {Springer},
year = {2016},
urlpublisher = {http://dx.doi.org/10.1007/978-3-662-49498-1_28}
}
@inproceedings{2016-Acar-CRS,
author = {Umut Acar and Arthur Charguéraud and Mike Rainey and Filip Sieczkowski},
title = {Dag-Calculus: A Calculus for Parallel Computation},
booktitle = {ICFP 2016: 21st International Conference on Functional Programming},
publisher = {ACM Press},
year = {2016},
url = {http://www.chargueraud.org/research/2016/dag_calculus/dag_calculus_icfp16.pdf}
}
@inproceedings{2016-Pottier,
author = {Fran{\c{c}}ois Pottier},
title = {Reachability and error diagnosis in {LR(1)} parsers},
booktitle = {CC 2016: 25th International Conference on Compiler Construction},
pages = {88--98},
publisher = {{ACM}},
year = {2016},
urlpublisher = {http://doi.acm.org/10.1145/2892208.2892224}
}
@article{acar:hal-01409069,
title = {Oracle-Guided Scheduling for Controlling Granularity in Implicitly Parallel Languages},
author = {Acar, Umut A and Chargu{\'e}raud, Arthur and Rainey, Mike},
urlhal = {https://hal.inria.fr/hal-01409069},
journal = {{Journal of Functional Programming}},
publisher = {{Cambridge University Press (CUP)}},
volume = {26},
year = {2016},
month = nov,
doi = {10.1017/S0956796816000101},
hal_id = {hal-01409069},
hal_version = {v1}
}
@inproceedings{jourdan:hal-01406795,
title = {Sparsity Preserving Algorithms for Octagons},
author = {Jourdan, Jacques-Henri},
urlhal = {https://hal.inria.fr/hal-01406795},
booktitle = {{NSAD 2016: Numerical and symbolic abstract domains workshop }},
publisher = {{Elsevier}},
pages = {14},
year = {2016},
month = sep,
hal_id = {hal-01406795},
hal_version = {v1}
}
@inproceedings{azaiez:hal-01322335,
title = {Proving Determinacy of the {PharOS} Real-Time Operating System},
author = {Azaiez, Selma and Doligez, Damien and Lemerre, Matthieu and Libal, Tomer and Merz, Stephan},
url = {https://hal.inria.fr/hal-01322335},
booktitle = {ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference},
publisher = {{Springer}},
series = {LNCS},
volume = {9675},
pages = {70-85},
year = {2016},
month = may,
doi = {10.1007/978-3-319-33600-8\_4},
hal_id = {hal-01322335},
hal_version = {v1}
}
@inproceedings{kastner:hal-01399482,
title = {Closing the Gap -- The Formally Verified Optimizing Compiler {CompCert}},
author = {K{\"a}stner, Daniel and Leroy, Xavier and Blazy, Sandrine and Schommer, Bernhard and Schmidt, Michael and Ferdinand, Christian},
urlhal = {https://hal.inria.fr/hal-01399482},
booktitle = {{SSS 2017: Safety-critical Systems Symposium 2017}},
year = {2017},
month = feb,
hal_id = {hal-01399482},
hal_version = {v1}
}
@inproceedings{acar:hal-01416531,
title = {Contention in Structured Concurrency: Provably Efficient Dynamic Non-Zero Indicators for Nested Parallelism},
author = {Acar, Umut A and Ben-David, Naama and Rainey, Mike},
urlhal = {https://hal.inria.fr/hal-01416531},
booktitle = {PPoPP 2017: 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
year = {2017},
month = feb,
doi = {10.1145/3018743.3018762},
hal_id = {hal-01416531},
hal_version = {v1}
}
@inproceedings{flur:hal-01413221,
title = {{Mixed-size Concurrency: ARM, POWER, C/C++11, and SC}},
author = {Flur, Shaked and Sarkar, Susmit and Pulte, Christopher and Nienhuis, Kyndylan and Maranget, Luc and Gray, Kathryn E. and Sezgin, Ali and Batty, Mark and Sewell, Peter},
urlhal = {https://hal.inria.fr/hal-01413221},
booktitle = {POPL 2017: 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
year = {2017},
month = jan,
pages = {429--442},
doi = {10.1145/3009837.3009839},
hal_id = {hal-01413221},
hal_version = {v1}
}
@inproceedings{pottier:hal-01417102,
title = {Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic},
author = {Pottier, Fran{\c c}ois},
urlhal = {https://hal.inria.fr/hal-01417102},
booktitle = {CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
year = {2017},
month = jan,
pages = {3--16},
doi = {10.1145/3018610.3018624},
hal_id = {hal-01417102},
hal_version = {v1}
}
@inproceedings{2017-Chargueraud-Pottier-slro,
author = {Arthur Charguéraud and François Pottier},
title = {Temporary Read-Only Permissions for Separation Logic},
booktitle = {ESOP 2017: Proceedings of the European Symposium on Programming},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10201},
pages = {260--286},
editor = {Hongseok Yang},
month = apr,
year = {2017},
url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-slro.pdf},
urlpublisher = {https://doi.org/10.1007/978-3-662-54434-1_10},
urlhal = {https://hal.inria.fr/hal-01408657}
}
@article{2017-Pottier-visitors,
author = {Fran{\c{c}}ois Pottier},
title = {Visitors unchained},
journal = {{Proc. ACM on Programming Languages}},
volume = {1},
number = {{ICFP}},
pages = {28:1--28:28},
year = {2017},
urlpublisher = {http://doi.acm.org/10.1145/3110272},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-visitors-unchained.pdf}
}
@inproceedings{chargueraud:hal-01561094,
title = {{VOCAL -- A Verified OCAml Library}},
author = {Chargu{\'e}raud, Arthur and Filli{\^a}tre, Jean-Christophe and Pereira, M{\'a}rio and Pottier, Fran{\c c}ois},
urlhal = {https://hal.inria.fr/hal-01561094},
booktitle = {ML Family Workshop 2017},
year = {2017},
month = sep,
organization = {{ACM}}
}
@inproceedings{bourke:hal-01512286,
title = {A Formally Verified Compiler for {Lustre}},
author = {Bourke, Timothy and Brun, L{\'e}lio and Dagand, Pierre-Evariste and Leroy, Xavier and Pouzet, Marc and Rieg, Lionel},
urlhal = {https://hal.inria.fr/hal-01512286},
urlpublisher = {https://doi.org/10.1145/3062341.3062358},
booktitle = {{PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation}},
address = {Barcelona, Spain},
organization = {{ACM}},
year = {2017},
month = jun
}
@article{2017-Jourdan-Pottier,
author = {Jourdan, Jacques-Henri and Pottier, Fran\c{c}ois},
title = {A Simple, Possibly Correct {LR} Parser for {C11}},
journal = {ACM Trans. Program. Lang. Syst.},
volume = {39},
number = {4},
month = sep,
year = {2017},
pages = {14:1--14:36},
numpages = {36},
urlpublisher = {http://doi.acm.org/10.1145/3064848},
urlhal = {https://hal.archives-ouvertes.fr/hal-01633123}
}
@article{chargueraud:hal-01652785,
title = {Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits},
author = {Chargu{\'e}raud, Arthur and Pottier, Fran{\c c}ois},
urlhal = {https://hal.inria.fr/hal-01652785},
journal = {{Journal of Automated Reasoning}},
publisher = {{Springer Verlag}},
year = {2017},
month = sep,
doi = {10.1007/s10817-017-9431-7},
hal_id = {hal-01652785},
hal_version = {v1}
}
@article{2018-Williams-Remy,
author = {Thomas Williams and Didier Rémy},
title = {A Principled approach to Ornamentation in {ML}},
journal = {{Proc. ACM on Programming Languages}},
volume = {2},
number = {POPL},
articleno = {21},
year = {2018},
month = jan,
urlhal = {https://hal.inria.fr/hal-01666104},
urlpublisher = {http://dx.doi.org/10.1145/3158109}
}
@inproceedings{2018-CompCert-ERTS,
author = {Daniel Kästner and
Ulrich Wünsche and
Jörg Barrho and
Marc Schlickling and
Bernhard Schommer and
Michael Schmidt and
Christian Ferdinand and
Xavier Leroy and
Sandrine Blazy},
title = {{CompCert}: Practical Experience on Integrating and Qualifying
a Formally Verified Optimizing Compiler},
booktitle = {ERTS 2018: Embedded Real Time Software and Systems},
publisher = {SEE},
year = 2018,
month = jan,
urlhal = {https://hal.inria.fr/hal-01643290}
}
@inproceedings{2018-CompCert-WCET,
title = {Embedded Program Annotations for {WCET} Analysis},
author = {Schommer, Bernhard and Cullmann, Christoph and Gebhard, Gernot and Leroy, Xavier and Schmidt, Michael and Wegener, Simon},
urlhal = {https://hal.inria.fr/hal-01848686},
booktitle = {WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis},
pages = {8:1--8:13},
series = {OpenAccess Series in Informatics (OASIcs)},
year = {2018},
month = jul,
volume = {63},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
urlpublisher = {http://drops.dagstuhl.de/opus/volltexte/2018/9754},
hal_id = {hal-01848686},
hal_version = {v1}
}
@inproceedings{barany:hal-01682683,
title = {Finding Missed Compiler Optimizations by Differential Testing},
author = {Barany, Gerg{\"o}},
urlhal = {https://hal.inria.fr/hal-01682683},
booktitle = {{27th International Conference on Compiler Construction}},
address = {Vienna, Austria},
year = {2018},
month = feb,
urlpublisher = {http://dx.doi.org/10.1145/3178372.3179521},
hal_id = {hal-01682683},
hal_version = {v1}
}
@inproceedings{barany:hal-01799629,
title = {A more precise, more correct stack and register model for {CompCert}},
author = {Barany, Gerg{\"o}},
urlhal = {https://hal.inria.fr/hal-01799629},
booktitle = {{LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018}},
address = {Oxford, United Kingdom},
year = {2018},
month = jul,
hal_id = {hal-01799629},
hal_version = {v1}
}
@inproceedings{2018-Acar-CGRS,
author = {Umut A. Acar and
Arthur Chargu{\'{e}}raud and
Adrien Guatto and
Mike Rainey and
Filip Sieczkowski},
title = {Heartbeat scheduling: provable efficiency for nested parallelism},
booktitle = {PLDI 2018: 39th ACM Conference on Programming
Language Design and Implementation},
pages = {769-782},
publisher = {{ACM}},
year = {2018},
urlpublisher = {http://doi.acm.org/10.1145/3192366.3192391},
url = {https://www.chargueraud.org/research/2018/heartbeat/heartbeat.pdf}
}
@inproceedings{2018-Gueneau-CP,
author = {Arma{\"{e}}l Gu{\'{e}}neau and
Arthur Chargu{\'{e}}raud and
Fran{\c{c}}ois Pottier},
title = {A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via
Deductive Program Verification},
booktitle = {ESOP 2018: Programming Languages and Systems - 27th European Symposium on Programming},
series = {Lecture Notes in Computer Science},
volume = {10801},
pages = {533--560},
publisher = {Springer},
year = {2018},
urlpublisher = {https://doi.org/10.1007/978-3-319-89884-1\_19}
}
@inproceedings{alglave:hal-01873636,
title = {Frightening Small Children and Disconcerting Grown-ups: Concurrency in the {Linux} Kernel},
author = {Alglave, Jade and Maranget, Luc and McKenney, Paul and Parri, Andrea and Stern, Alan},
urlhal = {https://hal.inria.fr/hal-01873636},
booktitle = {ASPLOS2018 - 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems},
pages = {405--418},
publisher = {ACM Press},
urlpublisher = {https://doi.org/10.1145/3173162.3177156},
year = {2018}
}
@phdthesis{aksenov:tel-01887505,
title = {Synchronization Costs in Parallel Programs and Concurrent Data Structures},
author = {Aksenov, Vitalii},
urlhal = {https://hal.inria.fr/tel-01887505},
school = {{ITMO University; Paris Diderot University}},
year = {2018},
month = sep
}
@inproceedings{aksenov:hal-01887733,
title = {Brief Announcement: Performance Prediction for Coarse-Grained Locking},
author = {Aksenov, Vitalii and Alistarh, Dan and Kuznetsov, Petr},
urlhal = {https://hal.inria.fr/hal-01887733},
booktitle = {{PODC 2018 -- ACM Symposium on Principles of Distributed Computing}},
year = {2018},
month = jul,
doi = {10.1145/3212734.3212785}
}
@inproceedings{aksenov:hal-01887717,
title = {{Poster: Performance challenges in modular parallel programs}},
author = {Aksenov, Vitalii and Acar, Umut A. and Chargu{\'e}raud, Arthur and Rainey, Mike},
urlhal = {https://hal.inria.fr/hal-01887717},
booktitle = {{PPoPP 2018: 23rd ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming}},
urlpublisher = {http://doi.acm.org/10.1145/3178487.3178516},
year = {2018},
month = feb,
doi = {10.1145/3178487.3178516}
}
@inproceedings{2019-Acar-ACR,
title = {Provably and Practically Efficient Granularity Control},
author = {Umut Acar and Vitaly Aksenov and Arthur Chargu{\'e}raud and Mike Rainey},
booktitle = {PPoPP 2019: 24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming},
pages = {213-228},
publisher = {ACM Press},
year = 2019,
urlhal = {https://hal.inria.fr/hal-01973285},
urlpublisher = {https://doi.org/10.1145/3293883.3295725}
}
@inproceedings{bozman:hal-01962838,
title = {{Learn-OCaml : un assistant {\`a} l'enseignement d'OCaml}},
author = {Bozman, Cagdas and Canou, Benjamin and Di Cosmo, Roberto and Couderc, Pierrick and Gesbert, Louis and Henry, Gr{\'e}goire and le Fessant, Fabrice and Mauny, Michel and Morel, Carine and Peyrot, Lo{\"i}c},
urlhal = {https://hal.inria.fr/hal-01962838},
booktitle = {{Journ{\'e}es Francophones des Langages Applicatifs (JFLA)}},
year = {2019},
month = jan,
hal_id = {hal-01962838},
hal_version = {v1},
x-international-audience = {no}
}
@book{kremer:hal-01993308,
title = {{Cybersecurity}},
author = {Kremer, Steve and M{\'e}, Ludovic and R{\'e}my, Didier and Roca, Vincent},
urlhal = {https://hal.inria.fr/hal-01993308},
publisher = {{Inria}},
series = {Inria white books},
volume = {3},
pages = {172},
year = {2019},
month = jan,
hal_id = {hal-01993308},
hal_version = {v1}
}
@inproceedings{2019-Mevel-Jourdan-Pottier,
author = {Glen Mével and Jacques-Henri Jourdan and François
Pottier},
title = {Time credits and time receipts in {Iris}},
booktitle = {European Symposium on Programming (ESOP)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {11423},
editor = {Luis Caires},
month = apr,
year = {2019},
pages = {1--27},
url = {http://gallium.inria.fr/~fpottier/publis/mevel-jourdan-pottier-time-in-iris-2019.pdf},
urlpublisher = {https://doi.org/10.1007/978-3-030-17184-1_1}
}
@inproceedings{gueneau:hal-02167236,
title = {Formal Proof and Analysis of an Incremental Cycle Detection Algorithm},
author = {Gu{\'e}neau, Arma{\"e}l and Jourdan, Jacques-Henri and Chargu{\'e}raud, Arthur and Pottier, Fran{\c c}ois},
booktitle = {ITP 2019, 10th Conference on Interactive Theorem Proving},
year = {2019},
month = sep,
urlhal = {https://hal.inria.fr/hal-02167236},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
year = {2019},
volume = {141},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
urlpublisher = {http://drops.dagstuhl.de/opus/volltexte/2019/11073}
}
@book{Leroy-lecon-inaugurale,
author = {Xavier Leroy},
title = {Le logiciel, entre l'esprit et la matière},
series = {Leçons inaugurales du Collège de France},
volume = {284},
publisher = {Fayard},
city = {Paris},
year = {2019},
month = sep
}
This file was generated by bibtex2html 1.98.