publications.bib

@MASTERSTHESIS{simonet-dea00,
  AUTHOR = {Vincent Simonet},
  TITLE = {Inférence de flots d'information pour {ML}},
  YEAR = {2001},
  MONTH = MAR,
  SCHOOL = {DEA «~Programmation~: Sémantique, Preuves, et Langages~»},
  NOTE = {In French},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-dea01.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-dea01.pdf}
}

@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)},
  PAGES = {319--330},
  ACM = {http://doi.acm.org/10.1145/503272.503302},
  PS = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-popl02.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-popl02.pdf},
  LONG-PS = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-popl02-long.ps.gz},
  LONG-PDF = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-popl02-long.pdf},
  ADDRESS = {Portland, Oregon},
  MONTH = JAN,
  YEAR = {2002},
  NOTE = {\copyright ACM},
  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.}
}

@INPROCEEDINGS{simonet-csfw-02,
  AUTHOR = {Vincent Simonet},
  TITLE = {Fine-grained Information Flow Analysis for a $\lambda$-calculus
           with Sum Types},
  BOOKTITLE = {Proceedings of the 15th {IEEE} 
               Computer Security Foundations Workshop (CSFW 15)},
  PAGES = {223--237},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-csfw-02.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-csfw-02.pdf},
  LONG-PS = {http://cristal.inria.fr/~simonet/publis/simonet-csfw-02-long.ps.gz},
  LONG-PDF = {http://cristal.inria.fr/~simonet/publis/simonet-csfw-02-long.pdf},
  ADDRESS = {Cape Breton, Nova Scotia (Canada)},
  MONTH = JUN,
  YEAR = {2002},
  NOTE = {\copyright IEEE},
  ABSTRACT = {This paper presents a new type system tracing
    information flow for a $\lambda$-calculus equipped with
    polymorphic ``let'' and with sums (a.k.a.\ union types or
    polymorphic variants).  The type system allows establishing (weak)
    non-interference properties.  Thanks to original forms of security
    annotations and constraints, it is more accurate than existing
    analyses.  Through a straightforward encoding into sums, this work
    also provides a new type-based information flow analysis for
    programming languages featuring exceptions.  From these systems,
    one may derive constraint-based formulations, in the style of
    HM(X), which have decidable type inference.}
}

@ARTICLE{pottier-simonet-toplas,
  AUTHOR = {François Pottier and Vincent Simonet},
  TITLE = {Information Flow Inference for {ML}},
  JOURNAL = {ACM Transactions on Programming Languages and Systems},
  VOLUME = {25},
  NUMBER = {1},
  MONTH = JAN,
  YEAR = 2003,
  PAGES = {117--158},
  ACM = {http://doi.acm.org/10.1145/596980.596983},
  PS = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-toplas.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/fpottier-simonet-toplas.pdf},
  NOTE = {\copyright ACM},
  ABSTRACT = {This paper presents a type-based information flow
    analysis for a call-by-value $\lambda$-calculus equip\-ped with
    references, exceptions and $let$-polymorphism, which we refer to
    as ML. The type system is constraint-based and has decidable type
    inference. Its noninterference proof is reasonably light-weight,
    thanks to the use of a number of orthogonal techniques. First, a
    syntactic segregation between \emph{values} and \emph{expressions}
    allows a lighter formulation of the type system. Second,
    noninterference is reduced to \emph{subject reduction} for a
    nonstandard language extension. Lastly, a \emph{semi-syntactic}
    approach to type soundness allows dealing with constraint-based
    polymorphism separately.}
}

@INPROCEEDINGS{simonet-appsem-03,
  AUTHOR = {Vincent Simonet},
  TITLE = {{Flow} {Caml} in a Nutshell},
  BOOKTITLE = {Proceedings of the first APPSEM-II workshop},
  PAGES = {152--165},
  EDITOR = {Graham Hutton},
  ADDRESS = {Nottingham, United Kingdom},
  MONTH = MAR,
  YEAR = 2003,
  ABSTRACT = {Flow Caml is an extension of the Objective Caml language
    with a type system tracing information flow.  It automatically
    checks information flow within Flow Caml programs, then translates
    them to regular Objective Caml code that can be compiled by the
    ordinary compiler to produce secure programs.  In this paper, we
    give a short overview of this system, from a practical viewpoint.}
}

@INPROCEEDINGS{simonet-icfp-03,
  AUTHOR = {Vincent Simonet},
  TITLE = {An Extension of {HM(X)} with Bounded Existential and
           Universal Data-Types},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-icfp03.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-icfp03.pdf},
  LONG-PS = {http://cristal.inria.fr/~simonet/publis/simonet-icfp03-full.ps.gz},
  LONG-PDF = {http://cristal.inria.fr/~simonet/publis/simonet-icfp03-full.pdf},
  ACM = {http://doi.acm.org/10.1145/944705.944710},
  MONTH = AUG,
  YEAR = 2003,
  BOOKTITLE = {Proceedings of the 8th ACM SIGPLAN International Conference on 
               Functional Programming (ICFP 2003)},
  PAGES = {39--50},
  ADDRESS = {Uppsala, Sweden},
  NOTE = {\copyright ACM},
  ABSTRACT = {We propose a conservative extension of HM(X), a generic
    constraint-based type inference framework, with bounded
    existential (a.k.a. abstract) and universal (a.k.a. polymorphic)
    data-types.  In the first part of the article, which remains
    abstract of the type and constraint language (i.e. the logic X),
    we introduce the type system, prove its safety and define a type
    inference algorithm which computes principal typing judgments.  In
    the second part, we propose a realistic constraint solving
    algorithm for the case of structural subtyping, which handles the
    non-standard construct of the constraint language generated by
    type inference: a form of bounded universal quantification.}
}

@INPROCEEDINGS{simonet-aplas-03,
  AUTHOR = {Vincent Simonet},
  TITLE = {Type inference with structural subtyping:
           A faithful formalization of an efficient constraint solver},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-aplas03.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-aplas03.pdf},
  LONG-PS = {http://cristal.inria.fr/~simonet/publis/simonet-aplas03-full.ps.gz},
  LONG-PDF = {http://cristal.inria.fr/~simonet/publis/simonet-aplas03-full.pdf},
  SPRINGER = {http://www.springerlink.com/link.asp?id=y21wma91n44y},
  MONTH = NOV,
  YEAR = {2003},
  BOOKTITLE = {Proceedings of the Asian Symposium on
               Programming Languages and Systems (APLAS'03)},
  EDITOR = {Atsushi Ohori},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {283--302},
  VOLUME = 2895,
  ADDRESS = {Beijing, China},
  NOTE = {\copyright Springer-Verlag},
  ABSTRACT = {We are interested in type inference in the presence of
    structural subtyping from a pragmatic perspective.  This work
    combines theoretical and practical contributions: first, it
    provides a faithful description of an efficient algorithm for
    solving and simplifying constraints; whose correctness is formally
    proved.  Besides, the framework has been implemented in Objective
    Caml, yielding a generic type inference engine.  Its efficiency is
    assessed by a complexity result and a series of experiments in
    realistic cases.}
}

@TECHREPORT{simonet-flowcaml-manual,
  AUTHOR = {Vincent Simonet},
  TITLE = {The {F}low {C}aml {S}ystem: documentation and user's manual},
  INSTITUTION = {Institut National de Recherche en Informatique et
                 en Automatique (INRIA)},
  NUMBER = {0282},
  TYPE = {Technical Report},
  HTML = {http://cristal.inria.fr/~simonet/soft/flowcaml/manual/},
  PS = {http://cristal.inria.fr/~simonet/soft/flowcaml/flowcaml-manual.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/soft/flowcaml/flowcaml-manual.pdf},
  INRIA = {http://www.inria.fr/rrrt/rt-0282.html},
  MONTH = JUL,
  YEAR = {2003},
  NOTE = {\copyright INRIA},
  ABSTRACT = {Flow Caml is an extension of the Objective Caml language
    with a type system tracing information flow.  Its purpose is
    basically to allow to write ``real'' programs and to automatically
    check that they obey some confidentiality or integrity policy.  In
    Flow Caml, standard ML types are annotated with security levels
    chosen in a user-definable lattice.  Each annotation gives an
    approximation of the information that the described expression may
    convey.  Because it has full type inference, the system verifies,
    without requiring source code annotations, that every information
    flow caused by the analyzed program is legal with regard to the
    security policy specified by the programmer.}
}

@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.},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-pottier-hmg.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-pottier-hmg.pdf},
  INRIA = {http://www.inria.fr/rrrt/rr-5462.html}
}

@ARTICLE{simonet-pottier-hmg-toplas,
  AUTHOR = {Vincent Simonet and François Pottier},
  TITLE = {A Constraint-Based Approach to Guarded Algebraic Data
                 Types},
  MONTH = DEC,
  YEAR = {2005},
  JOURNAL = {ACM Transactions on Programming Languages and
                 Systems},
  NOTE = {To appear},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-pottier-hmg-toplas.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-pottier-hmg-toplas.pdf},
  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.}
}

@PHDTHESIS{simonet-these,
  AUTHOR = {Vincent Simonet},
  TITLE = {Inférence de flots d'information pour {ML}: 
           formalisation et implantation},
  PS = {http://cristal.inria.fr/~simonet/publis/simonet-these.ps.gz},
  PDF = {http://cristal.inria.fr/~simonet/publis/simonet-these.pdf},
  MONTH = MAR,
  YEAR = {2004},
  SCHOOL = {Université Paris 7},
  ABSTRACT = {This thesis describes the conception of an information flow
    analyser for a language of the ML family, from its theoretical
    foundation to the practical issues.  The first part of the
    dissertation presents the tool that was implemented, Flow Caml,
    and illustrates its use on concrete example.  The second part
    gives a formalization of the type system featured by Flow Caml,
    together with a proof of its correctness.  This is the first type
    system for information flow analysis in a realistic programming
    language that has been formally proved.  Lastly, the third part is
    devoted to the formalization and the proof of an efficient
    algorithm for type inference in the presence of structural
    subtyping and polymorphism.  An instance of this algorithm is used
    to synthesize types in Flow Caml.}
}