@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.} }

@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}, pdf = {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 type system that controls aliasing and access to 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 = {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://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 = {Proceedings of the 6th Conference on Interactive Theorem Proving (ITP 2015)}, month = aug, year = {2015}, volume = {9236}, series = lncs, publisher = springer, pages = {137--153}, pdf = {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 = {Proceedings of the European Symposium on Programming (ESOP 2017)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10201}, editor = {Hongseok Yang}, month = apr, year = {2017}, pages = {260--286}, pdf = {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 temporarily accessed only for reading, our read-only 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}, pdf = {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 = {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.} }

@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://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-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 = {Proceedings of the European Symposium on Programming (ESOP 2018)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10801}, pages = {533--560}, editor = {Amal Ahmed}, month = apr, year = {2018}, pdf = {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}, 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.} }

@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}, pdf = {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}, 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.} }

@unpublished{mevel-jourdan-pottier-18, author = {Glen Mével and Jacques-Henri Jourdan and François Pottier}, title = {Time credits and time receipts in {Iris}}, note = {Submitted}, month = jul, year = {2018}, pdf = {http://gallium.inria.fr/~fpottier/publis/mevel-jourdan-pottier-time-in-iris-2018.pdf} }

@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 2011)}, month = jan, year = {2011}, address = {Austin, Texas}, pdf = {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}, 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-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} }

@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://dl.acm.org/authorize?N05385}, doi = {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-cpp-17, author = {François Pottier}, title = {Verifying a hash table and its iterators in higher-order separation logic}, booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)}, month = jan, year = {2017}, pages = {3--16}, pdf = {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}, pdf = {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.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.} }

@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 2015)}, month = jan, year = {2015}, pdf = {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.} }

@inproceedings{pottier-elaboration-14, author = {François Pottier}, title = {{Hindley-Milner} elaboration in applicative style}, booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP 2014)}, month = sep, year = {2014}, pdf = {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 = {http://gallium.inria.fr/~fpottier/inferno/inferno.tar.gz}, 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 2011)}, 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://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}, 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://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.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 1996)}, month = may, year = {1996}, pages = {122--133}, url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp96.ps.gz}, 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 = {Proceedings of the third {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP 1998)}, month = sep, year = {1998}, pages = {228--238}, url = {http://gallium.inria.fr/~fpottier/publis/fpottier-icfp98.ps.gz}, 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.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 2013)}, 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://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}, pdf = {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 = {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-reachability-cc-2016, author = {François Pottier}, title = {Reachability and error diagnosis in {LR}(1) parsers}, booktitle = {Proceedings of the 25th International Conference on Compiler Construction (CC 2016)}, month = mar, year = {2016}, pages = {88--98}, pdf = {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}, pdf = {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.} }

@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://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.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://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.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://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 = {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://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 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.} }

@inproceedings{pottier-visitors-17, author = {François Pottier}, title = {Visitors Unchained}, booktitle = {Proceedings of the 2017 {ACM} {SIGPLAN} International Conference on Functional Programming (ICFP 2017)}, month = sep, year = {2017}, pdf = {http://gallium.inria.fr/~fpottier/publis/fpottier-visitors-unchained.pdf}, doi = {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.} }

@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://dl.acm.org/authorize?N05375}, doi = {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 2008)}, 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://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}, 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 2002)}, 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.98.*