@article{BERTOT:GUILHOT:MAHBOUBI:2011,
hal_id = {inria-00503017},
url = {http://hal.archives-ouvertes.fr/inria-00503017/},
title = { {A} formal study of {B}ernstein coefficients and polynomials},
author = {{B}ertot, {Y}ves and {G}uilhot, {F}r{\'e}derique and {M}ahboubi, {A}ssia},
journal = {{M}athematical {S}tructures in {C}omputer {S}cience},
volume = 21,
number = 4,
pages = {731--762},
language = {{E}nglish},
year = {2011},
doi = {10.1017/S0960129511000090},
url = {http://dx.doi.org/10.1017/S0960129511000090},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} - {T}ypi{C}al - {INRIA} {S}aclay - {I}le de {F}rance - {INRIA} - {CNRS} : {UMR} - {P}olytechnique - {X} - {L}aboratoire d'informatique de l'{\'e}cole polytechnique - {LIX} - {CNRS} : {UMR}7161 - {P}olytechnique - {X} }
}
@inproceedings{Minh_UITP,
author = {Tuan-Minh Pham and Yves Bertot},
title = {A combination of a dynamic geometry software with a proof assistant for interactive formal proofs},
booktitle = {UITP'10, User-Interfaces for Theorem Provers},
mon = jul,
year = {2010}
}
@inproceedings{DBLP:conf/sac/Pham10,
author = {Tuan Minh Pham},
title = {Similar triangles and orientation in plane elementary geometry
for Coq-based proofs},
year = {2010},
pages = {1268-1269},
ee = {http://doi.acm.org/10.1145/1774088.1774358},
editor = {Sung Y. Shin and
Sascha Ossowski and
Michael Schumacher and
Mathew J. Palakal and
Chih-Cheng Hung},
booktitle = {Proceedings of the 2010 ACM Symposium on Applied Computing
(SAC), Sierre, Switzerland, March 22-26, 2010},
publisher = {ACM},
month = mar,
year = {2010},
isbn = {978-1-60558-639-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{ARMAND:2010:INRIA-00502496:1,
hal_id = {inria-00502496},
url = {http://hal.archives-ouvertes.fr/inria-00502496/en/},
title = { {E}xtending {C}oq with {I}mperative {F}eatures and its {A}pplication to {SAT} {V}erification},
author = {{A}rmand, {M}icha{\"e}l and {G}r{\'e}goire, {B}enjamin and {S}piwack, {A}rnaud and {T}h{\'e}ry, {L}aurent},
language = {{A}nglais},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} - {L}aboratoire d'informatique de l'{\'e}cole polytechnique - {LIX} - {CNRS} : {UMR}7161 - {P}olytechnique - {X} - {T}ypi{C}al - {INRIA} {S}aclay - {I}le de {F}rance - {INRIA} - {CNRS} : {UMR} - {P}olytechnique - {X} },
booktitle = {{I}nteractive {T}heorem {P}roving },
address = {{E}dinburgh {R}oyaume-{U}ni },
audience = {internationale },
month = jul,
year = {2010},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {83-98}
}
@proceedings{CoqWorkshop2010,
title = {{S}econd {C}oq {W}orkshop},
editor = {Yves Bertot},
url = {http://hal.inria.fr/COQ2010},
location = {Edinburgh, UK},
month = jul,
year = {2010},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@techreport{PASCA:2010:INRIA-00463150:1,
hal_id = {inria-00463150},
url = {http://hal.inria.fr/inria-00463150/en/},
title = { {F}ormal {P}roofs for {T}heoretical {P}roperties of {N}ewton's {M}ethod},
author = {{P}a{\c{s}}ca, {I}oana},
abstract = {{W}e discuss a formal development for the certification of {N}ewton's method. {W}e address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suite the features of a proof assistant, and designing new proofs based on the existing ones to deal with optimizations of the method. {W}e start from {K}antorovitch's theorem that states the convergence of {N}ewton's method in the case of a system of equations. {T}o formalize this proof inside the proof assistant {C}oq we first need to code the necessary concepts from multivariate analysis. {W}e also prove that rounding at each step in {N}ewton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. {A}n algorithm including rounding is a more accurate model for computations with {N}ewton's method in practice.},
keywords = {proof assistants ; formalization of mathematics ; multivariate analysis ; {K}antorovitch's theorem ; {N}ewton's method with rounding},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} },
type = {Research Report},
institution = {INRIA},
number = {{RR}-7228},
day = {11},
month = mar,
year = {2010}
}
@phdthesis{Pasca10b,
author = {Ioana Pa{\c{s}}ca},
title = {Formal Verification for Numerical Methods},
year = 2010,
month = nov,
school = {Universit{\'e} Nice - Sophia Antipolis},
x-proceedings = {no},
x-editorial-board = {no},
x-international-audience = {no},
x-invited-conference = {no},
url = {http://tel.archives-ouvertes.fr/tel-00555158}
}
@article{GregoirePottierThery2010,
title = {Proof certificates for algebra and their application to automatic geometry theorem proving},
author = {Benjamin Gr{\'e}goire and Lo{\"\i}c Pottier and Laurent Th\'ery},
journal = {Lecture Notes in Artificial Intelligence},
year = 2010,
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
url = {http://hal.inria.fr/inria-00504719}
}
@inproceedings{GREGOIRE:2010:HAL-00537104:1,
hal_id = {hal-00537104},
url = {http://hal.archives-ouvertes.fr/hal-00537104/en/},
title = { {O}n {S}trong {N}ormalization of the {C}alculus of {C}onstructions with {T}ype-{B}ased {T}ermination},
author = {{G}r{\'e}goire, {B}enjamin and {S}acchini, {J}orge},
abstract = {{T}ermination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. {T}ype-based termination is a mechanism for ensuring termination that uses types annotated with size information to check that recursive calls are performed on smaller arguments. {O}ur long-term goal is to extend the {C}alculus of {I}nductive {C}onstructions with a type-based termination mechanism and prove its logical consistency. {I}n this paper, we present an extension of the {C}alculus of {C}onstructions (including universes and impredicativity) with sized natural numbers, and prove strong normalization and logical consistency. {M}oreover, the proof can be easily adapted to include other inductive types.},
language = {{A}nglais},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} },
booktitle = {{L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning: 17th {I}nternational {C}onference, {LPAR}-17, {Y}ogyakarta, {I}ndonesia, {O}ctober 10-15, 2010, {P}roceedings 17th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence and {R}easoning },
pages = {333-347 },
address = {{Y}ogyakarta {I}ndon{\'e}sie },
note = {{T}he original publication is available at www.springerlink.com },
doi = {10.1007/978-3-642-16242-8{\_}24 },
day = {07},
month = nov,
year = {2010},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{DBLP:conf/itp/BartheGB10,
author = {Gilles Barthe and
Benjamin Gr{\'e}goire and
Santiago {Zanella B{\'e}guelin}},
title = {Programming Language Techniques for Cryptographic Proofs},
pages = {115-130},
ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_10},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
booktitle = {Interactive Theorem Proving, First International Conference,
ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6172},
year = {2010},
isbn = {978-3-642-14051-8},
ee = {http://dx.doi.org/10.1007/978-3-642-14052-5},
bibsource = {DBLP, http://dblp.uni-trier.de},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
bibsource = {DBLP, http://dblp.uni-trier.de},
url = {http://hal.inria.fr/inria-00552894}
}
@inproceedings{DBLP:conf/csfw/BartheHBGH10,
author = {Gilles Barthe and
Daniel Hedin and
Santiago {Zanella B{\'e}guelin} and
Benjamin Gr{\'e}goire and
Sylvain Heraud},
title = {A Machine-Checked Formalization of Sigma-Protocols},
pages = {246-260},
ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2010.24},
booktitle = {Proceedings of the 23rd IEEE Computer Security Foundations
Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19,
2010},
publisher = {IEEE Computer Society},
year = {2010},
isbn = {978-0-7695-4082-5},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
bibsource = {DBLP, http://dblp.uni-trier.de},
url = {http://hal.inria.fr/inria-00552886}
}
@inproceedings{DBLP:conf/itp/DufourdB10,
author = {Jean-Fran\c{c}ois Dufourd and
Yves Bertot},
title = {Formal Study of Plane Delaunay Triangulation},
pages = {211-226},
ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_16},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
booktitle = {Interactive Theorem Proving, First International Conference,
ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6172},
year = {2010},
isbn = {978-3-642-14051-8},
ee = {http://dx.doi.org/10.1007/978-3-642-14052-5},
url = {http://hal.archives-ouvertes.fr/inria-00504027/},
bibsource = {DBLP, http://dblp.uni-trier.de},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@techreport{BERTOT:2010:INRIA-00503017:1,
hal_id = {inria-00503017},
url = {http://hal.archives-ouvertes.fr/inria-00503017/},
title = { {A} formal study of {B}ernstein coefficients and polynomials},
author = {{B}ertot, {Y}ves and {G}uilhot, {F}r{\'e}derique and {M}ahboubi, {A}ssia},
institution = {INRIA},
language = {{E}nglish},
month = jul,
year = {2010},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} - {T}ypi{C}al - {INRIA} {S}aclay - {I}le de {F}rance - {INRIA} - {CNRS} : {UMR} - {P}olytechnique - {X} - {L}aboratoire d'informatique de l'{\'e}cole polytechnique - {LIX} - {CNRS} : {UMR}7161 - {P}olytechnique - {X} }
}
@inproceedings{DBLP:conf/aisc/Pasca10,
author = {Ioana Pa{\c{s}}ca},
title = {Formally Verified Conditions for Regularity of Interval
Matrices},
pages = {219-233},
ee = {http://dx.doi.org/10.1007/978-3-642-14128-7_19},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {Serge Autexier and
Jacques Calmet and
David Delahaye and
Patrick D. F. Ion and
Laurence Rideau and
Renaud Rioboo and
Alan P. Sexton},
booktitle = {Intelligent Computer Mathematics, 10th International Conference,
AISC 2010, 17th Symposium, Calculemus 2010, and 9th International
Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6167},
year = {2010},
isbn = {978-3-642-14127-0},
ee = {http://dx.doi.org/10.1007/978-3-642-14128-7},
url = {http://hal.archives-ouvertes.fr/inria-00464937},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{DENES:2009:INRIA-00504065:1,
hal_id = {inria-00504065},
url = {http://hal.inria.fr/inria-00504065/en/},
title = { {F}ormal proof of theorems on genetic regulatory networks},
author = {{D}{\'e}n{\`e}s, {M}axime and {L}esage, {B}enjamin and {B}ertot, {Y}ves and {R}ichard, {A}drien},
abstract = {{W}e describe the formal verification of two theorems of theoretical biology. {T}hese theorems concern genetic regulatory networks: they give, in a discrete modeling framework, relations between the topology and the dynamics of these biological networks. {I}n the considered discrete modeling framework, the dynamics is described by a transition graph, where vertices are vectors indicating the expression level of each gene, and where edges represent the evolution of these expression levels. {T}he topology is also described by a graph, called interaction graph, where vertices are genes and where edges correspond to influences between genes. {T}he two results we formalize show that circuits of some kind must be present in the interaction graph if some behaviors are possible in the transition graph. {T}his work was performed with the ssreflect extension of the {C}oq system.},
language = {{A}nglais},
affiliation = {{MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} - {L}aboratoire d'{I}nformatique, {S}ignaux, et {S}yst{\`e}mes de {S}ophia-{A}ntipolis - {I}3{S} - {U}niversit{\'e} de {N}ice {S}ophia-{A}ntipolis - {CNRS} : {UMR}6070 },
booktitle = {{SYNASC}'09 {S}ynasc 2009, 11th {I}nternational {S}ymposium on {S}ymbolic and {N}umeric {A}lgorithms for {S}cientific {C}omputing },
publisher = {{IEEE} },
address = {{T}imisoara {R}oumanie },
audience = {internationale },
year = {2009}
}
@inproceedings{DLBR09,
author = {D{\'e}n{\`e}s, Maxime and Lesage, Benjamin and Bertot, Yves
and Richard, Adrien},
title = {Formal proof of theorems on genetic regulatory networks},
booktitle = {Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2009)},
publisher = {IEEE},
pages = {69-76},
year = {2009},
month = sep,
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{JulienP09,
author = {Nicolas Julien and
Ioana Pasca},
title = {{Formal Verification of Exact Computations Using Newton's
Method}},
booktitle = {Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009)},
publisher = {Springer},
pages = {408-423},
series = {LNCS},
volume = {5674},
year = {2009},
month = aug,
url = {http://hal.inria.fr/inria-00369511/en/},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{GGMR:TPHOLS2009,
title = { {P}ackaging {M}athematical {S}tructures},
author = {{G}arillot, {F}ran{\c{c}}ois and {G}onthier, {G}eorges and {M}ahboubi, {A}ssia and {R}ideau, {L}aurence},
keywords = {{F}ormalization of {A}lgebra, {C}oercive subtyping, {T}ype inference, {C}oq, {SSR}eflect},
language = {{A}nglais},
affiliation = {{C}entre commun {INRIA} - {M}icrosoft {R}esearch - {INRIA} - {M}icrosoft - {M}icrosoft {R}esearch {C}ambridge - {M}icrosoft - {M}icrosoft {R}esearch - {T}ypi{C}al - {INRIA} {S}aclay {I}le de {F}rance - {INRIA} - {CNRS} : {UMR} - {P}olytechnique - {X} - {MARELLE} - {INRIA} {S}ophia {A}ntipolis - {INRIA} },
booktitle = {{T}heorem {P}roving in {H}igher {O}rder {L}ogics },
publisher = {{S}pringer },
address = {{M}unich {A}llemagne },
volume = {5674 },
editor = {{T}obias {N}ipkow and {C}hristian {U}rban },
series = {{L}ecture {N}otes in {C}omputer {S}cience },
note = {{G}.: {M}athematics of {C}omputing/{G}.4: {MATHEMATICAL} {SOFTWARE}, {I}.: {C}omputing {M}ethodologies/{I}.1: {SYMBOLIC} {AND} {ALGEBRAIC} {MANIPULATION}/{I}.1.0: {G}eneral },
audience = {internationale },
year = {2009},
url = {http://hal.inria.fr/inria-00368403/en/},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-paper = {no}
}
@inproceedings{OuldBiha09,
author = {Sidi {Ould Biha}},
title = {Finite groups representation theory with Coq},
booktitle = {Mathematical Knowledge Management},
year = {2009},
pages = {438-452},
series = {LNAI},
volume = {5625},
publisher = {Springer},
month = jul,
url = {http://hal.inria.fr/inria-00377431},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{BarrasCGHS:Types09,
author = {Bruno Barras and
Pierre Corbineau and
Benjamin Gr{\'e}goire and
Hugo Herbelin and
Jorge Luis Sacchini},
title = {A New Elimination Rule for the {C}alculus of {I}nductive {C}onstructions},
booktitle = {Types for proofs and programs 2008},
year = {2009},
pages = {32-48},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
editor = {S. Berardi and F. Damiani and U de'Liguoro},
volume = {5497},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{BGOZ:2009:SP,
author = { Gilles Barthe and
Benjamin Gr{\'e}goire and
Federico Olmedo and
Santiago {Zanella B{\'e}guelin}},
title = {Formally Certifying the Security of Digital Signature Schemes},
booktitle = {30th IEEE Symposium on Security and Privacy, S\&P 2009},
year = {2009},
publisher = {IEEE},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{BGZ:2009:POPL,
author = {Gilles Barthe and
Benjamin Gr{\'e}goire and
Santiago {Zanella B{\'e}guelin}},
title = {Formal Certification of Code-Based Cryptographic Proofs},
booktitle = {36th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL 2009},
year = {2009},
pages = {90--101},
publisher = {ACM},
isbn = {978-1-60558-379-2},
url = {http://dx.doi.org/10.1145/1480881.1480894},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{BGHKP:2009:ICFEM,
author = {Gilles Barthe and
Benjamin Gr{\'e}goire and
Sylvain Heraud and
Cesar Kunz and
Anne Pacalet},
title = {Implementing a direct method for certificate translation},
booktitle = {International Conference on Formal Engineering Methods, ICFEM 2009},
pages = {541-560},
number = {5885},
series = {Lectures Notes in Computer Science},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no},
year = 2009
}
@inproceedings{GreOlaf09,
author = {Jan Olaf Blech and Benjamin Gr\'egoire},
title = { Using Checker Predicates in Certifying Code Generation },
booktitle = { Proceedings of the Workshop Compiler Optimization meets Compiler Verification (COCV 2009)},
year = {2009},
publisher = {ENTCS},
note = {To appear},
topic = {COMPILER},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@book{TributeGilles09,
title = {From {S}emantics to {C}omputer {S}cience, essays in {H}onour of {G}illes {K}ahn},
editor = {Yves Bertot and G{\'e}rard Huet and Jean-Jacques L{\'e}vy and Gordon Plotkin},
year = 2009,
publisher = {Cambridge University Press},
x-international-audience = {yes}
}
@inbook{Bertot:Kahn09,
author = {Yves Bertot},
chapter = {Theorem proving support in programming language semantics},
crossref = {TributeGilles09},
pages = {337--361},
url = {http://hal.inria.fr/inria-00160309/},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{Bertot:Lernet09,
author = {Yves Bertot},
title = {Structural abstract interpretation, A formal study in Coq},
booktitle = {Language Engineering and Rigorous Software Development,
International LerNet ALFA Summer School 2008, revised tutorial lectures},
year = {2009},
pages = {153-194},
publisher = {Springer},
editor = {A. Bove and L. S. Barbosa and A. Pardo and J. S. Pinto},
series = {Lecture Notes in Computer Science},
volume = {5520},
url = {http://hal.inria.fr/inria-00329572/},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{BertotKomendantskaya:Types09,
author = {Yves Bertot and Ekaterina Komendantskaya},
title = {Using Structural Recursion for Corecursion},
booktitle = {Types for proofs and programs 2008},
year = {2009},
pages = {220-236},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
editor = {S. Berardi and F. Damiani and U de'Liguoro},
volume = {5497},
url = {http://hal.inria.fr/inria-00322331},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@phdthesis{Hurlin09c,
author = {Cl\'ement Hurlin},
title = {\href{http://www-sop.inria.fr/everest/Clement.Hurlin/publis/these.pd
f}{Specification and Verification of Multithreaded Object-Oriented Programs with
Separation Logic}},
year = 2009,
month = sep,
school = {Universit\'e Nice - Sophia Antipolis},
abstract = {First, we develop verification rules in separation logic for primi
tives concerning multithreading:
the primitives fork and join that control how threads start
and how threads wait, and the primitive for reentrant locks
(locks that can be acquired and released more than once) that are used in Java.
Second, we develop three analyses that use separation logic. The first
analysis permits to specify sequences of method calls and to
verify that they are correct w.r.t. method contracts.
The second analysis presents a fast algorithm to disprove entailment
between separation logic formulae. The third analysis shows how to parallelize a
nd optimize programs by rewriting their proofs.},
x-proceedings = {no},
x-editorial-board = {no},
x-international-audience = {no},
x-invited-conference = {no}
}
@techreport{Hurlin09d,
author = {Cl\'ement Hurlin},
title = {Automatic Parallelization and Optimization of Programs by Proof Rewriting (or Automatic Parallelization with Separation Logic!)},
month = jun,
year = 2009,
institution = {INRIA Sophia-Antipolis -- M\'editerrann\'ee},
number = 6806,
x-proceedings = {no},
x-editorial-board = {no},
x-international-audience = {no},
x-invited-conference = {no}
}
@inproceedings{Hurlin09b,
author = {Cl\'ement Hurlin},
title = {Automatic Parallelization and Optimization of Programs by Proof Rewriting (or Automatic Parallelization with Separation Logic!)},
booktitle = {\href{http://sas09.cs.ucdavis.edu/}{Static Analysis Symposium (SA
S'09)}},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
month = aug,
year = 2009,
url = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/eterlou.pdf},
abstract = {We show how, given a program and its separation logic proof,
one can parallelize and optimize this program and transform its pr
oof simultaneously to obtain
a proven parallelized and optimized program.
To achieve this goal, we present new proof rules for generating pr
oof trees
and a rewrite system on proof trees.},
pages = {52--68},
volume = 5673,
isbn = {978-3-642-03236-3},
doi = {10.1007/978-3-642-03237-0\_6},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{HurlinBS09,
author = {Cl\'ement Hurlin and Fran\c{c}ois Bobot and Alexander J. Summers},
title = {Size Does Matter : Two Certified Abstractions to Disprove Entailment
in Intuitionistic and Classical Separation Logic},
booktitle = {\href{http://www.cs.purdue.edu/homes/wrigstad/iwaco09/index.html}
{International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09)}},
url = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/iwaco09.pdf},
ps = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/iwaco09.ps},
dvi = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/iwaco09.dvi},
month = jul,
year = {2009},
abstract = {We describe an algorithm to disprove entailment between
separation logic formulas. We abstract models
of formulas by their size and check whether two formulas
have models whose sizes are compatible.
Given two formulas $A$ and $B$ that do not have compatible models,
we can conclude that $A$ does not entail $B$. We provide
two different abstractions (of different precision) of models.
Our algorithm is of interest wherever entailment checking
is performed (such as in program verifiers).},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@article{HaackH09,
author = {Christian Haack and Cl\'ement Hurlin},
title = {Resource Usage Protocols for Iterators},
journal = {Journal of Object Technology},
abstract = {We discuss usage protocols for iterator objects that prevent concurrent
modifications of the underlying collection while iterators are in
progress.
We formalize these protocols in Java-like object interfaces, enriched with
separation logic contracts. We present examples of iterator clients and
proofs that they adhere to the iterator protocol, as well as examples
of iterator implementations and proofs that they implement the iterator
interface.},
note = {This is an extended version of a paper that appeared in the
\href{http://www.cs.purdue.edu/homes/wrigstad/iwaco08/index.html}{IWACO'08} workshop},
year = 2009,
url = {http://www.jot.fm/issues/issue\_2009\_06/article3/index.html},
volume = 8,
number = 4,
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{Hurlin09,
author = {Cl\'ement Hurlin},
title = {Specifying and Checking Protocols of Multithreaded Classes},
booktitle = {\href{http://www.acm.org/conferences/sac/sac2009/}{ACM Symposium
on Applied Computing (SAC'09)}, \href{http://www-sop.inria.fr/everest/Tamara.Rezk/SAC-SVT-09/Main.html}{Software Verification and Testing Track}},
month = mar,
year = {2009},
note = {Additional material (examples, detailed statistics, and implementation) is available:
\href{http://www-sop.inria.fr/everest/Clement.Hurlin/pyrolobus.shtml}{pyrolobus}.},
url = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/sac09.pdf},
location = {Waikiki Beach, Hawaii, USA},
abstract = {In the Design By Contract (DBC) approach,
programmers specify methods with \emph{pre and postconditions}
(also called \emph{contracts}). Earlier work added \emph{protocols}
to the DBC approach to describe allowed method call
sequences for classes. We extend
this work to
We present the semantical foundations of our extension.
We describe a new technique to check that method contracts
are correct w.r.t. to protocols.
We show how to generate
programs that must be proven to show that method contracts
are correct w.r.t. to protocols. Because little support currently exists
to help writing method contracts, our technique
helps programmers to check their contracts early in the development process.},
publisher = {ACM},
doi = {10.1145/1529282.1529407},
pages = {587--592},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
x-invited-conference = {no}
}
@inproceedings{DBLP:conf/tphol/Bertot08,
author = {Yves Bertot},
title = {A Short Presentation of Coq},
booktitle = {Theorem Proving in Higher Order Logics, 21st International
Conference, TPHOLs 2008, Montreal, Canada, August 18-21,
2008. Proceedings},
year = {2008},
pages = {12-16},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5170},
isbn = {978-3-540-71065-3},
x-proceedings = {yes},
x-international-audience = {yes},
x-invited-conference = {yes},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{LP08,
author = {Lo{\"i}c Pottier},
year = {2008},
title = {Connecting Gr{\"o}bner Bases Programs with Coq to do Proofs in
Algebra, Geometry and Arithmetics},
editor = {Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and
Konev, B. and Schulz, S.},
booktitle = {{Proceedings of the LPAR Workshops: Knowledge Exchange:
Automated Provers and Proof Assistants, and The 7th
International Workshop on the Implementation of Logics}},
place = {Doha, Qattar},
series = {CEUR Workshop Proceedings},
number = {418},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
comment = {}
}
@inproceedings{ifip/bertotThery08,
author = {Yves Bertot and Laurent Th{\'ery}},
title = {Dependent Types, Theorem Proving, and Applications for a Verifying
Compiler},
booktitle = {1st IFIP TC 2/WG 2.3 Conference, on Verified Software: Theories, Tools, Experiments (VSTTE)},
year = {2008},
series = {LNCS},
volume = {4171},
publisher = {Springer},
pages = {173--181},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes}
}
@article{Rideau-Serpette-Leroy-parmov,
author = {Laurence Rideau and Bernard P. Serpette and
Xavier Leroy},
title = {Tilting at windmills with {Coq}:
formal verification of a compilation algorithm
for parallel moves},
journal = {Journal of Automated Reasoning},
year = {2008},
volume = 40,
number = 4,
pages = {307--326},
xtopic = {compcert},
url = {http://gallium.inria.fr/~xleroy/publi/parallel-move.pdf},
urlpublisher = {http://dx.doi.org/10.1007/s10817-007-9096-8},
x-editorial-board = {yes},
x-international-audience = {yes},
abstract = {
This article describes the formal verification of a compilation algorithm
that transforms parallel moves (parallel assignments between variables)
into a semantically-equivalent sequence of elementary moves.
Two different specifications of the algorithm are given: an inductive
specification and a functional one, each with its correctness proofs.
A functional program can then be extracted and integrated in the
Compcert verified compiler.}
}
@inproceedings{BerVKom08,
author = {Yves Bertot and Vladimir Komendantsky},
title = {Fixed point semantics and partial recursion in Coq},
booktitle = {PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming},
year = {2008},
isbn = {978-1-60558-117-0},
pages = {89--96},
location = {Valencia, Spain},
doi = {http://doi.acm.org/10.1145/1389449.1389461},
publisher = {ACM},
address = {New York, NY, USA},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
url = {http://hal.inria.fr/inria-00190975/}
}
@inproceedings{BerEKom08,
author = {Yves Bertot and Ekaterina Komendantskaya},
title = {{Inductive and Coinductive Components of Corecursive Functions in Coq}},
booktitle = {Proceedings of CMCS'08, the 9th International Workshop on Coalgebraic Methods in Computer Science},
volume = 203,
series = {ENTCS},
year = 2008,
month = apr,
location = {Budapest},
pages = {25 - 47},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
url = {http://hal.inria.fr/inria-00277075/en/}
}
@inproceedings{BGOBP:BIG08,
author = {Yves Bertot and Georges Gonthier and Sidi Ould Biha and
Ioana Pa{\c{s}}ca },
title = {{Canonical Big Operators}},
month = aug,
booktitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008)},
year = 2008,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes},
volume = 5170,
pages = {12--16},
url = {http://hal.inria.fr/inria-00331193/}
}
@inproceedings{Thery08,
author = {Laurent Th{\'e}ry },
title = {{Proof Pearl. Revisiting the Mini-Rubik in Coq}},
month = aug,
booktitle = {Proceedings of the 21st International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2008)},
year = 2008,
series = {LNCS},
volume = 5170,
x-editorial-board = {yes},
x-proceedings = {yes},
x-international-audience = {yes}
}
@inproceedings{Julien08,
author = {Nicolas Julien},
title = {Certified exact real arithmetic using co-induction in arbitrary integer base},
booktitle = {Functional and Logic Programming Symposium (FLOPS)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
x-proceedings = {yes},
x-editorial-board = {yes},
x-international-audience = {yes},
url = {http://hal.inria.fr/inria-00202744},
year = {2008}
}
@inproceedings{OuldBiha08,
author = {Sidi {Ould Biha}},
title = {{Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton}},
booktitle = {Journ{\'e}es Francophones des Langages Applicatifs},
url = {http://hal.inria.fr/inria-00202795/en/},
year = {2008},
location = {{\'E}tretat},
month = jan
}
@inproceedings{Pasca08,
author = {Ioana Pa{\c{s}}ca},
title = {{A Formal Verification for Kantorovitch's Theorem}},
booktitle = {Journ{\'e}es Francophones des Langages Applicatifs},
year = {2008},
url = {http://hal.inria.fr/inria-00202808/en/},
location = {{\'E}tretat},
month = jan
}
@inproceedings{Roux08,
author = {Cody Roux},
title = {{Types, Logique et Coercions Implicites}},
booktitle = {Journ{\'e}es Francophones des Langages Applicatifs},
year = {2008},
url = {http://hal.inria.fr/inria-00202824/en/},
location = {{\'E}tretat},
month = jan
}
@inproceedings{pate2007,
author = {Jérémy Blanc and J.P. Giacometti and André Hirschowitz and Loïc Pottier},
title = {Proofs for freshmen with Coqweb},
booktitle = {Proceedings of the International Workshop on Proof Assistants and
Types in Education, June 25th, 2007, associated workshop of the 2007 Federated Conference on Rewriting, Deduction and Programming},
editor = {H. Geuvers and P. Courtieu},
month = jun,
address = {CNAM Paris, France},
year = {2007},
url = {http://www.cs.ru.nl/~herman/PUBS/proceedingsPATE.pdf}
}
@inproceedings{Julien07,
author = {Nicolas Julien},
booktitle = {\sl Journ{\'e}es francophones pour les langages applicatifs,
JFLA'07},
title = { {Arithm{\'e}tique
r{\'e}elle exacte certifi{\'e}e, co-induction et base arbitraire}},
url = {http://hal.inria.fr/inria-00116820},
year = 2007
}
@inproceedings{GMRTT:GROUPS07,
author = {Georges Gonthier and Assia Mahboubi and Laurence Rideau and Enrico Tassi and Laurent Th{\'e}ry },
title = {A Modular Formalisation of Finite Group Theory},
month = sep,
booktitle = {Proceedings of the 20th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2007)},
volume = 4732,
series = {LNCS},
publisher = {Springer-Verlag},
year = 2007,
editor = {Klaus Schneider and Jens Brandt},
pages = {86-101},
url = {http://hal.inria.fr/inria-00139131}
}
@inproceedings{LTGH:ELLIPTIC07,
author = {Laurent Th{\'e}ry and Guillaume Hanrot },
title = {Primality Proving with Elliptic Curves},
month = sep,
pages = {319-333},
url = {http://hal.inria.fr/inria-00138382},
editor = {Klaus Schneider and Jens Brandt},
booktitle = {Proceedings of the 20th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2007)},
volume = 4732,
series = {LNCS},
publisher = {Springer-Verlag},
year = 2007
}
@techreport{BerKom07,
author = {Yves Bertot and Vladimir Komendantsky},
title = {Fixed point semantics and partial recursion in Coq},
year = {2007},
month = nov,
institution = {INRIA},
note = {Draft paper, submitted to a conference},
url = {http://hal.inria.fr/inria-00190975}
}
@techreport{RSL07,
author = {Laurence Rideau and Bernard P. Serpette and Xavier Leroy},
title = {Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves},
year = {2007},
month = sep,
institution = {INRIA},
note = {Draft paper, submitted to a journal},
url = {http://hal.inria.fr/inria-00176007/fr/}
}
@phdthesis{MahboubiPhD,
author = {Assia Mahboubi},
title = {Contribution {\`a} la certification des calculs dans R : th{\'e}orie,
preuves, programmation},
school = {Uni\-versit{\'e} de Nice-Sophia Anti\-polis},
year = 2006,
address = {Nice}
}
@techreport{Bertot06,
author = {Yves Bertot},
title = {Extending the Calculus of Constructions with Tarski's
fix-point theorem},
year = {2006},
month = oct,
institution = {INRIA},
url = {http://hal.inria.fr/inria-00105529}
}
@techreport{Pottier06,
author = {Lo{\"\i}c Pottier},
title = {Ambiguous typing},
year = {2006},
month = dec,
institution = {INRIA},
url = {http://hal.inria.fr/inria-00117458}
}
@techreport{LRLT:SYLOW06,
author = {Th{\'e}ry, Laurent and Rideau, Laurence},
title = {Formalising Sylow's theorems in Coq},
year = {2006},
month = nov,
institution = {INRIA},
number = {0327},
type = {Technical Report},
pages = {23 p.},
url = {https://hal.inria.fr/inria-00113750}
}
@article{BertotMSCS06,
author = {Yves Bertot},
title = {Affine functions and series with co-inductive real numbers},
journal = {Mathematical Structure in Computer Sciences},
publisher = {Cambridge University Press},
year = 2007,
volume = 17,
number = 1,
pages = {37--63},
url = {http://hal.inria.fr/inria-00001171}
}
@article{MahboubiMSCS06,
author = {Assia Mahboubi},
title = {Implementing the cylindrical algebraic decomposition
within the Coq system},
journal = {Mathematical Structure in Computer Sciences},
year = {2007},
volume = {17},
number = {1},
pages = {99--127},
publisher = {Cambridge University Press}
}
@inproceedings{DBLP:conf/tphol/TheryLG06,
author = {Laurent Th{\'e}ry and
Pierre Letouzey and
Georges Gonthier},
title = {Coq.},
booktitle = {The Seventeen Provers of the World},
year = {2006},
volume = {3600},
pages = {28-35},
publisher = {Springer},
series = {LNCS}
}
@inproceedings{DBLP:conf/flops/GregoireTW06,
author = {Benjamin Gr{\'e}goire and
Laurent Th{\'e}ry and
Benjamin Werner},
title = {A Computational Approach to Pocklington Certificates in
Type Theory.},
booktitle = {Functional and Logic Programming Symposium (FLOPS)},
pages = {97-113},
publisher = {Springer},
series = {LNCS},
volume = {3945},
year = {2006}
}
@inproceedings{ijcar/GregoireThery06,
author = {Benjamin Gr\'egoire and Laurent Th{\'e}ry},
title = {A purely functional library for modular arithmetic and its application for certifying large prime numbers},
pages = {423-437},
booktitle = {3rd International Joint Conference on Automated Reasoning (IJCAR)},
year = 2006,
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = 4130,
editor = {U. Furbach and N. Shankar},
pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/numlib.pdf}
}
@inproceedings{ijcar/Mahboubi06,
author = {Assia Mahboubi},
title = {Proving Formally the Implementation
of an Efficient gcd Algorithm for Polynomials},
pages = {438-452},
booktitle = {3rd International Joint Conference on Automated Reasoning (IJCAR)},
year = 2006,
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = 4130,
editor = {U. Furbach and N. Shankar},
url = {https://hal.inria.fr/inria-00001270/en},
pdfurl = {https://hal.inria.fr/docs/00/06/71/08/PDF/SousRes.pdf}
}
@masterthesis{JulienMsc,
author = {Nicolas Julien},
title = {V{\'e}rification formelle d'arithm{\'e}tique r{\'e}elle exacte et
fonctions analytiques},
school = {Ecole doctorale STIC, Universit{\'e} de Nice},
year = 2006
}
@masterthesis{BihaMsc,
author = {Sidi {Ould Biha}},
title = {V{\'e}rification d'un algorithme de test de primalit{\'e} avec
Caduceus},
school = {Ecole doctorale SFA, Universit{\'e} de Nice},
year = 2006
}
@inproceedings{DBLP:conf/types/BertotGL04,
author = {Yves Bertot and
Benjamin Gr{\'e}goire and
Xavier Leroy},
title = {A Structured Approach to Proving Compiler Optimizations
Based on Dataflow Analysis.},
booktitle = {TYPES},
year = {2004},
pages = {66-81},
ee = {http://dx.doi.org/10.1007/11617990\_5},
crossref = {DBLP:conf/types/2004},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/types/2004,
editor = {Jean-Christophe Filli{\^a}tre and
Christine Paulin-Mohring and
Benjamin Werner},
title = {Types for Proofs and Programs, International Workshop, TYPES
2004, Jouy-en-Josas, France, December 15-18, 2004, Revised
Selected Papers},
booktitle = {TYPES},
publisher = {Springer},
series = {LNCS},
volume = {3839},
year = {2006},
isbn = {3-540-31428-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{CadDag,
author = {Assia Mahboubi},
title = {Programming and certifying a CAD algorithm in the Coq system.},
booktitle = {Mathematics, Algorithms, Proofs},
year = {2005},
ee = {http://drops.dagstuhl.de/opus/volltexte/2006/276},
crossref = {DBLP:conf/dagstuhl/2005P5021},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dagstuhl/2005P5021,
editor = {Thierry Coquand and
Henri Lombardi and
Marie-Fran\c{c}oise Roy},
title = {Mathematics, Algorithms, Proofs, 9.-14. January 2005},
booktitle = {Mathematics, Algorithms, Proofs},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"u}r
Informatik (IBFI), Schloss Dagstuhl, Germany},
series = {Dagstuhl Seminar Proceedings},
volume = {05021},
year = {2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{tphols2000-Letouzey,
editor = {J. Harrison and M. Aagaard},
crossref = {tphols2000},
title = {Formalizing {S}t{\aa}lmarck's algorithm in {C}oq},
author = {Pierre Letouzey and Laurent Th{\'e}ry},
pages = {387--404}
}
@inproceedings{BKT,
author = {Yves Bertot and Gilles Kahn and Laurent Th\'ery},
title = {Proof by Pointing},
booktitle = {{T}heoretical {A}spects of {C}omputer {S}oftware},
location = {Sendai, Japan},
series = {LNCS},
volume = {789},
pages = {141--160},
year = 1994
}
@inproceedings{tphols2000-Balaa,
crossref = {tphols2000},
title = {Fix-point Equations for Well-Founded Recursion in Type Theory},
author = {Antonia Balaa and Yves Bertot},
pages = {1--16}
}
@inproceedings{Pons98,
author = {Olivier Pons and Yves Bertot and Laurence Rideau},
title = {Notions of dependency in proof assistants},
booktitle = {User Interfaces for Theorem Provers 1998},
address = {Eindhoven University of Technology},
date = jul,
year = 1998
}
@article{realinterfaces,
title = {{R}eal {T}heorem {P}rovers {D}eserve {R}eal {U}ser-{I}nterfaces},
author = {Laurent {Th\'ery} and Yves Bertot and Gilles Kahn},
note = {Proceedings of the 5th Symposium on Software Development Environments},
location = {Tyson's Corner, Virginia},
year = 1992,
journal = {Software Engineering Notes},
volume = 17,
number = 5
}
@inproceedings{Bertot05b,
author = {Yves Bertot},
title = {Filters on CoInductive streams, an application to Eratosthenes' sieve},
booktitle = {Typed Lambda Calculi and Applications (TLCA'05)},
publisher = {Springer},
series = {LNCS},
year = 2005
}
@article{CtCoqDesign,
title = {The {CtCoq} System: Design and Architecture},
author = {Yves Bertot},
journal = {Formal Aspects of Computing},
volume = 11,
pages = {225--243},
year = 1999
}
@article{BertotTheryGeneric,
title = {A Generic Approach to Building User Interfaces for Theorem Provers},
author = {Yves Bertot and Laurent Th{\'e}ry},
journal = {Journal of Symbolic Computation},
year = 1998,
volume = 25,
pages = {161--194}
}
@inproceedings{reasonningexecutable,
title = {{R}easoning with {E}xecutable {S}pecifications},
author = {Yves Bertot and Ranan Fraer},
volume = 915,
pages = {531--545},
location = {Aarhus, Denmark},
year = 1995,
series = {LNCS},
journal = {Springer-Verlag LNCS},
booktitle = {Proceedings of the International Joint Conference on Theory
and Practice of Software Development (TAPSOFT'95)}
}
@techreport{RideauThery97,
author = { Laurence Rideau and Laurent Th{é}ry},
title = {Interactive Programming environment for ML},
type = {Rapport de recherche},
number = {RR-3139},
institution = {INRIA},
year = 1997,
url = {http://www.inria.fr/rrrt/rr-3139.html}
}
@inproceedings{TheryJar,
title = {A {M}achine-{C}hecked {I}mplementation of {B}uchberger's {A}lgorithm},
author = {Laurent Th{\'e}ry},
booktitle = {Journal of Automated Reasoning},
volume = {26},
pages = {107--137},
year = {2001}
}
@inproceedings{Thery98,
title = {A certified version of {B}uchberger's algorithm},
author = {Laurent Th{\'e}ry},
booktitle = {Automated Deduction---CADE-15},
publisher = {Springer-Verlag},
volume = {1421},
series = {Lecture Notes in Artificial Intelligence},
pages = {349--364},
year = {1998}
}
@inproceedings{tphols2002-BertotCaprettaDasBarman,
author = {Yves Bertot and Venanzio Capretta and Kuntal Das Barman},
title = {Type-theo\-re\-tic functional semantics},
crossref = {tphols02}
}
@article{RacineCarreeGMP,
author = {Yves Bertot and Nicolas Magaud and Paul Zimmermann},
title = {A proof of {GMP} square root},
journal = {Journal of Automated Reasoning},
publisher = {Kluwer Academic Publishers},
volume = {29},
pages = {225-252},
year = 2002
}
@inproceedings{MagaudBertot01,
title = {Changement de repr{\'e}sentation des
structures de donn{\'e}es en Coq: le cas des entiers naturels},
author = {Nicolas Magaud and Yves Bertot},
booktitle = {Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2001
}
@inproceedings{Magaud03,
author = {Nicolas Magaud},
title = {Changing Data Representation within the Coq system},
crossref = {tphols03}
}
@inproceedings{Pons00,
title = {Ing{\'e}ni{\'e}rie de preuve},
author = {Olivier Pons},
booktitle = {Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2000
}
@article{Bertot05a,
author = {Yves Bertot},
title = {V{\'e}rification formelle d'extractions de racines enti{\`e}res},
journal = {Techniques et Sciences Informatiques},
publisher = {Herm{\`e}s Sciences},
volume = {24},
number = {9},
year = 2005,
pages = {1161--1185},
note = {paru {\'e}galement comme rapport de recherche INRIA RR-5344},
url = {http://hal.inria.fr/inria-00001172/}
}
@inproceedings{DBLP:conf/tlca/CoscoyKT95,
author = {Yann Coscoy and
Gilles Kahn and
Laurent Th{\'e}ry},
title = {Extracting Text from Proofs.},
booktitle = {TLCA},
series = {LNCS},
volume = {902},
year = {1995},
pages = {109-123}
}
@proceedings{DBLP:conf/tlca/1995,
editor = {Mariangiola Dezani-Ciancaglini and
Gordon D. Plotkin},
title = {Typed Lambda Calculi and Applications, Second International
Conference on Typed Lambda Calculi and Applications, TLCA
'95, Edinburgh, UK, April 10-12, 1995, Proceedings},
booktitle = {TLCA},
publisher = {Springer},
isbn = {3-540-59048-X},
year = 1995,
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@techreport{PottierAlgebra,
author = {Lo{\"\i}c Pottier},
title = {Basics notions of algebra},
institution = {Contributions to the Coq system},
year = 1999
}
@inproceedings{MahboubiPottier2002,
title = {Élimination des quantificateurs sur les réels en {C}oq},
author = {Assia Mahboubi and Loïc Pottier},
booktitle = {{J}ourn\'ees {F}rancophones des {L}angages {A}pplicatifs,
Anglet},
month = jan,
year = {2002}
}
@inproceedings{BalaaBertot02,
title = {Fonctions r\'ecursives g\'en\'erales par it\'eration en th\'eorie
des
types},
author = {Antonia Balaa and Yves Bertot},
booktitle = {Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2002
}
@inproceedings{GregoireMahboubi05,
title = {Proving Equalities in a Commutative Ring Done Right in Coq},
author = {Benjamin Gr{\'e}goire and Assia Mahboubi},
booktitle = {Proceedings of the 18th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2005)},
editor = {Joe Hurd and Tom Melham},
series = {LNCS},
publisher = {Springer-Verlag},
year = 2005
}
@inproceedings{theryTPHOLs03,
crossref = {tphols03},
title = {Proving Pearl: Knuth's algorithm for prime numbers},
author = {Laurent Th{\'e}ry}
}
@phdthesis{pottier03hab,
author = {Pottier, Loïc},
title = {Quelques expériences de calculs et de raisonnements à l'aide de machines},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2003,
address = {Nice}
}
@phdthesis{bertot99hab,
author = {Bertot, Yves},
title = {Des environnements de programmation aux environnements de preuve},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 1999,
address = {Nice}
}
@phdthesis{chicli03thesis,
author = {Chicli, Laurent},
title = {Sur la formalisation des math\'ematiques dans le
Cal\-cul des Cons\-truc\-tions In\-duc\-tives},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2003,
address = {Nice}
}
@phdthesis{balaa02thesis,
author = {Balaa, Antonia},
title = {Fonctions récursives générales dans le calcul des constructions},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2002,
address = {Nice}
}
@phdthesis{naciri02thesis,
author = {Naciri, Hanane},
title = {Conception et réalisation d'outils pour l'interaction homme machine dans les environnements de démonstrations mathématiques},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2002,
address = {Nice}
}
@phdthesis{kuntal04thesis,
author = {Das Barman, Kuntal},
title = {Type theoretic semantics for programming languages},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2004,
address = {Nice}
}
@phdthesis{magaud2003thesis,
author = {Magaud, Nicolas},
title = {Changements de représentation des données dans le calcul des constructions},
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2003,
address = {Nice}
}
@phdthesis{coscoy00thesis,
author = {Coscoy, Yann},
title = {Explication textuelle de preuves pour le calcul des constructions inductives },
school = {Uni\-versit\'e de Nice-Sophia Anti\-polis},
year = 2000,
address = {Nice}
}
@phdthesis{pons99thesis,
author = {Pons, Olivier},
title = {Conception et réalisation d'outils d'aide au développement de grosses théories dans les systèmes de preuves interactifs},
school = { Conservatoire National des Arts et Métiers},
year = 1999,
address = {Paris}
}
@techreport{DauMorThe01,
author = {Marc Daumas and Claire Moreau-Finot and Laurent Th{\'e}ry},
address = {Le Chesnay, France},
institution = {INRIA},
number = 4095,
title = {Computer validated proofs of a toolset for adaptable
arithmetic},
type = {Research report},
year = 2001,
crindex = {Fichier},
location = {http://www.inria.fr/rrrt/rr-4095.html}
}
@techreport{TheryHuffman,
author = {Laurent Th{\'e}ry},
address = {L'Aquila, Italie},
institution = {Universit{\`a} di L'Aquila},
number = 034,
title = {{F}ormalising {H}uffman's algorithm},
type = {Technical report},
year = 2004,
crindex = {Fichier},
location = {ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Aquila.pdf}
}
@techreport{TheryPpml,
author = {Laurent Th{\'e}ry},
address = {Le Chesnay, France},
institution = {INRIA},
number = 0288,
title = {A {T}able-{D}riven {C}ompiler for {P}retty {P}rinting},
type = {Technical report},
year = 2003,
crindex = {Fichier},
location = {http://www.inria.fr/rrrt/rt-0288.html}
}
@inproceedings{DauRidThe01,
author = {Marc Daumas and Laurence Rideau and Laurent
Th{\'e}ry},
crossref = {tphols2001},
title = {A generic library of floating-point numbers and its
application to exact computing},
pages = {169-184}
}
@inproceedings{TheryCalculemus,
author = {Sylvie Boldo and Marc Daumas and Laurent Th{\'e}ry},
title = {Formal proofs and computations in finite precision arithmetic},
year = {2003},
booktitle = {Calculemus'03},
location = {Rome, Italie}
}
@book{coqart,
title = { Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions},
author = {Yves Bertot and Pierre Cast{\'e}ran},
year = 2004,
publisher = {Springer-Verlag}
}
@inproceedings{NaciriRideau00,
author = {Hanane Naciri and Laurence Rideau},
title = {Affichage interactif, bidimensionnel et incr{é}mental de formules math{é}matiques},
booktitle = {CARI'2000 5{\`e}me Colloque Africain sur la Recherche en Informatique},
location = {Antananarivo, Madagascar},
year = 2000
}
@inproceedings{NaciriRideau01b,
author = {Hanane Naciri and Laurence Rideau},
title = {{The Marriage of MathML ans Theorem Proving}},
booktitle = {IACM'2001 Workshop},
location = {London Ontario, Canada},
year = 2001
}
@techreport{NaciriRideau01c,
author = {Hanane Naciri and Laurence Rideau},
title = {Affichage et manipulation interactive de formules math{é}matiques dans les documents structur{é}s},
type = {Rapport de recherche},
number = {RR-4140},
institution = {INRIA},
year = 2001,
url = {http://www.inria.fr/rrrt/rr-4140.html}
}
@inproceedings{AmerBerRidPot01,
author = {Ahmed Amerkad and Yves Bertot and Laurence Rideau and Lo{ï}c Pottier},
title = {Mathematics and proof presentation in {Pcoq}},
booktitle = {PTP'01 Workshop},
location = {Sienna, Italy},
year = 2001
}
@inproceedings{NaciriRideau02,
author = {Hanane Naciri and Laurence Rideau},
title = {Affichage et diffusion sur Internet d'explications en langue arabe de
preuves math{\'e}matiques},
booktitle = {CARI'2002 6{\`e}me Colloque Africain sur la Recherche en Informatique},
location = {Yaound{\'e}, Cameroun},
year = 2002
}
@inproceedings{NaciriRideau02b,
title = {{Formal Mathematical Proof Explanations in Natural Language Using MathML: An Application to Proofs in Arabic}},
author = {Hanane Naciri and Laurence Rideau},
booktitle = {MathML International Conference 2002},
location = {Chicago,USA},
year = 2002
}
@inproceedings{NaciriRideau01,
title = {{FIGUE: Mathematical Formula Layout with Interaction and MathML Support}},
author = {Hanane Naciri and Laurence Rideau},
booktitle = {Fifth Asian Symposium on Computer Mathematics ASCM'2001},
location = {Chicago,USA},
year = 2002
}
@inproceedings{CYP,
title = {Colouring Proofs: A Lightweight Approach to Adding Formal Structure
to Proofs},
author = {Laurent Th{\'e}ry},
booktitle = {User-Interfaces for Theorem Provers},
series = {Electronic Notes in Theoretical Computer Science},
volume = 103,
year = 2004,
pages = {121--138}
}
@techreport{TheryPolSimpl,
author = {Laurent Théry},
title = {Simplifying Polynomial Expressions in a Proof Assistant},
type = {Rapport de recherche},
number = {RR-5614},
institution = {INRIA},
year = 2005,
url = {http://www.inria.fr/rrrt/rr-5624.html}
}
@inproceedings{geoview03,
author = {Yves Bertot and Fr{\'e}d{\'e}rique Guilhot and Lo{\"\i}c Pottier},
title = {Visualizing geometrical statements with {G}eo{V}iew},
booktitle = {User-Interfaces for Theorem Provers},
series = {Electronic Notes in Theoretical Computer Science},
volume = 103,
year = 2004
}
@inproceedings{AudebaudRideau03,
author = {Philippe Audebaud and Laurence Rideau},
title = {{TeXmacs} as Authoring Tool for Publication and Dissemination of
Formal Developments},
booktitle = {User-Interface for Theorem Provers},
journal = {Electronic Notes in Theoretical Computer Science},
volume = 103,
year = 2004
}
@inproceedings{AudebaudPaulin-mpc06,
author = {Audebaud, Philippe and Paulin, Christine},
title = {Proofs of randomized algorithms in Coq},
optcrossref = {},
optkey = {},
booktitle = {Mathematics of Program Construction},
optpages = {},
year = {2006},
editor = {Uustalu, Tarmo},
optvolume = {},
number = {4014},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
publisher = {LNCS},
optnote = {},
optannote = {}
}
@inproceedings{canonicalrationals03,
author = {Yves Bertot},
title = {Simple canonical representation of rational numbers},
booktitle = {Mathematics, Logic and Computation},
series = {Electronic Notes in Theoretical Computer Science},
volume = {85.7},
year = 2004
}
@inproceedings{NiquiBertot04,
author = {Milad Niqui and Yves Bertot},
title = {QArith: Coq Formalisation of Lazy Rational Arithmetic},
editor = {S. Berardi and M. Coppo and F. Damiani},
booktitle = {Post-Proceedings of TYPES 2003 Workshop},
location = {Torino, Italy},
volume = 3085,
series = {LNCS},
publisher = {Springer-Verlag},
year = 2004
}
@inproceedings{PichardieBertot01,
crossref = {tphols2001},
title = {Formalizing Convex Hull Algorithms},
author = {David Pichardie and Yves Bertot},
pages = {346--361}
}
@inproceedings{fg04,
author = {Fr{\'e}d{\'e}rique Guilhot},
title = {Formalisation en Coq d'un cours de g{\'e}om{\'e}trie pour le
lyc{\'e}e},
year = {2004},
booktitle = {Proceedings of JFLA'04}
}
@inproceedings{Bertot05jfla,
author = {Yves Bertot},
title = {Calcul de formules affines et de s{\'e}ries enti{\`e}res en
arithm{\'e}tique exacte avec types co-inductifs},
year = {2005},
booktitle = {Proceedings of JFLA'05}
}
@inproceedings{BertotCAV01,
title = {Formalizing a JVML verifier for initialization
in a theorem prover},
author = {Yves Bertot},
booktitle = {Computer Aided Verification (CAV'01)},
publisher = {Springer-Verlag},
address = {Paris, France},
month = jul,
year = {2001},
series = {LNCS},
number = 2102
}
@inproceedings{chicli03quotients,
author = {Chicli, Laurent and Pottier, Lo\"{\i}c and Simpson, Carlos},
title = {Mathematical quotients and quotient types in {Coq}},
booktitle = {Types for Proofs and Programs},
pages = {95-107},
year = 2003,
editor = {H. Geuvers and F. Wiedijk},
number = 2646,
series = {LNCS},
publisher = {Springer}
}
@techreport{fg02,
author = {Fr{\'e}d{\'e}rique Guilhot},
title = {Proofs with Coq of theorems in plane geometry using oriented angles},
institution = {INRIA},
type = {Rapport de recherche},
year = {2002},
number = {RR-4356}
}
@techreport{rr3488,
author = {Yves Bertot},
title = {A certified compiler for an imperative language},
institution = {INRIA},
type = {Research report},
year = 1998,
number = {RR-3488}
}
@techreport{fg03,
author = {Fr{\'e}d{\'e}rique Guilhot},
title = {Premiers pas vers un cours de g{\'e}om{\'e}trie en Coq pour le lyc{\'e}e},
institution = {INRIA},
type = {Rapport de recherche},
year = {2003},
number = {RR-4893}
}
@misc{Booksite,
author = {Yves Bertot and Pierre Cast\'eran},
title = {Coq'{A}rt: examples and exercises},
year = 2004,
note = {\url{http://www.labri.fr/Perso/~casteran/CoqArt}}
}
@proceedings{tphols2001,
editor = {Richard J. Boulton and Paul B. Jackson},
booktitle = {Theorem Proving in Higher Order Logics:
14th International Conference, TPHOLs 2001},
title = {Theorem Proving in Higher Order Logics:
14th International Conference, TPHOLs 2001},
series = {LNCS},
volume = 2152,
year = 2001,
publisher = {Springer-Verlag}
}
@article{DBLP:journals/jar/HarrisonT98,
author = {John Harrison and
Laurent Th{\'e}ry},
title = {A Skeptic's Approach to Combining HOL and Maple.},
journal = {J. Autom. Reasoning},
volume = {21},
number = {3},
year = {1998},
pages = {279-294},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{tphols2000,
editor = {J. Harrison and M. Aagaard},
title = {Theorem Proving in Higher Order Logics:
13th International Conference, TPHOLs 2000},
booktitle = {Theorem Proving in Higher Order Logics:
13th International Conference, TPHOLs 2000},
series = {LNCS},
volume = 1869,
year = 2000,
publisher = {Springer-Verlag}
}
@proceedings{tphols02,
title = {Theorem Proving in Higher Order Logics (TPHOLS'02)},
booktitle = {Theorem Proving in Higher Order Logics (TPHOLS'02)},
year = 2002,
editor = {Victor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and
Sofi{\`e}ne Tahar},
location = {Hampton, Va},
series = {LNCS},
publisher = {Springer-Verlag},
volume = 2410
}
@proceedings{tphols03,
editor = {David Basin and Burkhart Wolff},
booktitle = {Proceedings of the 16th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2003)},
title = {Proceedings of the 16th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs 2003)},
volume = 2758,
series = {LNCS},
publisher = {Springer-Verlag},
year = 2003
}
@inproceedings{RidSer05,
title = {Coq à la conquête des moulins},
author = {Laurence Rideau and Bernard P. Serpette},
booktitle = {Journ{\'e}es Francophones pour les Langages Applicatifs},
month = mar,
year = 2005
}
@inproceedings{Bertot-direct97,
author = {Yves Bertot},
title = {Direct manipulation of algebraic formulae in interactive proof
systems},
booktitle = {User-Interfaces for theorem provers (UITP'97)},
year = {1997},
url = {http://www-sop.inria.fr/croap/events/uitp97.html}
}
@techreport{Bertot07,
author = {Yves Bertot},
title = {Theorem proving support in programming language semantics},
institution = {INRIA},
url = {http://hal.inria.fr/inria-00160309/fr/},
number = {6242},
year = 2007
}
@inproceedings{bertot90implementation,
author = {Yves Bertot},
title = {Implementation of an Interpreter for a Parallel Language in Centaur},
booktitle = {European Symposium on Programming},
publisher = {Springer},
pages = {57-69},
year = {1990},
volume = {432}
}
@inproceedings{bertot92origin,
author = {Yves Bertot},
title = {Origin Functions in Lambda-Calculus and Term Rewriting Systems},
booktitle = {CAAP '92: Proceedings of the 17th Colloquium on Trees in Algebra and Programming},
year = {1992},
isbn = {3-540-55251-0},
pages = {49--65},
publisher = {Springer-Verlag},
address = {London, UK},
volume = {581}
}
@inproceedings{bertot92canonical,
author = {Yves Bertot},
title = {{A} {C}anonical {C}alculus of {R}esiduals},
booktitle = {Proceedings of the 2nd workshop on {L}ogical {F}rameworks},
publisher = {Cambridge University Press},
editor = {G. Huet and G. Plotkin},
year = {1992},
url = {citeseer.ist.psu.edu/bertot91canonical.html}
}
@inproceedings{bertot91occurrences,
author = {Y. Bertot},
title = {Occurrences in Debugger Specifications},
booktitle = {Proceedings of the {ACM} {SIGPLAN} '91 Conference on Programming Language Design and Implementation ({PLDI})},
journal = {SIGPLAN Notices},
volume = {26},
number = {6},
isbn = {0-89791-428-7},
pages = {327--337},
year = {1991},
url = {citeseer.ist.psu.edu/bertot91occurrences.html}
}
@inproceedings{DBLP:conf/amast/Bertot97,
author = {Yves Bertot},
title = {Head-Tactics Simplification},
booktitle = {AMAST},
year = {1997},
pages = {16-29},
crossref = {DBLP:conf/amast/1997},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/amast/1997,
editor = {Michael Johnson},
title = {Algebraic Methodology and Software Technology, 6th International
Conference, AMAST '97, Sydney, Australia, December 13-17,
1997, Proceedings},
booktitle = {AMAST},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1349},
year = {1997},
isbn = {3-540-63888-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cade/BertotB96,
author = {Janet Bertot and
Yves Bertot},
title = {CtCoq: A System Presentation},
booktitle = {CADE},
year = {1996},
pages = {231-234},
ee = {http://dx.doi.org/10.1007/3-540-61511-3_85},
crossref = {DBLP:conf/cade/1996},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cade/1996,
editor = {Michael A. McRobbie and
John K. Slaney},
title = {Automated Deduction - CADE-13, 13th International Conference
on Automated Deduction, New Brunswick, NJ, USA, July 30
- August 3, 1996, Proceedings},
booktitle = {CADE},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1104},
year = {1996},
isbn = {3-540-61511-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
This file was generated by bibtex2html 1.96.