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 = {Proceedings of the 12th International Symposium on
                 Functional and Logic Programming (FLOPS 2014)},
  month = jun,
  year = {2014},
  series = lncs,
  publisher = springer,
  volume = {8475},
  pages = {253--269},
  pdf = {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
                 type system that controls aliasing and access to
                 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.}
}
@unpublished{balabonski-pottier-protzenko-mezzo-journal-14,
  author = {Thibaut Balabonski and François Pottier and Jonathan
                 Protzenko},
  title = {The Design and Formalization of {Mezzo}, a
                 Permission-Based Programming Language},
  month = jul,
  year = {2014},
  pdf = {http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf},
  note = {Submitted for publication},
  abstract = {The programming language Mezzo is equipped with a rich
                 type system that controls aliasing and access to
                 mutable memory. We present the language at large, via
                 an introduction along with some motivating examples. We
                 then 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.}
}
@inproceedings{chargueraud-pottier-08,
  author = {Arthur Charguéraud and François Pottier},
  title = {Functional Translation of a Calculus of Capabilities},
  booktitle = {Proceedings of the 2008 {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'08)},
  month = sep,
  year = {2008},
  pages = {213--224},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilities.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilities.pdf},
  off = {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{conchon-pottier-01,
  author = {Sylvain Conchon and François Pottier},
  title = {{JOIN$(X)$}: Constraint-Based Type Inference for the
                 Join-Calculus},
  booktitle = {Proceedings of the 10th European Symposium on
                 Programming (ESOP'01)},
  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.ps.gz},
  url = {http://gallium.inria.fr/~fpottier/publis/conchon-fpottier-esop01.ps.gz},
  off = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2028&spage=30},
  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.}
}
@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.ps.gz},
  pdf = {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},
  off = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11417170_14},
  booktitle = {Seventh International Conference on Typed Lambda
                 Calculi and Applications (TLCA'05)},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {3461},
  address = {Nara, Japan},
  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.ps.gz},
  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.}
}
@unpublished{fpottier-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.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-appsem-2005.pdf}
}
@inproceedings{gauthier-pottier-04,
  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.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/gauthier-fpottier-icfp04.pdf},
  off = {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.}
}
@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},
  pdf = {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 = {Proceedings of the 21st European Symposium on
                 Programming (ESOP 2012)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {7211},
  pages = {397--416},
  pdf = {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.}
}
@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},
  pdf = {http://hal.inria.fr/docs/00/07/44/88/PDF/RR-2183.pdf},
  url = {http://gallium.inria.fr/~fpottier/publis/rapport-maitrise.ps.gz},
  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{pilkiewicz-pottier-monotonicity-11,
  author = {Alexandre Pilkiewicz and François Pottier},
  title = {The essence of monotonic state},
  booktitle = {Proceedings of the Sixth {ACM} {SIGPLAN} Workshop on
                 Types in Language Design and Implementation (TLDI'11)},
  month = jan,
  year = {2011},
  address = {Austin, Texas},
  pdf = {http://gallium.inria.fr/~fpottier/publis/pilkiewicz-pottier-monotonicity.pdf},
  off = {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},
  pages = {27--52},
  volume = {148},
  number = {2},
  series = {Electronic Notes in Theoretical Computer Science},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-alphacaml.ps.gz},
  pdf = {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.}
}
@misc{pottier-alphacaml-software,
  author = {François Pottier},
  title = {{C$\alpha$ml}},
  soft = {http://gallium.inria.fr/~fpottier/alphaCaml/},
  month = jun,
  year = {2005}
}
@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 = {Twenty-Third Annual {IEEE} Symposium on Logic In
                 Computer Science (LICS'08)},
  address = {Pittsburgh, Pennsylvania},
  pdf = {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-caf,
  author = {François Pottier},
  title = {Three comments on the anti-frame rule},
  note = {Unpublished},
  month = jul,
  year = {2009},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-caf-2009.pdf},
  abstract = {This informal note presents three comments about the
                 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},
  title = {Information Flow Inference for Free},
  booktitle = {Proceedings of the Fifth {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'00)},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-conchon-icfp00.ps.gz},
  off = {http://doi.acm.org/10.1145/351240.351245},
  pages = {46--57},
  address = {Montréal, Canada},
  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-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.ps.gz},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-csfw15.ps.gz},
  off = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2002.1021826},
  booktitle = {Proceedings of the 15th {IEEE} Computer Security
                 Foundations Workshop},
  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},
  pdf = {http://hal.inria.fr/docs/00/07/42/26/PDF/RR-2449.pdf},
  url = {http://gallium.inria.fr/~fpottier/publis/memoire-dea.ps.gz},
  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.}
}
@unpublished{pottier-dfs-scc-15,
  author = {François Pottier},
  title = {Depth-First Search and Strong Connectivity in {Coq}},
  month = sep,
  year = {2014},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-dfs-scc.pdf},
  note = {Submitted for publication},
  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.}
}
@inproceedings{pottier-elaboration-13,
  author = {François Pottier},
  title = {{Hindley-Milner} elaboration in applicative style},
  booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'14)},
  month = sep,
  year = {2014},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf},
  off = {http://dx.doi.org/10.1145/2628136.2628145},
  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 = {Proceedings of the 2000 European Symposium on
                 Programming (ESOP'00)},
  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.ps.gz},
  off = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1782&spage=320},
  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},
  pdf = {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 = {Proceedings of the 38th {ACM} Symposium on Principles
                 of Programming Languages (POPL'11)},
  address = {Austin, Texas},
  month = jan,
  year = {2011},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork.pdf},
  longpdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-fork-x.pdf},
  off = {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},
  pdf = {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.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-popl04.pdf},
  booktitle = {Proceedings of the 31st {ACM} Symposium on Principles
                 of Programming Languages (POPL'04)},
  address = {Venice, Italy},
  month = jan,
  year = {2004},
  pages = {89--98},
  off = {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.ps.gz},
  pdf = {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 1995 (journée du pôle
                 Programmation Fonctionnelle)},
  month = nov,
  year = {1995},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-gdr-95.ps.gz},
  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.}
}
@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.ps.gz},
  pdf = {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},
  pdf = {http://hal.inria.fr/docs/00/07/24/75/PDF/RR-4150.pdf},
  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.ps.gz},
  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 = {Proceedings of the 1996 {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'96)},
  month = may,
  year = {1996},
  pages = {122--133},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp96.ps.gz},
  off = {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 = {Proceedings of the third {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'98)},
  month = sep,
  year = {1998},
  pages = {228--238},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp98.ps.gz},
  off = {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.ps.gz},
  long = {http://gallium.inria.fr/~fpottier/publis/fpottier-lics03-long.ps.gz},
  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 = {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.}
}
@misc{pottier-menhir-software,
  author = {François Pottier and Yann Régis-Gianas},
  title = {Menhir},
  soft = {http://gallium.inria.fr/~fpottier/menhir/},
  month = dec,
  year = {2005}
}
@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.ps.gz},
  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},
  pdf = {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.ps.gz},
  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 = {Proceedings of the 2013 {ACM} {SIGPLAN} International
                 Conference on Functional Programming (ICFP'13)},
  month = sep,
  year = {2013},
  pages = {173--184},
  pdf = {http://gallium.inria.fr/~fpottier/publis/pottier-protzenko-mezzo.pdf},
  longpdf = {http://gallium.inria.fr/~fpottier/publis/mezzo-icfp2013-long.pdf},
  off = {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-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)},
  address = {Wroclaw, Poland},
  pages = {356--365},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml.pdf},
  long = {http://gallium.inria.fr/~fpottier/publis/fpottier-pure-freshml-long.ps.gz},
  longpdf = {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
                 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.}
}
@inproceedings{pottier-regis-gianas-06,
  author = {François Pottier and Yann Régis-Gianas},
  title = {Stratified type inference for generalized algebraic
                 data types},
  booktitle = {Proceedings of the 33rd {ACM} Symposium on Principles
                 of Programming Languages (POPL'06)},
  address = {Charleston, South Carolina},
  month = jan,
  year = {2006},
  pages = {232--244},
  url = {http://gallium.inria.fr/~fpottier/publis/pottier-regis-gianas-popl06.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/pottier-regis-gianas-popl06.pdf},
  off = {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.ps.gz},
  pdf = {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},
  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},
  pdf = {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 = {Proceedings of the 29th {ACM} Symposium on Principles
                 of Programming Languages (POPL'02)},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-popl02.ps.gz},
  long = {http://gallium.inria.fr/~fpottier/publis/fpottier-simonet-popl02-long.ps.gz},
  address = {Portland, Oregon},
  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://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.ps.gz},
  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://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 = {Proceedings of the 10th European Symposium on
                 Programming (ESOP'01)},
  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.ps.gz},
  off = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2028&spage=30},
  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.ps.gz},
  off = {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
                 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 \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},
  pdf = {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.}
}
@misc{pottier-wallace,
  author = {François Pottier},
  title = {\texttt{Wallace}: an efficient implementation of type
                 inference with subtyping},
  soft = {http://gallium.inria.fr/~fpottier/wallace/},
  month = feb,
  year = {2000}
}
@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},
  pdf = {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
                 our library is safe, and to obtain theorems for free
                 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 = {Proceedings of the fifteenth {ACM} {SIGPLAN}
                 International Conference on Functional Programming
                 (ICFP 2010)},
  pages = {217--228},
  month = sep,
  year = {2010},
  off = {http://doi.acm.org/10.1145/1863543.1863575},
  pdf = {http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-fresh-look.pdf},
  longpdf = {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 = {Proceedings of the Ninth International Conference on
                 Mathematics of Program Construction (MPC'08)},
  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.ps.gz},
  pdf = {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 = {Proceedings of the 13th International Conference on
                 Foundations of Software Science and Computational
                 Structures (FOSSACS 2010)},
  month = mar,
  year = {2010},
  pages = {2--17},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6014},
  editor = {C.-H. L. Ong},
  pdf = {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},
  pdf = {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.ps.gz},
  pdf = {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.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.pdf},
  off = {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},
  address = {Dagstuhl, Germany},
  url = {http://gallium.inria.fr/~fpottier/publis/skalka-fpottier-tip-02.ps.gz},
  booktitle = {Proceedings of the Workshop on Types in Programming
                 (TIP'02)},
  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.96.