[1] 
Armaël Guéneau, Arthur Charguéraud, and François Pottier.
A fistful of dollars: Formalizing
asymptotic complexity claims via deductive program verification.
In Amal Ahmed, editor, Proceedings of the European Symposium on
Programming (ESOP 2018), Lecture Notes in Computer Science. Springer, April
2018.
[ bib 
PDF ]
We present a framework for simultaneously verifying the functional correctness and the worstcase asymptotic time complexity of higherorder 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.

[2] 
Arthur Charguéraud and François Pottier.
Verifying the correctness and amortized
complexity of a unionfind implementation in separation logic with time
credits.
Journal of Automated Reasoning, September 2017.
[ bib 
Software 
PDF 
At publisher's ]
UnionFind 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 UnionFind 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 metatheoretical foundations of our approach, we define a Separation Logic with time credits for an untyped callbyvalue lambdacalculus, and formally verify its soundness.

[3] 
François Pottier.
Visitors unchained.
In Proceedings of the 2017 ACM SIGPLAN International
Conference on Functional Programming (ICFP 2017), September 2017.
[ bib 
DOI 
PDF ]
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 objectoriented features. We use visitor classes as partial, composable descriptions of the operations that we wish to perform on abstract syntax trees. We introduce visitors, a simple typedirected facility for generating visitor classes that have no knowledge of binding. Separately, we present alphaLib, a library of small handwritten 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.

[4]  JacquesHenri Jourdan and François Pottier. A simple, possibly correct LR parser for C11. ACM Transactions on Programming Languages and Systems, 39(4):14:114:36, August 2017. [ bib  Software  PDF  At publisher's ] 
[5]  François Pottier. Revisiting the CPS transformation and its implementation. In submission, July 2017. [ bib  PDF ] 
[6] 
Arthur Charguéraud and François Pottier.
Temporary readonly permissions for
separation logic.
In Hongseok Yang, editor, Proceedings of the European Symposium
on Programming (ESOP 2017), volume 10201 of Lecture Notes in Computer
Science, pages 260286. Springer, April 2017.
[ bib 
Software 
PDF ]
We present an extension of Separation Logic with a general mechanism for temporarily converting any assertion (or “permission”) to a readonly form. No accounting is required: our readonly permissions can be freely duplicated and discarded. We argue that, in circumstances where mutable data structures are temporarily accessed only for reading, our readonly permissions enable more concise specifications and proofs. The metatheory of our proposal is verified in Coq.

[7] 
François Pottier.
Verifying a hash table and its iterators
in higherorder separation logic.
In Proceedings of the 6th ACM SIGPLAN Conference on Certified
Programs and Proofs (CPP 2017), pages 316, January 2017.
[ bib 
DOI 
Software 
PDF 
At publisher's ]
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 higherorder 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.

[8] 
Thibaut Balabonski, François Pottier, and Jonathan Protzenko.
The design and formalization of Mezzo, a
permissionbased programming language.
ACM Transactions on Programming Languages and Systems,
38(4):14:114:94, August 2016.
[ bib 
DOI 
Software 
PDF 
At publisher's ]
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 λ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 welltyped programs do not go wrong and are datarace free. Our definitions and proofs are machinechecked.

[9] 
François Pottier.
Reachability and error diagnosis in
LR(1) parsers.
In Proceedings of the 25th International Conference on Compiler
Construction (CC 2016), pages 8898, March 2016.
[ bib 
DOI 
PDF 
At publisher's ]
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.

[10] 
François Pottier.
Reachability and error diagnosis in
LR(1) automata.
In Journées Francophones des Langages Applicatifs (JFLA),
January 2016.
[ bib 
PDF 
At publisher's ]
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.

[11] 
Arthur Charguéraud and François Pottier.
Machinechecked verification of the
correctness and amortized complexity of an efficient unionfind
implementation.
In Proceedings of the 6th Conference on Interactive Theorem
Proving (ITP 2015), volume 9236, pages 137153, August 2015.
[ bib 
Software 
PDF 
At publisher's ]
UnionFind 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. Moreover, we implement UnionFind 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.

[12] 
François Pottier and Jonathan Protzenko.
A few lessons from the Mezzo project.
In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S.
Lerner, and Greg Morrisett, editors, Summit oN Advances in Programming
Languages (SNAPL), volume 32 of Leibniz International Proceedings in
Informatics, pages 221237. Schloss DagstuhlLeibnizZentrum für
Informatik, May 2015.
[ bib 
PDF 
At publisher's ]
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.

[13] 
François Pottier.
Depthfirst search and strong connectivity
in Coq.
In Journées Francophones des Langages Applicatifs (JFLA 2015),
January 2015.
[ bib 
Software 
PDF 
At publisher's ]
Using Coq, we mechanize Wegener's proof of Kosaraju's lineartime algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depthfirst search algorithm.

[14] 
François Pottier.
HindleyMilner elaboration in
applicative style.
In Proceedings of the 2014 ACM SIGPLAN International
Conference on Functional Programming (ICFP 2014), September 2014.
[ bib 
DOI 
Software 
PDF 
At publisher's ]
Type inferencethe problem of determining whether a program is welltypedis wellunderstood. In contrast, elaborationthe task of constructing an explicitlytyped representation of the programseems to have received relatively little attention, even though, in a nonlocal type inference system, it is nontrivial. We show that the constraintbased presentation of HindleyMilner 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.

[15] 
Thibaut Balabonski, François Pottier, and Jonathan Protzenko.
Type soundness and race freedom for
Mezzo.
In Proceedings of the 12th International Symposium on Functional
and Logic Programming (FLOPS 2014), volume 8475, pages 253269, June 2014.
[ bib 
PDF 
At publisher's ]
The programming language Mezzo is equipped with a rich type system that controls aliasing and access to mutable memory. We incorporate sharedmemory concurrency into Mezzo and present a modular formalization of Mezzo's core type system, in the form of a concurrent lambdacalculus, which we extend with references and locks. We prove that welltyped programs do not go wrong and are datarace free. Our definitions and proofs are machinechecked.

[16] 
François Pottier and Jonathan Protzenko.
Programming with permissions in Mezzo.
In Proceedings of the 2013 ACM SIGPLAN International
Conference on Functional Programming (ICFP 2013), pages 173184, September
2013.
[ bib 
DOI 
PDF 
Long PDF 
At publisher's ]
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 reuse, 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”.

[17] 
Armaël Guéneau, François Pottier, and Jonathan Protzenko.
The ins and outs of iteration in
Mezzo.
Talk proposal for HOPE 2013, July 2013.
[ bib 
PDF ]
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.

[18]  Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, and Hongseok Yang. A stepindexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1):154, February 2013. [ bib  PDF  At publisher's ] 
[19] 
François Pottier.
Syntactic soundness proof of a
typeandcapability system with hidden state.
Journal of Functional Programming, 23(1):38144, January 2013.
[ bib 
PDF 
At publisher's ]
This paper presents a formal definition and machinechecked soundness proof for a very expressive typeandcapability system, that is, a lowlevel type system that keeps precise track of ownership and side effects.

[20] 
Nicolas Pouillard and François Pottier.
A unified treatment of syntax with
binders.
Journal of Functional Programming, 22(45):614704, September
2012.
[ bib 
PDF 
At publisher's ]
Atoms and de Bruijn indices are two wellknown 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.

[21] 
JacquesHenri Jourdan, François Pottier, and Xavier Leroy.
Validating LR(1) parsers.
In Proceedings of the 21st European Symposium on Programming
(ESOP 2012), volume 7211 of Lecture Notes in Computer Science, pages
397416. Springer, March 2012.
[ bib 
PDF 
At publisher's ]
An LR(1) parser is a finitestate 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 contextfree grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other highassurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formallyverified parser for the C99 language.

[22] 
Alexandre Pilkiewicz and François Pottier.
The essence of monotonic state.
In Proceedings of the Sixth ACM SIGPLAN Workshop on Types in
Language Design and Implementation (TLDI 2011), Austin, Texas, January 2011.
[ bib 
DOI 
PDF 
At publisher's ]
We extend a static typeandcapability 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 nontrivial 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”.

[23] 
François Pottier.
A typed storepassing translation for
general references.
In Proceedings of the 38th ACM Symposium on Principles of
Programming Languages (POPL 2011), Austin, Texas, January 2011.
Supplementary material.
[ bib 
DOI 
PDF 
Long PDF 
At publisher's ]
We present a storepassing translation of System F with general references into an extension of System F_{ω} with certain wellbehaved recursive kinds. This seems to be the first typepreserving storepassing translation for general references. It can be viewed as a purely syntactic account of a possible worlds model.

[24] 
Nicolas Pouillard and François Pottier.
A fresh look at programming with names and
binders.
In Proceedings of the fifteenth ACM SIGPLAN International
Conference on Functional Programming (ICFP 2010), pages 217228, September
2010.
[ bib 
DOI 
PDF 
Long PDF 
At publisher's ]
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.

[25] 
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, and
Bernhard Reus.
A semantic foundation for hidden state.
In C.H. L. Ong, editor, Proceedings of the 13th International
Conference on Foundations of Software Science and Computational Structures
(FOSSACS 2010), volume 6014 of Lecture Notes in Computer Science,
pages 217. Springer, March 2010.
[ bib 
PDF 
At publisher's ]
We present the first complete soundness proof of the antiframe rule, a recently proposed proof rule for capturing information hiding in the presence of higherorder store. Our proof involves solving a nontrivial 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.

[26] 
François Pottier.
Lazy least fixed points in ML.
Unpublished, December 2009.
[ bib 
PDF ]
This “not quite functional” pearl describes an algorithm for computing the least solution of a system of monotone equations. It is implemented in imperative 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.

[27] 
François Pottier.
Three comments on the antiframe rule.
Unpublished, July 2009.
[ bib 
PDF ]
This informal note presents three comments about the antiframe rule, which respectively regard: its interaction with polymorphism; its interaction with the higherorder frame axiom; and a problematic lack of modularity.

[28] 
François Pottier.
Generalizing the higherorder frame and
antiframe rules.
Unpublished, July 2009.
[ bib 
PDF ]
This informal note presents generalized versions of the higherorder frame and antiframe rules. The main insights reside in two successive generalizations of the “tensor” operator . In the first step, a form of “local invariant”, which allows implicit reasoning about “wellbracketed state changes”, is introduced. In the second step, a form of “local monotonicity” is added.

[29] 
Arthur Charguéraud and François Pottier.
Functional translation of a calculus of
capabilities.
In Proceedings of the 2008 ACM SIGPLAN International
Conference on Functional Programming (ICFP'08), pages 213224, September
2008.
[ bib 
DOI 
PDF 
PostScript 
At publisher's ]
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 highlevel calculus with higherorder 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.

[30] 
Yann RégisGianas and François Pottier.
A Hoare logic for callbyvalue
functional programs.
In Proceedings of the Ninth International Conference on
Mathematics of Program Construction (MPC 2008), volume 5133 of Lecture
Notes in Computer Science, pages 305335. Springer, July 2008.
[ bib 
PDF 
PostScript 
At publisher's ]
We present a Hoare logic for a callbyvalue programming language equipped with recursive, higherorder 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, higherorder logic, are discharged using offtheshelf 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.

[31] 
François Pottier.
Hiding local state in direct style: a
higherorder antiframe rule.
In TwentyThird Annual IEEE Symposium on Logic In Computer
Science (LICS'08), pages 331340, Pittsburgh, Pennsylvania, June 2008.
[ bib 
PDF 
At publisher's ]
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 higherorder frame rule. I point out that this approach to hiding local state imposes continuationpassing style, which is impractical. Instead, I introduce a higherorder antiframe 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 MLlike programming language, and prove type soundness via a syntactic argument. Several applications illustrate the expressive power of the new rule.

[32] 
François Pottier.
Static name control for FreshML.
In TwentySecond Annual IEEE Symposium on Logic In Computer
Science (LICS'07), pages 356365, Wroclaw, Poland, July 2007.
[ bib 
PDF 
PostScript 
Long PDF 
Long PostScript 
At publisher's ]
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 userprovided 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 nontrivial syntaxmanipulating algorithms.

[33] 
Vincent Simonet and François Pottier.
A constraintbased approach to guarded
algebraic data types.
ACM Transactions on Programming Languages and Systems, 29(1),
January 2007.
[ bib 
DOI 
PDF 
PostScript 
At publisher's ]
We study HMG(X), an extension of the constraintbased 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, (firstclass) 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.

[34] 
François Pottier.
An overview of Cαml.
In ACM Workshop on ML, volume 148(2) of Electronic Notes
in Theoretical Computer Science, pages 2752, March 2006.
[ bib 
PDF 
PostScript 
At publisher's ]
Cαml is a tool that turns a socalled “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αml is meant to help writers of interpreters, compilers, or other programsthatmanipulateprograms deal with αconversion in a safe and concise style. This paper presents an overview of Cαml's binding specification language and of the code that Cαml produces.

[35] 
François Pottier and Nadji Gauthier.
Polymorphic typed defunctionalization and
concretization.
HigherOrder and Symbolic Computation, 19:125162, March 2006.
[ bib 
PDF 
PostScript 
At publisher's ]
Defunctionalization is a program transformation that eliminates functions as firstclass values. We show that defunctionalization can be viewed as a typepreserving transformation of an extension of with guarded algebraic data types into itself. We also suggest that defunctionalization is an instance of concretization, a more general technique that allows eliminating constructs other than functions. We illustrate this point by presenting two new typepreserving transformations that can be viewed as instances of concretization. One eliminates Rémystyle polymorphic records; the other eliminates the dictionary records introduced by the standard compilation scheme for Haskell's type classes.

[36] 
François Pottier and Yann RégisGianas.
Towards efficient, typed LR parsers.
In ACM Workshop on ML, volume 148(2) of Electronic Notes
in Theoretical Computer Science, pages 155180, March 2006.
[ bib 
PDF 
PostScript 
At publisher's ]
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 welltyped (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.

[37] 
François Pottier and Yann RégisGianas.
Stratified type inference for generalized
algebraic data types.
In Proceedings of the 33rd ACM Symposium on Principles of
Programming Languages (POPL'06), pages 232244, Charleston, South Carolina,
January 2006.
[ bib 
DOI 
PDF 
PostScript 
At publisher's ]
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.

[38]  François Pottier and Yann RégisGianas. Menhir, December 2005. [ bib  Software ] 
[39]  François Pottier. A modern eye on ML type inference: old techniques and recent developments. Lecture notes for the APPSEM Summer School, September 2005. [ bib  PDF  PostScript ] 
[40]  François Pottier. Cαml, June 2005. [ bib  Software ] 
[41] 
Roberto Di Cosmo, François Pottier, and Didier Rémy.
Subtyping recursive types modulo
associative commutative products.
In Seventh International Conference on Typed Lambda Calculi and
Applications (TLCA'05), volume 3461 of Lecture Notes in Computer
Science, pages 179193, Nara, Japan, April 2005. Springer.
[ bib 
PDF 
PostScript 
Long PDF 
Long PostScript 
At publisher's ]
This work sets the formal bases for building tools that help retrieve classes in objectoriented 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 productsthat is, subtyping modulo a restricted form of type isomorphismsas 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.

[42] 
François Pottier, Christian Skalka, and Scott Smith.
A systematic approach to static access
control.
ACM Transactions on Programming Languages and Systems,
27(2):344382, March 2005.
[ bib 
DOI 
PostScript 
At publisher's ]
The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the socalled stack inspection process. While the architecture has several appealing features, access control checks are all implemented via dynamic method calls. This is a highly nondeclarative form of specification which is hard to read, and which leads to additional runtime 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 securitypassing style translation, proposed by Wallach, Appel and Felten as a dynamic implementation technique, also gives rise to static securityaware 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 unificationbased type systems.

[43]  François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389489. MIT Press, 2005. A draft extended version is also available. [ bib  PDF  At publisher's ] 
[44] 
Vincent Simonet and François Pottier.
Constraintbased type inference for
guarded algebraic data types.
Research Report 5462, INRIA, January 2005.
[ bib 
PDF 
PostScript 
At publisher's ]
Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and firstclass phantom types, and are closely related to 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.

[45]  François Pottier. Types et contraintes. Mémoire d'habilitation à diriger des recherches, Université Paris 7, December 2004. [ bib  PDF  PostScript ] 
[46] 
Nadji Gauthier and François Pottier.
Numbering matters: Firstorder canonical
forms for secondorder recursive types.
In Proceedings of the 2004 ACM SIGPLAN International
Conference on Functional Programming (ICFP'04), pages 150161, September
2004.
[ bib 
DOI 
PDF 
PostScript 
At publisher's ]
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(nlogn), 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(nlog n), a new result. To achieve this bound, we associate, with every F_{mu} type, a firstorder canonical form, which may be computed in time O(nlogn). By exploiting this notion, we reduce all three problems to equality and unification of firstorder recursive terms, for which efficient algorithms are known.

[47] 
François Pottier and Nadji Gauthier.
Polymorphic typed defunctionalization.
In Proceedings of the 31st ACM Symposium on Principles of
Programming Languages (POPL'04), pages 8998, Venice, Italy, January 2004.
Superseded by [35].
[ bib 
DOI 
PDF 
PostScript 
At publisher's ]
Defunctionalization is a program transformation that aims to turn a higherorder functional program into a firstorder one, that is, to eliminate the use of functions as firstclass values. Its purpose is thus identical to that of closure conversion. It differs from closure conversion, however, by storing a tag, instead of a code pointer, within every closure. Defunctionalization has been used both as a reasoning tool and as a compilation technique.

[48] 
JeanChristophe Filliâtre and François Pottier.
Producing all ideals of a forest,
functionally.
Journal of Functional Programming, 13(5):945956, September
2003.
[ bib 
PostScript 
At publisher's ]
We present functional implementations of Koda and Ruskey's algorithm for generating all ideals of a forest poset as a Gray code. Using a continuationbased approach, we give an extremely concise formulation of the algorithm's core. Then, in a number of steps, we derive a firstorder version whose efficiency is comparable to that of a C implementation given by Knuth.

[49] 
François Pottier.
A constraintbased presentation and
generalization of rows.
In Eighteenth Annual IEEE Symposium on Logic In Computer
Science (LICS'03), pages 331340, Ottawa, Canada, June 2003.
[ bib 
PostScript 
Long PostScript 
At publisher's ]
We study the combination of possibly conditional nonstructural subtyping constraints with rows. We give a new presentation of rows, where row terms disappear; instead, we annotate constraints with 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^{3}mlogm), 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.

[50] 
François Pottier and Vincent Simonet.
Information flow inference for ML.
ACM Transactions on Programming Languages and Systems,
25(1):117158, January 2003.
[ bib 
DOI 
PostScript 
At publisher's ]
This paper presents a typebased information flow analysis for a callbyvalue lambdacalculus equipped with references, exceptions and letpolymorphism, which we refer to as Core ML. The type system is constraintbased and has decidable type inference. Its noninterference proof is reasonably lightweight, 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, noninterference is reduced to subject reduction for a nonstandard language extension. Lastly, a semisyntactic approach to type soundness allows dealing with constraintbased polymorphism separately.

[51] 
Christian Skalka and François Pottier.
Syntactic type soundness for HM(X).
In Proceedings of the Workshop on Types in Programming (TIP
2002), volume 75 of Electronic Notes in Theoretical Computer Science,
Dagstuhl, Germany, July 2002.
[ bib 
PostScript ]
The HM(X) framework is a constraintbased type framework with builtin letpolymorphism. 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.

[52] 
François Pottier.
A simple view of typesecure information
flow in the πcalculus.
In Proceedings of the 15th IEEE Computer Security Foundations
Workshop, pages 320330, Cape Breton, Nova Scotia, June 2002.
[ bib 
PostScript 
Long PostScript 
At publisher's ]
One way of enforcing an information flow control policy is to use a static type system capable of guaranteeing a 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.

[53] 
François Pottier and Vincent Simonet.
Information flow inference for ML.
In Proceedings of the 29th ACM Symposium on Principles of
Programming Languages (POPL'02), pages 319330, Portland, Oregon, January
2002.
Superseded by [50].
[ bib 
DOI 
PostScript 
Long PostScript 
At publisher's ]
This paper presents a typebased information flow analysis for a callbyvalue lambdacalculus equipped with references, exceptions and letpolymorphism, which we refer to as Core ML. The type system is constraintbased and has decidable type inference. Its noninterference proof is reasonably lightweight, 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, noninterference is reduced to subject reduction for a nonstandard language extension. Lastly, a semisyntactic approach to type soundness allows dealing with constraintbased polymorphism separately.

[54] 
François Pottier.
Simplifying subtyping constraints: a
theory.
Information & Computation, 170(2):153183, November 2001.
[ bib 
PostScript 
At publisher's ]
This paper offers a theoretical study of constraint simplification, a fundamental issue for the designer of a practical type inference system with subtyping.

[55] 
Sylvain Conchon and François Pottier.
JOIN(X): Constraintbased type
inference for the joincalculus.
In David Sands, editor, Proceedings of the 10th European
Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in
Computer Science, pages 221236. Springer, April 2001.
[ bib 
PostScript 
Long PostScript 
At publisher's ]
We present a generic constraintbased type system for the joincalculus. 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 value restriction.

[56] 
François Pottier, Christian Skalka, and Scott Smith.
A systematic approach to static access
control.
In David Sands, editor, Proceedings of the 10th European
Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in
Computer Science, pages 3045. Springer, April 2001.
Superseded by [42].
[ bib 
PostScript 
At publisher's ]
The Java JDK 1.2 Security Architecture includes a dynamic mechanism for enforcing access control checks, socalled 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 securitypassing style translation, proposed by Wallach and Felten as a dynamic implementation technique, also gives rise to static securityaware 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 unificationbased 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.

[57] 
François Pottier.
A semisyntactic soundness proof for
HM(X).
Research Report 4150, INRIA, March 2001.
[ bib 
PDF ]
This document gives a soundness proof for the generic constraintbased type inference framework HM(X). Our proof is semisyntactic. It consists of two steps. The first step is to define a ground type system, where polymorphism is 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).

[58] 
François Pottier.
A versatile constraintbased type
inference system.
Nordic Journal of Computing, 7(4):312347, November 2000.
[ bib 
PostScript ]
The combination of subtyping, conditional constraints and rows yields a powerful constraintbased type inference system. We illustrate this claim by proposing solutions to three delicate type inference problems: “accurate” pattern matchings, record concatenation, and firstclass 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.

[59] 
François Pottier and Sylvain Conchon.
Information flow inference for free.
In Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP'00), pages 4657, Montréal,
Canada, September 2000.
[ bib 
DOI 
PostScript 
At publisher's ]
This paper shows how to systematically extend an arbitrary type system with dependency information, and how the new system's soundness and noninterference 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.

[60] 
François Pottier.
A 3part type inference engine.
In Gert Smolka, editor, Proceedings of the 2000 European
Symposium on Programming (ESOP'00), volume 1782 of Lecture Notes in
Computer Science, pages 320335. Springer, March 2000.
Superseded by [58].
[ bib 
PostScript 
At publisher's ]
Extending a subtypingconstraintbased type inference framework with conditional constraints and 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.

[61]  François Pottier. Wallace: an efficient implementation of type inference with subtyping, February 2000. [ bib  Software ] 
[62] 
François Pottier.
A framework for type inference with
subtyping.
In Proceedings of the third ACM SIGPLAN International
Conference on Functional Programming (ICFP 1998), pages 228238, September
1998.
[ bib 
DOI 
PostScript 
At publisher's ]
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.

[63] 
François Pottier.
Type inference in the presence of
subtyping: from theory to practice.
Research Report 3483, INRIA, September 1998.
[ bib 
PDF ]
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.

[64] 
François Pottier.
Synthèse de types en présence de
soustypage: de la théorie à la pratique.
PhD thesis, Université Paris 7, July 1998.
[ bib 
PostScript ]
D'un point de vue purement théorique, l'inférence de types pour un langage fonctionnel doté de polymorphisme paramétrique et de soustypage 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, cellesci 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é.

[65] 
François Pottier.
Simplifying subtyping constraints.
In Proceedings of the 1996 ACM SIGPLAN International
Conference on Functional Programming (ICFP 1996), pages 122133, May 1996.
[ bib 
DOI 
PostScript 
At publisher's ]
This paper studies type inference for a functional, MLstyle 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.

[66] 
François Pottier.
Type inference and simplification for
recursively constrained types.
In Actes du GDR Programmation 1995 (journée du pôle
Programmation Fonctionnelle), November 1995.
[ bib 
PostScript ]
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.

[67] 
François Pottier.
Implémentation d'un système de modules
évolué en CamlLight.
Research Report 2449, INRIA, January 1995.
[ bib 
PDF 
PostScript ]
Ce mémoire décrit la conception et l'implémentation d'un langage de modules évolué en CamlLight. 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.

[68] 
Michel Mauny and François Pottier.
An implementation of Caml Light with
existential types.
Technical Report 2183, INRIA, October 1993.
[ bib 
PDF 
PostScript ]
This work is based on a proposal by Läufer and Odersky. They show that it is possible to add existential types to an MLlike language without even modifying its syntax. ML's strong typing properties are of course retained. We implemented their proposal into CamlLight, thus making it possible to write realsized programs using existential types.

This file was generated by bibtex2html 1.98.