# pottier.bib

@inproceedings{balabonski-pottier-protzenko-mezzo-14,
author = {Thibaut Balabonski and François Pottier and Jonathan
Protzenko},
title = {Type Soundness and Race Freedom for {Mezzo}},
booktitle = {International Symposium on Functional and Logic
Programming (FLOPS)},
month = jun,
year = {2014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {8475},
pages = {253--269},
url = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo.pdf},
off = {http://dx.doi.org/10.1007/978-3-319-07151-0_16},
abstract = {The programming language Mezzo is equipped with a rich
mutable memory. We incorporate shared-memory
concurrency into Mezzo and present a modular
formalization of Mezzo's core type system, in the form
of a concurrent lambda-calculus, which we extend with
references and locks. We prove that well-typed programs
do not go wrong and are data-race free. Our definitions
and proofs are machine-checked.}
}

@article{balabonski-pottier-protzenko-mezzo-journal-16,
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},
month = aug,
year = {2016},
off = {http://dl.acm.org/authorize?N10539},
url = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf},
doi = {http://dx.doi.org/10.1145/2837022},
soft = {http://gallium.inria.fr/~fpottier/mezzo/mezzo-coq.tar.gz},
abstract = {The programming language Mezzo is equipped with a rich
mutable memory. We give a comprehensive tutorial
overview of the language. Then, we present a modular
formalization of Mezzo's core type system, in the form
of a concurrent $\lambda$-calculus, which we
successively extend with references, locks, and
adoption and abandon, a novel mechanism that marries
Mezzo's static ownership discipline with dynamic
ownership tests. We prove that well-typed programs do
not go wrong and are data-race free. Our definitions
and proofs are machine-checked.}
}

@inproceedings{chargueraud-pottier-08,
author = {Arthur Charguéraud and François Pottier},
title = {Functional Translation of a Calculus of Capabilities},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = sep,
year = {2008},
pages = {213--224},
url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilities.pdf},
off = {http://dl.acm.org/authorize?N05376},
doi = {http://doi.acm.org/10.1145/1411204.1411235},
abstract = {Reasoning about imperative programs requires the
ability to track aliasing and ownership properties. We
present a type system that provides this ability, by
using regions, capabilities, and singleton types. It is
designed for a high-level calculus with higher-order
functions, algebraic data structures, and references
(mutable memory cells). The type system has
polymorphism, yet does not require a value restriction,
because capabilities act as explicit store typings.\par
We exhibit a type-directed, type-preserving, and
meaning-preserving translation of this imperative
calculus into a pure calculus. Like the monadic
translation, this is a store-passing translation. Here,
however, the store is partitioned into multiple
fragments, which are threaded through a computation
only if they are relevant to it. Furthermore, the
decomposition of the store into fragments can evolve
dynamically to reflect ownership transfers.\par The
translation offers deep insight about the inner
workings and soundness of the type system. If coupled
with a semantic model of its target calculus, it leads
to a semantic model of its imperative source calculus.
Furthermore, it provides a foundation for our long-term
objective of designing a system for specifying and
certifying imperative programs with dynamic memory
allocation.}
}

@inproceedings{chargueraud-pottier-15,
author = {Arthur Charguéraud and François Pottier},
title = {Machine-Checked Verification of the Correctness and
Amortized Complexity of an Efficient Union-Find
Implementation},
booktitle = {Interactive Theorem Proving (ITP)},
month = aug,
year = {2015},
volume = {9236},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pages = {137--153},
url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf.pdf},
off = {http://dx.doi.org/10.1007/978-3-319-22102-1_9},
soft = {http://gallium.inria.fr/~fpottier/dev/uf},
abstract = {Union-Find is a famous example of a simple data
structure whose amortized asymptotic time complexity
analysis is non-trivial. We present a Coq formalization
of this analysis. Moreover, we implement Union-Find as
an OCaml library and formally endow it with a modular
specification that offers a full functional correctness
guarantee as well as an amortized complexity bound.
Reasoning in Coq about imperative OCaml code relies on
the CFML tool, which is based on characteristic
formulae and Separation Logic, and which we extend with
time credits. Although it was known in principle that
amortized analysis can be explained in terms of time
credits and that time credits can be viewed as
resources in Separation Logic, we believe our work is
the first practical demonstration of this approach.}
}

@inproceedings{chargueraud-pottier-slro-17,
author = {Arthur Charguéraud and François Pottier},
title = {Temporary Read-Only Permissions for Separation Logic},
booktitle = {European Symposium on Programming (ESOP)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10201},
editor = {Hongseok Yang},
month = apr,
year = {2017},
pages = {260--286},
url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-slro.pdf},
soft = {http://gallium.inria.fr/~fpottier/dev/seplogics/},
abstract = {We present an extension of Separation Logic with a
general mechanism for temporarily converting any
assertion (or permission'') to a read-only form. No
accounting is required: our read-only permissions can
be freely duplicated and discarded. We argue that, in
circumstances where mutable data structures are
permissions enable more concise specifications and
proofs. The metatheory of our proposal is verified in
Coq.}
}

@article{chargueraud-pottier-uf-sltc-17,
author = {Arthur Charguéraud and François Pottier},
title = {Verifying the Correctness and Amortized Complexity of
a Union-Find Implementation in Separation Logic with
Time Credits},
journal = {Journal of Automated Reasoning},
month = sep,
year = {2017},
url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf},
off = {http://rdcu.be/v7EN},
soft = {http://gallium.inria.fr/~fpottier/dev/uf},
abstract = {Union-Find is a famous example of a simple data
structure whose amortized asymptotic time complexity
analysis is nontrivial. We present a Coq formalization
of this analysis, following Alstrup et al.'s recent
proof (2014). Moreover, we implement Union-Find as an
OCaml library and formally endow it with a modular
specification that offers a full functional correctness
guarantee as well as an amortized complexity bound. In
order to reason in Coq about imperative OCaml code, we
use the CFML tool, which implements Separation Logic
for a subset of OCaml, and which we extend with time
credits. Although it was known in principle that
amortized analysis can be explained in terms of time
credits and that time credits can be viewed as
resources in Separation Logic, we believe our work is
the first practical demonstration of this approach.
Finally, in order to explain the meta-theoretical
foundations of our approach, we define a Separation
Logic with time credits for an untyped call-by-value
lambda-calculus, and formally verify its soundness.}
}

@inproceedings{conchon-pottier-01,
author = {Sylvain Conchon and François Pottier},
title = {{JOIN$(X)$}: Constraint-Based Type Inference for the
Join-Calculus},
booktitle = {European Symposium on Programming (ESOP)},
editor = {David Sands},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2028},
pages = {221--236},
month = apr,
year = {2001},
long = {http://gallium.inria.fr/~fpottier/publis/conchon-fpottier-esop01-long.pdf},
url = {http://gallium.inria.fr/~fpottier/publis/conchon-fpottier-esop01.pdf},
abstract = {We present a generic constraint-based type system for
the join-calculus. The key issue is type
generalization, which, in the presence of concurrency,
must be restricted. We first define a liberal
generalization criterion, and prove it correct. Then,
we find that it hinders type inference, and propose a
cruder one, reminiscent of ML's \emph{value
restriction}.\par We establish type safety using a
\emph{semi-syntactic} technique, which we believe is of
independent interest. It consists in interpreting
typing judgements as (sets of) judgements in an
underlying system, which itself is given a syntactic
soundness proof. This hybrid approach allows giving
pleasant logical meaning to high-level notions such as
type variables, constraints and generalization, and
clearly separating them from low-level aspects
(substitution lemmas, etc.), which are dealt with in a
simple, standard way.}
}

@unpublished{de-vilhena-pottier-jourdan-19,
author = {Paulo Emílio de Vilhena and François Pottier and
Jacques-Henri Jourdan},
title = {Spy game---verifying a local generic solver in {Iris}},
note = {Submitted},
month = jul,
year = {2019},
url = {http://gallium.inria.fr/~fpottier/publis/de-vilhena-pottier-jourdan-spy-game-2019.pdf},
abstract = {We verify the partial correctness of a local generic
solver'', that is, an on-demand, incremental, memoizing
least fixed point computation algorithm. The
verification is carried out in Iris, a modern breed of
concurrent separation logic. The specification is
simple: the solver computes the optimal least fixed
point of a system of monotone equations. Although the
solver relies on mutable internal state for memoization
and for spying'', a form of dynamic dependency
discovery, it is apparently pure: no side effects are
mentioned in its specification. As auxiliary
contributions, we provide several illustrations of the
use of prophecy variables, a novel feature of Iris; we
establish a restricted form of the infinitary
conjunction rule; and we provide a specification and
proof of Longley's $\mathit{modulus}$ function, an
archetypical example of spying.}
}

@inproceedings{dicosmo-pottier-remy-05,
author = {Roberto {Di Cosmo} and François Pottier and Didier
Rémy},
title = {Subtyping Recursive Types modulo Associative
Commutative Products},
url = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.pdf},
booktitle = {Seventh International Conference on Typed Lambda
Calculi and Applications (TLCA 2005)},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {3461},
month = apr,
year = {2005},
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.}
}

@article{filliatre-pottier-03,
author = {Jean-Christophe Filliâtre and François Pottier},
title = {Producing All Ideals of a Forest, Functionally},
month = sep,
year = {2003},
url = {http://gallium.inria.fr/~fpottier/publis/filliatre-pottier.pdf},
off = {http://dx.doi.org/10.1017/S0956796803004763},
journal = {Journal of Functional Programming},
volume = {13},
number = {5},
pages = {945--956},
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.}
}

@inproceedings{gauthier-pottier-04,
author = {Nadji Gauthier and François Pottier},
title = {Numbering Matters: First-Order Canonical Forms for
Second-Order Recursive Types},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
url = {http://gallium.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf},
off = {http://dl.acm.org/authorize?N05371},
doi = {http://doi.acm.org/10.1145/1016850.1016872},
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{gueneau-chargueraud-jourdan-pottier-19,
author = {Armaël Guéneau and Jacques-Henri Jourdan and Arthur
Charguéraud and François Pottier},
title = {Formal Proof and Analysis of an Incremental Cycle
Detection Algorithm},
booktitle = {Interactive Theorem Proving (ITP)},
month = sep,
year = {2019},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics},
volume = {141},
editor = {John Harrison and John O'Leary and Andrew Tolmach},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
url = {http://gallium.inria.fr/~fpottier/publis/gueneau-jourdan-chargueraud-pottier-2019.pdf},
off = {https://doi.org/10.4230/LIPIcs.ITP.2019.18}
}

@inproceedings{gueneau-chargueraud-pottier-18,
author = {Armaël Guéneau and Arthur Charguéraud and François
Pottier},
title = {A Fistful of Dollars: Formalizing Asymptotic
Complexity Claims via Deductive Program Verification},
booktitle = {European Symposium on Programming (ESOP)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10801},
pages = {533--560},
editor = {Amal Ahmed},
month = apr,
year = {2018},
volume = {10801},
pages = {533--560},
url = {http://gallium.inria.fr/~fpottier/publis/gueneau-chargeraud-pottier-esop2018.pdf},
abstract = {We present a framework for simultaneously verifying
the functional correctness and the worst-case
asymptotic time complexity of higher-order imperative
programs. We build on top of Separation Logic with Time
Credits, embedded in an interactive proof assistant. We
formalize the $O$ notation, which is key to enabling
modular specifications and proofs. We cover the
subtleties of the multivariate case, where the
complexity of a program fragment depends on multiple
parameters. We propose a way of integrating complexity
bounds into specifications, present lemmas and tactics
that support a natural reasoning style, and illustrate
their use with a collection of examples.}
}

@unpublished{gueneau-pottier-protzenko-13,
author = {Armaël Guéneau and François Pottier and Jonathan
Protzenko},
title = {The ins and outs of iteration in {Mezzo}},
note = {Talk proposal for HOPE 2013},
month = jul,
year = {2013},
url = {http://gallium.inria.fr/~fpottier/publis/gueneau-pottier-protzenko-iteration-in-mezzo.pdf},
abstract = {This is a talk proposal for HOPE 2013. Using iteration
over a collection as a case study, we wish to
illustrate the strengths and weaknesses of the
prototype programming language {Mezzo}.}
}

@inproceedings{jourdan-leroy-pottier-12,
author = {Jacques-Henri Jourdan and François Pottier and Xavier
Leroy},
title = {Validating ${LR}(1)$ Parsers},
month = mar,
year = {2012},
booktitle = {European Symposium on Programming (ESOP)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7211},
pages = {397--416},
url = {http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf},
off = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
abstract = {An $LR(1)$ parser is a finite-state automaton,
equipped with a stack, which uses a combination of its
current state and one lookahead symbol in order to
determine which action to perform next. We present a
validator which, when applied to a context-free grammar
$\mathcal{G}$ and an automaton $\mathcal{A}$, checks
that $\mathcal{A}$ and $\mathcal{G}$ agree. Validating
the parser provides the correctness guarantees required
by verified compilers and other high-assurance software
that involves parsing. The validation process is
independent of which technique was used to construct
$\mathcal{A}$. The validator is implemented and proved
correct using the Coq proof assistant. As an
application, we build a formally-verified parser for
the C99 language.}
}

@article{jourdan-pottier-17,
author = {Jacques-Henri Jourdan and François Pottier},
title = {A simple, possibly correct {LR} parser for {C11}},
journal = {ACM Transactions on Programming Languages and
Systems},
month = aug,
year = {2017},
volume = {39},
number = {4},
pages = {14:1--14:36},
url = {http://gallium.inria.fr/~fpottier/publis/jourdan-fpottier-2016.pdf},
off = {http://dx.doi.org/10.1145/3064848},
soft = {https://github.com/jhjourdan/C11parser}
}

@techreport{mauny-pottier-93,
author = {Michel Mauny and François Pottier},
title = {An implementation of {Caml Light} with existential
types},
number = {2183},
institution = {INRIA},
month = oct,
year = {1993},
off = {http://hal.inria.fr/docs/00/07/44/88/PDF/RR-2183.pdf},
url = {http://gallium.inria.fr/~fpottier/publis/rapport-maitrise.pdf},
abstract = {This work is based on a proposal by Läufer and
Odersky. They show that it is possible to add
existential types to an ML-like language without even
modifying its syntax. ML's strong typing properties are
of course retained. We implemented their proposal into
Caml-Light, thus making it possible to write real-sized
programs using existential types.\par This paper is
divided into three parts. First, we give a definition
of existential types and show how to use them in our
enhanced version of Caml-Light. We then give
interesting examples demonstrating their usefulness.
Finally, a more technical section gives an overview of
the changes made to the compiler and discusses some
technical issues.}
}

@inproceedings{mevel-jourdan-pottier-19,
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},
off = {https://doi.org/10.1007/978-3-030-17184-1_1},
abstract = {We present a machine-checked extension of the program
logic Iris with time credits and time receipts, two
dual means of reasoning about time. Whereas time
credits are used to establish an upper bound on a
program's execution time, time receipts can be used to
establish a lower bound. More strikingly, time receipts
can be used to prove that certain undesirable
events---such as integer overflows---cannot occur until
a very long time has elapsed. We present several
machine-checked applications of time credits and time
receipts, including an application where both concepts
are exploited.}
}

@inproceedings{pilkiewicz-pottier-monotonicity-11,
author = {Alexandre Pilkiewicz and François Pottier},
title = {The essence of monotonic state},
booktitle = {ACM SIGPLAN Workshop on Types in Language Design and
Implementation (TLDI)},
month = jan,
year = {2011},
url = {http://gallium.inria.fr/~fpottier/publis/pilkiewicz-pottier-monotonicity.pdf},
off = {http://dl.acm.org/authorize?N05364},
doi = {http://dx.doi.org/10.1145/1929553.1929565},
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''.\par We
apply these mechanisms to solve two reasoning
challenges that involve mutable state. First, we show
how an implementation of thunks in terms of references
can be assigned types that reflect time complexity
properties, in the style of Danielsson (2008). Second,
we show how an implementation of hash-consing can be
assigned a specification that conceals the existence of
an internal state yet guarantees that two pieces of
input data receive the same code if and only if they
are equal.}
}

@inproceedings{pottier-alphacaml,
author = {François Pottier},
title = {An overview of {C$\alpha$ml}},
month = mar,
year = {2006},
booktitle = {ACM Workshop on ML (ML)},
pages = {27--52},
volume = {148},
number = {2},
series = {Electronic Notes in Theoretical Computer Science},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-alphacaml.pdf},
off = {http://dx.doi.org/10.1016/j.entcs.2005.11.039},
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{pottier-antiframe-08,
author = {François Pottier},
title = {Hiding local state in direct style: a higher-order
anti-frame rule},
month = jun,
year = {2008},
booktitle = {IEEE Symposium on Logic In Computer Science (LICS)},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-antiframe-2008.pdf},
off = {http://doi.ieeecomputersociety.org/10.1109/LICS.2008.16},
pages = {331--340},
abstract = {Separation logic involves two dual forms of
modularity: local reasoning makes part of the store
invisible within a static scope, whereas hiding local
state makes part of the store invisible outside a
static scope. In the recent literature, both idioms are
explained in terms of a higher-order frame rule. I
point out that this approach to hiding local state
imposes continuation-passing style, which is
impractical. Instead, I introduce a higher-order
anti-frame rule, which permits hiding local state in
direct style. I formalize this rule in the setting of a
type system, equipped with linear capabilities, for an
ML-like programming language, and prove type soundness
via a syntactic argument. Several applications
illustrate the expressive power of the new rule.}
}

@unpublished{pottier-appsem-05,
author = {François Pottier},
title = {A modern eye on {ML} type inference: old techniques
and recent developments},
note = {Lecture notes for the {APPSEM} Summer School},
month = sep,
year = {2005},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-appsem-2005.pdf}
}

@unpublished{pottier-caf,
author = {François Pottier},
title = {Three comments on the anti-frame rule},
note = {Unpublished},
month = jul,
year = {2009},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-caf-2009.pdf},
anti-frame rule, which respectively regard: its
interaction with polymorphism; its interaction with the
higher-order frame axiom; and a problematic lack of
modularity.}
}

@inproceedings{pottier-conchon-00,
author = {François Pottier and Sylvain Conchon},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-conchon-icfp00.pdf},
off = {http://dl.acm.org/authorize?N05385},
doi = {http://doi.acm.org/10.1145/351240.351245},
pages = {46--57},
month = sep,
year = {2000},
abstract = {This paper shows how to systematically extend an
arbitrary type system with dependency information, and
how the new system's soundness and non-interference
proofs may rely upon, rather than duplicate, the
original system's soundness proof. This allows
enriching virtually any of the type systems known today
with information flow analysis, while requiring only a
minimal proof effort.\par Our approach is based on an
untyped operational semantics for a labelled calculus
akin to core ML. Thus, it is simple, and should be
applicable to other computing paradigms, such as object
or process calculi.\par The paper also discusses access
control, and shows it may be viewed as entirely
independent of information flow control. Letting the
two mechanisms coexist, without interacting, yields a
simple and expressive type system, which allows, in
particular, selective'' declassification.}
}

@inproceedings{pottier-cpp-17,
author = {François Pottier},
title = {Verifying a hash table and its iterators in
higher-order separation logic},
booktitle = {ACM SIGPLAN Conference on Certified Programs and
Proofs (CPP)},
month = jan,
year = {2017},
pages = {3--16},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-hashtable.pdf},
off = {http://dl.acm.org/authorize?N20956},
doi = {https://doi.org/10.1145/3018610.3018624},
soft = {http://gallium.inria.fr/~fpottier/dev/hash/},
abstract = {We describe the specification and proof of an
(imperative, sequential) hash table implementation. The
usual dictionary operations (insertion, lookup, and so
on) are supported, as well as iteration via folds and
iterators. The code is written in OCaml and verified
using higher-order separation logic, embedded in Coq,
via the CFML tool and library. This case study is part
of a larger project that aims to build a verified OCaml
library of basic data structures.}
}

@unpublished{pottier-cps-17,
author = {François Pottier},
title = {Revisiting the {CPS} Transformation and its
Implementation},
note = {Unpublished},
month = jul,
year = {2017},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-cps.pdf}
}

@inproceedings{pottier-csfw-02,
author = {François Pottier},
title = {A Simple View of Type-Secure Information Flow in the
$\pi$-Calculus},
month = jun,
year = {2002},
address = {Cape Breton, Nova Scotia},
long = {http://gallium.inria.fr/~fpottier/publis/fpottier-csfw15-long.pdf},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-csfw15.pdf},
off = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2002.1021826},
booktitle = {{IEEE} Computer Security Foundations Workshop (CSFW)},
pages = {320--330},
abstract = {One way of enforcing an \emph{information flow
control} policy is to use a static type system capable
of guaranteeing a \emph{noninterference} property.
Noninterference requires that two processes with
distinct high''-level components, but common
low''-level structure, cannot be distinguished by
low''-level observers. We state this property in
terms of a rather strict notion of process equivalence,
namely weak barbed reduction congruence.\par Because
noninterference is not a \emph{safety} property, it is
often regarded as more difficult to establish than a
conventional type safety result. This paper aims to
provide an elementary noninterference proof in the
setting of the $\pi$-calculus. This is done by reducing
the problem to \emph{subject reduction} -- a safety
property -- for a nonstandard, but fairly natural,
extension of the $\pi$-calculus, baptized the
<$\pi$>-calculus.}
}

@techreport{pottier-dea-95,
author = {François Pottier},
title = {Implémentation d'un système de modules évolué en
{Caml-Light}},
institution = {INRIA},
number = {2449},
type = {Research Report},
month = jan,
year = {1995},
off = {http://hal.inria.fr/docs/00/07/42/26/PDF/RR-2449.pdf},
url = {http://gallium.inria.fr/~fpottier/publis/memoire-dea.pdf},
abstract = {Ce mémoire décrit la conception et l'implémentation
d'un langage de modules évolué en Caml-Light. Nous
décrivons d'abord ce que nous entendons par langage de
modules, et l'intérêt qu'un tel langage présente
pour la programmation à moyenne ou grande échelle.
Nous expliquons ensuite en quoi le précurseur en la
matière, SML, souffre de limitations graves vis-à-vis
de la compilation séparée. Nous exposons un système
similaire mais mieux adapté à la compilation
séparée, et en même temps simplifié. Enfin,
certains problèmes d'implémentation inattendus sont
évoqués.}
}

@inproceedings{pottier-dfs-scc-15,
author = {François Pottier},
title = {Depth-First Search and Strong Connectivity in {Coq}},
booktitle = {Journées Francophones des Langages Applicatifs
(JFLA)},
month = jan,
year = {2015},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-dfs-scc.pdf},
off = {https://hal.inria.fr/hal-01091954},
soft = {http://gallium.inria.fr/~fpottier/dfs/dfs.tar.gz},
abstract = {Using Coq, we mechanize Wegener's proof of Kosaraju's
linear-time algorithm for computing the strongly
connected components of a directed graph. Furthermore,
also in Coq, we define an executable and terminating
depth-first search algorithm.},
keywords = {national}
}

@inproceedings{pottier-elaboration-14,
author = {François Pottier},
title = {{Hindley-Milner} elaboration in applicative style},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = sep,
year = {2014},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf},
off = {http://dl.acm.org/authorize?N05361},
doi = {http://dx.doi.org/10.1145/2628136.2628145},
soft = {https://gitlab.inria.fr/fpottier/inferno},
abstract = {Type inference---the problem of determining whether a
program is well-typed---is well-understood. In
contrast, elaboration---the task of constructing an
explicitly-typed representation of the program---seems
to have received relatively little attention, even
though, in a non-local type inference system, it is
non-trivial. We show that the constraint-based
presentation of Hindley-Milner type inference can be
extended to deal with elaboration, while preserving its
elegance. This involves introducing a new notion of
constraint with a value'', which forms an applicative
functor.}
}

@inproceedings{pottier-esop-00,
author = {François Pottier},
title = {A 3-part type inference engine},
booktitle = {European Symposium on Programming (ESOP)},
editor = {Gert Smolka},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1782},
pages = {320--335},
month = mar,
year = {2000},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-esop-2000.pdf},
abstract = {Extending a \emph{subtyping-constraint-based type
inference} framework with \emph{conditional
constraints} and \emph{rows} yields a powerful type
inference engine. We illustrate this claim by proposing
solutions to three delicate type inference problems:
accurate'' pattern matchings, record concatenation,
and dynamic'' messages. Until now, known solutions
required significantly different techniques; our
theoretical contribution is in using only a single (and
simple) set of tools. On the practical side, this
allows all three problems to benefit from a common set
of constraint simplification techniques, leading to
efficient solutions.},
note = {Superseded by~\cite{pottier-njc-00}}
}

@unpublished{pottier-fix-09,
author = {François Pottier},
title = {Lazy Least Fixed Points in {ML}},
note = {Unpublished},
month = dec,
year = {2009},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-fix.pdf},
abstract = {This not quite functional'' pearl describes an
algorithm for computing the least solution of a system
of monotone equations. It is implemented in imperative
\textsc{ocaml} code, but presents a purely functional,
lazy interface. It is simple, useful, and has good
asymptotic complexity. Furthermore, it presents a
challenge to researchers interested in modular formal
proofs of ML programs.}
}

@inproceedings{pottier-fork,
author = {François Pottier},
title = {A typed store-passing translation for general
references},
booktitle = {ACM Symposium on Principles of Programming Languages
(POPL)},
month = jan,
year = {2011},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork-x.pdf},
off = {http://dl.acm.org/authorize?N05363},
doi = {http://dx.doi.org/10.1145/1925844.1926403},
abstract = {We present a store-passing translation of System $F$
with general references into an extension of System
$F_\omega$ with certain well-behaved recursive kinds.
This seems to be the first type-preserving
store-passing translation for general references. It
can be viewed as a purely syntactic account of a
possible worlds model.},
note = {\href{/~fpottier/fork/}{Supplementary material}}
}

@unpublished{pottier-gaf,
author = {François Pottier},
title = {Generalizing the higher-order frame and anti-frame
rules},
note = {Unpublished},
month = jul,
year = {2009},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gaf-2009.pdf},
abstract = {This informal note presents generalized versions of
the higher-order frame and anti-frame rules. The main
insights reside in two successive generalizations of
the tensor'' operator ${}\otimes{}$. In the first
step, a form of local invariant'', which allows
implicit reasoning about well-bracketed state
changes'', is introduced. In the second step, a form of
local monotonicity'' is added.}
}

@inproceedings{pottier-gauthier-04,
author = {François Pottier and Nadji Gauthier},
title = {Polymorphic Typed Defunctionalization},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-popl04.pdf},
booktitle = {ACM Symposium on Principles of Programming Languages
(POPL)},
month = jan,
year = {2004},
pages = {89--98},
off = {http://dl.acm.org/authorize?N05372},
doi = {http://doi.acm.org/10.1145/964001.964009},
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.\par
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.},
note = {Superseded by~\cite{pottier-gauthier-hosc}}
}

@article{pottier-gauthier-hosc,
author = {François Pottier and Nadji Gauthier},
title = {Polymorphic Typed Defunctionalization and
Concretization},
journal = {Higher-Order and Symbolic Computation},
month = mar,
year = {2006},
volume = {19},
pages = {125--162},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf},
off = {http://dx.doi.org/10.1007/s10990-006-8611-7},
abstract = {\emph{Defunctionalization} is a program transformation
that eliminates functions as first-class values. We
show that defunctionalization can be viewed as a
\emph{type-preserving} transformation of an extension
of \f with \emph{guarded algebraic data types} into
itself. We also suggest that defunctionalization is an
instance of \emph{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.}
}

@inproceedings{pottier-gdr-95,
author = {François Pottier},
title = {Type inference and simplification for recursively
constrained types},
booktitle = {Actes du {GDR} Programmation (journée du pôle
Programmation Fonctionnelle)},
month = nov,
year = {1995},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gdr-95.pdf},
abstract = {This paper studies type inference for a functional
language with subtyping, and focuses on the issue of
simplifying inferred types. It does not attempt to give
a fully detailed, formal framework; instead, it tries
to explain the issues informally and suggest possible
solutions by providing examples.},
keywords = {national}
}

@phdthesis{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}
}

@techreport{pottier-hmx-01,
author = {François Pottier},
title = {A semi-syntactic soundness proof for {HM$(X)$}},
institution = {INRIA},
number = {4150},
type = {Research Report},
month = mar,
year = {2001},
abstract = {This document gives a soundness proof for the generic
constraint-based type inference framework {HM$(X)$}.
Our proof is \emph{semi-syntactic}. It consists of two
steps. The first step is to define a \emph{ground} type
system, where polymorphism is \emph{extensional}, and
prove its correctness in a syntactic way. The second
step is to interpret {HM$(X)$} judgements as (sets of)
judgements in the underlying system, which gives a
logical view of polymorphism and constraints. Overall,
the approach may be seen as more modular than a purely
syntactic approach: because polymorphism and
constraints are dealt with separately, they do not
clutter the subject reduction proof. However, it yields
a slightly weaker result: it only establishes type
soundness, rather than subject reduction, for
{HM$(X)$}.}
}

@article{pottier-ic-01,
author = {François Pottier},
title = {Simplifying subtyping constraints: a theory},
journal = {Information \& Computation},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-ic01.pdf},
off = {http://dx.doi.org/10.1006/inco.2001.2963},
month = nov,
year = {2001},
volume = {170},
number = {2},
pages = {153--183},
abstract = {This paper offers a theoretical study of constraint
simplification, a fundamental issue for the designer of
a practical type inference system with subtyping.\par
In the simpler case where constraints are equations, a
simple isomorphism between constrained type schemes and
finite state automata yields a complete constraint
simplification method. Using it as a guide for the
intuition, we move on to the case of subtyping, and
describe several simplification algorithms. Although no
longer complete, they are conceptually simple,
efficient, and very effective in practice.\par Overall,
this paper gives a concise theoretical account of the
techniques found at the core of our type inference
system. Our study is restricted to the case where
constraints are interpreted in a non-structural lattice
of regular terms. Nevertheless, we highlight a small
number of general ideas, which explain our algorithms
at a high level and may be applicable to a variety of
other systems.}
}

@inproceedings{pottier-icfp-96,
author = {François Pottier},
title = {Simplifying subtyping constraints},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = may,
year = {1996},
pages = {122--133},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp96.pdf},
off = {http://dl.acm.org/authorize?N05387},
doi = {http://doi.acm.org/10.1145/232627.232642},
abstract = {This paper studies type inference for a functional,
ML-style language with subtyping, and focuses on the
issue of simplifying inferred constraint sets. We
propose a powerful notion of entailment between
constraint sets, as well as an algorithm to check it,
which we prove to be sound. The algorithm, although
very powerful in practice, is not complete. We also
introduce two new typing rules which allow simplifying
constraint sets. These rules give very good practical
results.}
}

@inproceedings{pottier-icfp-98,
author = {François Pottier},
title = {A Framework for Type Inference with Subtyping},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = sep,
year = {1998},
pages = {228--238},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp98.pdf},
off = {http://dl.acm.org/authorize?N05386},
doi = {http://doi.acm.org/10.1145/289423.289448},
abstract = {This paper describes a full framework for type
inference and simplification in the presence of
subtyping. We give a clean, simple presentation of the
system and show that it leads to an efficient
implementation. Previous inference systems had severe
efficiency problems, mainly by lack of a systematic
substitution algorithm, but also because the issue of
data representation was not settled. We explain how to
solve these problems and obtain a fully integrated
framework.}
}

@inproceedings{pottier-lics-03,
author = {François Pottier},
title = {A Constraint-Based Presentation and Generalization of
Rows},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-lics03.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/fpottier-lics03-long.pdf},
off = {http://ieeexplore.ieee.org/xpl/abs_free.jsp?arNumber=1210073},
other = {http://csdl.computer.org/comp/proceedings/lics/2003/1884/00/18840331abs.htm},
booktitle = {IEEE Symposium on Logic In Computer Science (LICS)},
pages = {331--340},
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.}
}

@article{pottier-njc-00,
author = {François Pottier},
title = {A Versatile Constraint-Based Type Inference System},
journal = {Nordic Journal of Computing},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-njc-2000.pdf},
month = nov,
year = {2000},
volume = {7},
number = {4},
pages = {312--347},
abstract = {The combination of \emph{subtyping}, \emph{conditional
constraints} and \emph{rows} yields a powerful
\emph{constraint-based type inference} system. We
illustrate this claim by proposing solutions to three
delicate type inference problems: accurate'' pattern
matchings, record concatenation, and first-class
messages. Previously known solutions involved a
different technique in each case; our theoretical
contribution is in using only a single set of tools. On
the practical side, this allows all three problems to
benefit from a common set of constraint simplification
techniques, a formal description of which is given in
an appendix.}
}

@techreport{pottier-phd-english-98,
author = {François Pottier},
title = {Type inference in the presence of subtyping: from
theory to practice},
institution = {INRIA},
number = {3483},
type = {Research Report},
month = sep,
year = {1998},
url = {http://hal.inria.fr/docs/00/07/32/05/PDF/RR-3483.pdf},
abstract = {From a purely theoretical point of view, type
inference for a functional language with parametric
polymorphism and subtyping poses no difficulties.
Indeed, it suffices to generalize the inference
algorithm used in the ML language, so as to deal with
type inequalities, rather than equalities. However, the
number of such inequalities is linear in the program
size; whence, from a practical point of view, a serious
efficiency and readability problem.\par To solve this
problem, one must simplify the inferred constraints.
So, after studying the logical properties of subtyping
constraints, this work proposes several simplification
algorithms. They combine seamlessly, yielding a
homogeneous, fully formal framework, which directly
leads to an efficient implementation. Although this
theoretical study is performed in a simplified setting,
numerous extensions are possible. Thus, this framework
is realistic, and should allow a practical appearance
of subtyping in languages with type inference.\par This
is the English version of the author's PhD
dissertation.}
}

@phdthesis{pottier-phd-french-98,
author = {François Pottier},
title = {Synthèse de types en présence de sous-typage: de la
théorie à la pratique},
school = {Université Paris 7},
month = jul,
year = {1998},
url = {http://gallium.inria.fr/~fpottier/publis/these-fpottier.pdf},
abstract = {D'un point de vue purement théorique, l'inférence de
types pour un langage fonctionnel doté de
polymorphisme paramétrique et de sous-typage ne pose
pas de difficultés. Il suffit en effet de
généraliser l'algorithme d'inférence utilisé par le
langage ML, de façon à manipuler non plus des
égalités, mais des inégalités entre types.
Cependant, celles-ci sont engendrées en nombre
proportionnel à la taille du programme, ce qui pose,
d'un point de vue pratique, un grave problème
d'efficacité et de lisibilité.\par Pour résoudre ce
problème, il est nécessaire de simplifier les
contraintes inférées. Ce travail étudie donc d'abord
les propriétés logiques des contraintes de
sous-typage, puis propose plusieurs algorithmes de
simplification. Ceux-ci se composent naturellement pour
former un tout homogène, entièrement formalisé, qui
conduit directement à une implémentation efficace.
Bien que cette étude théorique soit effectuée dans
un cadre simplifié, de nombreuses extensions sont
possibles. Le système proposé est donc réaliste, et
permet d'imaginer l'introduction pratique du
sous-typage dans des langages dotés d'inférence de
types.}
}

@inproceedings{pottier-protzenko-13,
author = {François Pottier and Jonathan Protzenko},
title = {Programming with permissions in {Mezzo}},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = sep,
year = {2013},
pages = {173--184},
url = {http://gallium.inria.fr/~fpottier/publis/pottier-protzenko-mezzo.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/mezzo-icfp2013-long.pdf},
off = {http://dl.acm.org/authorize?N05362},
doi = {http://dx.doi.org/10.1145/2500365.2500598},
abstract = {We present Mezzo, a typed programming language of ML
lineage. Mezzo is equipped with a novel static
discipline of duplicable and affine permissions, which
controls aliasing and ownership. This rules out certain
mistakes, including representation exposure and data
races, and enables new idioms, such as gradual
initialization, memory re-use, and (type)state changes.
Although the core static discipline disallows sharing a
mutable data structure, Mezzo offers several ways of
working around this restriction, including a novel
dynamic ownership control mechanism which we dub
adoption and abandon''.}
}

@inproceedings{pottier-protzenko-lessons-mezzo-15,
author = {François Pottier and Jonathan Protzenko},
title = {A few lessons from the {Mezzo} project},
booktitle = {Summit oN Advances in Programming Languages (SNAPL)},
month = may,
year = {2015},
pages = {221--237},
series = {Leibniz International Proceedings in Informatics},
volume = {32},
editor = {Thomas Ball and Rastislav Bodik and Shriram
Krishnamurthi and Benjamin S. Lerner and Greg
Morrisett},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-protzenko-lessons-mezzo.pdf},
off = {http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.221},
abstract = {With Mezzo, we set out to design a new, better
programming language. In this modest document, we
recount our adventure: what worked, and what did not;
the decisions that appear in hindsight to have been
good, and the design mistakes that cost us; the things
that we are happy with in the end, and the frustrating
aspects we wish we had handled better.}
}

@inproceedings{pottier-pure-freshml,
author = {François Pottier},
title = {Static Name Control for {FreshML}},
month = jul,
year = {2007},
booktitle = {IEEE Symposium on Logic In Computer Science (LICS)},
pages = {356--365},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml-long.pdf},
off = {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
on a conservative, automatic decision procedure for
this logic. It is argued that Pure FreshML can express
non-trivial syntax-manipulating algorithms.}
}

@inproceedings{pottier-reachability-cc-2016,
author = {François Pottier},
title = {Reachability and error diagnosis in {LR}(1) parsers},
booktitle = {International Conference on Compiler Construction
(CC)},
month = mar,
year = {2016},
pages = {88--98},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-reachability-cc2016.pdf},
doi = {http://dx.doi.org/10.1145/2892208.2892224},
off = {http://dl.acm.org/authorize?N10538},
abstract = {Given an LR(1) automaton, what are the states in which
an error can be detected? For each such error
state'', what is a minimal input sentence that causes
an error in this state? We propose an algorithm that
answers these questions. This allows building a
collection of pairs of an erroneous input sentence and
a (handwritten) diagnostic message, ensuring that this
collection covers every error state, and maintaining
this property as the grammar evolves. We report on an
application of this technique to the CompCert ISO C99
parser, and discuss its strengths and limitations.}
}

@inproceedings{pottier-reachability-jfla-2016,
author = {François Pottier},
title = {Reachability and error diagnosis in {LR}(1) automata},
booktitle = {Journées Francophones des Langages Applicatifs
(JFLA)},
month = jan,
year = {2016},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-reachability-jfla2016.pdf},
off = {https://hal.inria.fr/hal-01248101},
abstract = {Given an LR(1) automaton, what are the states in which
an error can be detected? For each such error
state'', what is a minimal input sentence that causes
an error in this state? We propose an algorithm that
answers these questions. Such an algorithm allows
building a collection of pairs of an erroneous input
sentence and a diagnostic message, ensuring that this
collection covers every error state, and maintaining
this property as the grammar evolves. We report on an
application of this technique to the CompCert ISO C99
parser, and discuss its strengths and limitations.},
keywords = {national}
}

@inproceedings{pottier-regis-gianas-06,
author = {François Pottier and Yann Régis-Gianas},
title = {Stratified type inference for generalized algebraic
data types},
booktitle = {ACM Symposium on Principles of Programming Languages
(POPL)},
month = jan,
year = {2006},
pages = {232--244},
url = {http://gallium.inria.fr/~fpottier/publis/pottier-regis-gianas-popl06.pdf},
off = {http://dl.acm.org/authorize?N05378},
doi = {http://doi.acm.org/10.1145/1111037.1111058},
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{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},
off = {http://dx.doi.org/10.1016/j.entcs.2005.11.044},
month = mar,
year = {2006},
pages = {155--180},
booktitle = {ACM Workshop on ML (ML)},
series = {Electronic Notes in Theoretical Computer Science},
volume = {148},
number = {2},
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.}
}

@incollection{pottier-remy-emlti,
author = {François Pottier and Didier Rémy},
title = {The Essence of {ML} Type Inference},
booktitle = {Advanced Topics in Types and Programming Languages},
pages = {389--489},
publisher = {MIT Press},
year = {2005},
editor = {Benjamin C. Pierce},
chapter = {10},
url = {http://gallium.inria.fr/~fpottier/publis/emlti-final.pdf},
off = {http://www.cis.upenn.edu/~bcpierce/attapl},
note = {A \href{http://cristal.inria.fr/attapl/}{draft
extended version} is also available}
}

@inproceedings{pottier-simonet-02,
author = {François Pottier and Vincent Simonet},
title = {Information Flow Inference for {ML}},
booktitle = {ACM Symposium on Principles of Programming Languages
(POPL)},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-popl02.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-popl02-long.pdf},
month = jan,
year = {2002},
pages = {319--330},
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.},
off = {http://dl.acm.org/authorize?N05374},
doi = {http://doi.acm.org/10.1145/503272.503302},
note = {Superseded by~\cite{pottier-simonet-toplas-03}}
}

@article{pottier-simonet-toplas-03,
author = {François Pottier and Vincent Simonet},
title = {Information Flow Inference for {ML}},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-toplas.pdf},
month = jan,
year = {2003},
volume = {25},
number = {1},
pages = {117--158},
journal = {ACM Transactions on Programming Languages and
Systems},
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.},
off = {http://dl.acm.org/authorize?N05373},
doi = {http://doi.acm.org/10.1145/596980.596983}
}

@inproceedings{pottier-skalka-smith-01,
author = {François Pottier and Christian Skalka and Scott
Smith},
title = {A Systematic Approach to Static Access Control},
booktitle = {European Symposium on Programming (ESOP)},
editor = {David Sands},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {2028},
pages = {30--45},
month = apr,
year = {2001},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-skalka-smith-esop01.pdf},
abstract = {The Java JDK 1.2 Security Architecture includes a
dynamic mechanism for enforcing access control checks,
so-called \emph{stack inspection}. This paper studies
type systems which can statically guarantee the success
of these checks. We develop these systems using a new,
systematic methodology: we show that the
security-passing style translation, proposed by Wallach
and Felten as a \emph{dynamic} implementation
technique, also gives rise to \emph{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.
They offer significant improvements on a previous type
system for JDK access control, both in terms of
expressiveness and in terms of readability of type
specifications.},
note = {Superseded by~\cite{pottier-skalka-smith-05}}
}

@article{pottier-skalka-smith-05,
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.pdf},
off = {http://dl.acm.org/authorize?N05370},
doi = {http://doi.acm.org/10.1145/1057387.1057392},
month = mar,
year = {2005},
volume = {27},
number = {2},
pages = {344--382},
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 \emph{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
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 \emph{dynamic}
implementation technique, also gives rise to
\emph{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.}
}

@article{pottier-ssphs-13,
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},
month = jan,
year = {2013},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-ssphs.pdf},
off = {http://dx.doi.org/10.1017/S0956796812000366},
abstract = {This paper presents a formal definition and
machine-checked soundness proof for a very expressive
type-and-capability system, that is, a low-level type
system that keeps precise track of ownership and side
effects. \par The programming language has first-class
functions and references. The type system's features
include: universal, existential, and recursive types;
subtyping; a distinction between affine and
unrestricted data; support for strong updates; support
for naming values and heap fragments, via singleton and
group regions; a distinction between ordinary values
(which exist at runtime) and capabilities (which
don't); support for dynamic re-organizations of the
ownership hierarchy, by dis-assembling and
re-assembling capabilities; support for temporarily or
permanently hiding a capability, via frame and
anti-frame rules. \par One contribution of the paper is
the definition of the type-and-capability system
itself. We present the system as modularly as possible.
In particular, at the core of the system, the treatment
of affinity, in the style of dual intuitionistic linear
logic, is formulated in terms of an arbitrary monotonic
separation algebra, a novel axiomatization of
resources, ownership, and the manner in which they
evolve with time. Only the peripheral layers of the
system are aware that we are dealing with a specific
monotonic separation algebra, whose resources are
references and regions. This semi-abstract organization
should facilitate further extensions of the system with
new forms of resources. \par The other main
contribution is a machine-checked proof of type
soundness. The proof is carried out in Wright and
Felleisen's syntactic style. This offers evidence that
this relatively simple-minded proof technique can scale
up to systems of this complexity, and constitutes a
viable alternative to more sophisticated semantic proof
techniques. We do not claim that the syntactic
technique is superior: we simply illustrate how it is
used and highlight its strengths and shortcomings.}
}

@inproceedings{pottier-visitors-17,
author = {François Pottier},
title = {Visitors Unchained},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
month = sep,
year = {2017},
url = {http://gallium.inria.fr/~fpottier/publis/fpottier-visitors-unchained.pdf},
off = {http://dx.doi.org/10.1145/3110272},
abstract = {Traversing and transforming abstract syntax trees that
involve name binding is notoriously difficult to do in
a correct, concise, modular, customizable manner. We
address this problem in the setting of OCaml, a
functional programming language equipped with powerful
object-oriented features. We use visitor classes as
partial, composable descriptions of the operations that
we wish to perform on abstract syntax trees. We
introduce \texttt{visitors}, a~simple type-directed
facility for generating visitor classes that have no
knowledge of binding. Separately, we present
\texttt{alphaLib}, a library of small hand-written
visitor classes, each of which knows about a specific
binding construct, a specific representation of names,
and/or a specific operation on abstract syntax trees.
By combining these components, a wide range of
operations can be defined. Multiple representations of
names can be supported, as well as conversions between
representations. Binding structure can be described
either in a programmatic style, by writing visitor
methods, or in a declarative style, via preprogrammed
binding combinators.}
}

@article{pouillard-pottier-12,
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},
month = sep,
year = {2012},
url = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-unified.pdf},
off = {http://dx.doi.org/10.1017/S0956796812000251},
abstract = {Atoms and de Bruijn indices are two well-known
representation techniques for data structures that
involve names and binders. However, using either
technique, it is all too easy to make a programming
error that causes one name to be used where another was
intended.\par We propose an abstract interface to names
and binders that rules out many of these errors. This
interface is implemented as a library in Agda. It
allows defining and manipulating term representations
in nominal style and in de Bruijn style. The programmer
is not forced to choose between these styles: on the
contrary, the library allows using both styles in the
same program, if desired.\par Whereas indexing the
types of names and terms with a natural number is a
well-known technique to better control the use of de
Bruijn indices, we index types with worlds. Worlds are
at the same time more precise and more abstract than
natural numbers. Via logical relations and
parametricity, we are able to demonstrate in what sense
about world-polymorphic functions. For instance, we
prove that a world-polymorphic term transformation
function must commute with any renaming of the free
variables. The proof is entirely carried out in Agda.}
}

@inproceedings{pouillard-pottier-fresh-look-2010,
author = {Nicolas Pouillard and François Pottier},
title = {A fresh look at programming with names and binders},
booktitle = {ACM SIGPLAN International Conference on Functional
Programming (ICFP)},
pages = {217--228},
month = sep,
year = {2010},
off = {http://dl.acm.org/authorize?N05375},
doi = {http://doi.acm.org/10.1145/1863543.1863575},
url = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-fresh-look.pdf},
long = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-fresh-look-x.pdf},
abstract = {A wide range of computer programs, including compilers
and theorem provers, manipulate data structures that
involve names and binding. However, the design of
programming idioms which allow performing these
manipulations in a safe and natural style has, to a
large extent, remained elusive.\par In this paper, we
present a novel approach to the problem. Our proposal
can be viewed either as a programming language design
or as a library: in fact, it is currently implemented
within Agda. It provides a safe and expressive means of
programming with names and binders. It is abstract
enough to support multiple concrete implementations: we
present one in nominal style and one in de Bruijn
style. We use logical relations to prove that
well-typed programs do not mix names with different
scope''. We exhibit an adequate encoding of Pitts-style
nominal terms into our system.}
}

@inproceedings{regis-gianas-pottier-08,
author = {Yann Régis-Gianas and François Pottier},
title = {A {Hoare} Logic for Call-by-Value Functional
Programs},
booktitle = {International Conference on Mathematics of Program
Construction (MPC)},
month = jul,
year = {2008},
series = {Lecture Notes in Computer Science},
volume = {5133},
publisher = {Springer},
url = {http://gallium.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf},
off = {http://dx.doi.org/10.1007/978-3-540-70594-9_17},
pages = {305--335},
abstract = {We present a Hoare logic for a call-by-value
programming language equipped with recursive,
higher-order functions, algebraic data types, and a
polymorphic type system in the style of Hindley and
Milner. It is the theoretical basis for a tool that
extracts proof obligations out of programs annotated
with logical assertions. These proof obligations,
expressed in a typed, higher-order logic, are
discharged using off-the-shelf automated or interactive
theorem provers. Although the technical apparatus that
we exploit is by now standard, its application to
functional programming languages appears to be new, and
(we claim) deserves attention. As a sample application,
we check the partial correctness of a balanced binary
search tree implementation.}
}

@inproceedings{schwinghammer-shfs-10,
author = {Jan Schwinghammer and Hongseok Yang and Lars Birkedal
and François Pottier and Bernhard Reus},
title = {A Semantic Foundation for Hidden State},
booktitle = {International Conference on Foundations of Software
Science and Computational Structures (FOSSACS)},
month = mar,
year = {2010},
pages = {2--17},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6014},
editor = {C.-H. L. Ong},
url = {http://gallium.inria.fr/~fpottier/publis/sfhs.pdf},
off = {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.}
}

@article{sikmhs-13,
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},
month = feb,
year = {2013},
volume = {23},
number = {1},
pages = {1--54},
url = {http://gallium.inria.fr/~fpottier/publis/sikmhs.pdf},
off = {http://dx.doi.org/10.1017/S0960129512000035}
}

@techreport{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://gallium.inria.fr/~fpottier/publis/simonet-pottier-hmg.pdf},
off = {http://hal.inria.fr/docs/00/07/05/44/PDF/RR-5462.pdf}
}

@article{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},
url = {http://gallium.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.pdf},
off = {http://dl.acm.org/authorize?N05377},
doi = {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.}
}

@inproceedings{skalka-pottier-tip-02,
author = {Christian Skalka and François Pottier},
title = {Syntactic Type Soundness for {HM$(X)$}},
month = jul,
year = {2002},
url = {http://gallium.inria.fr/~fpottier/publis/skalka-fpottier-tip-02.pdf},
booktitle = {Workshop on Types in Programming (TIP)},
series = {Electronic Notes in Theoretical Computer Science},
volume = {75},
abstract = {The HM$(X)$ framework is a constraint-based type
framework with built-in let-polymorphism. This paper
establishes purely syntactic type soundness for the
framework, treating an extended version of the language
containing state and recursive binding. These results
demonstrate that any instance of HM$(X)$, comprising a
specialized constraint system and possibly additional
functional constants and their types, enjoys syntactic
type soundness.}
}


This file was generated by bibtex2html 1.99.