@phdthesis{regis-gianas-07,
author = {Yann Régis-Gianas and François Pottier},
title = {Des types aux assertions logiques~: Preuve automatique ou assistée de propriétée sur les programmes fonctionnels},
school = {Université Paris 7},
address = {},
month = {Novembre},
year = {2007}
}
@inproceedings{regis-gianas-pottier-08,
author = {Yann Régis-Gianas and François Pottier},
title = {A {Hoare} Logic for Call-by-Value Functional
Programs},
booktitle = {Proceedings of the Ninth International Conference on
Mathematics of Program Construction (MPC'08)},
month = jul,
year = {2008},
url = {http://cristal.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.ps.gz},
pdf = {http://cristal.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{pottier-regis-gianas-typed-lr,
author = {François Pottier and Yann {Régis-Gianas}},
title = {Towards efficient, typed {LR} parsers},
url = {http://cristal.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.ps.gz},
pdf = {http://cristal.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.}
}
@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://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-popl06.ps.gz},
pdf = {http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-popl06.pdf},
off = {http://doi.acm.org/10.1145/1111037.1111058},
abstract = {We offer a solution to the type inference problem for
an extension of Hindley and Milner's type system with
generalized algebraic data types. Our approach is in
two strata. The bottom stratum is a core language that
marries type inference in the style of Hindley and
Milner with type checking for generalized algebraic
data types. This results in an extremely simple
specification, where case constructs must carry an
explicit type annotation and type conversions must be
made explicit. The top stratum consists of (two
variants of) an independent shape inference algorithm.
This algorithm accepts a source term that contains some
explicit type information, propagates this information
in a local, predictable way, and produces a new source
term that carries more explicit type information. It
can be viewed as a preprocessor that helps produce some
of the type annotations required by the bottom stratum.
It is proven sound in the sense that it never inserts
annotations that could contradict the type derivation
that the programmer has in mind.}
}
This file was generated by bibtex2html 1.92.