Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Yves Bertot
@article{DBLP:journals/jfrea/AppelB20,
author = {Andrew W. Appel and
Yves Bertot},
title = {C floating-point proofs layered with {VST} and Flocq},
journal = {J. Formaliz. Reason.},
volume = {13},
number = {1},
pages = {1--16},
year = {2020},
url = {https://doi.org/10.6092/issn.1972-5787/11442},
doi = {10.6092/ISSN.1972-5787/11442},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfrea/AppelB20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/AppelB20a,
author = {Andrew W. Appel and
Yves Bertot},
title = {Corrigendum: {C} floating-point proofs layered with {VST} and Flocq},
journal = {J. Formaliz. Reason.},
volume = {13},
number = {1},
year = {2020},
url = {https://doi.org/10.6092/issn.1972-5787/12643},
doi = {10.6092/ISSN.1972-5787/12643},
timestamp = {Fri, 27 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfrea/AppelB20a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BertotRT18,
author = {Yves Bertot and
Laurence Rideau and
Laurent Th{\'{e}}ry},
title = {Distant Decimals of {\(\pi\)} : Formal Proofs of Some Algorithms Computing
Them and Guarantees of Exact Computation},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {33--71},
year = {2018},
url = {https://doi.org/10.1007/s10817-017-9444-2},
doi = {10.1007/S10817-017-9444-2},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BertotRT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ictac/Bertot18,
author = {Yves Bertot},
editor = {Bernd Fischer and
Tarmo Uustalu},
title = {Formal Verification of a Geometry Algorithm: {A} Quest for Abstract
Views and Symmetry in Coq Proofs},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2018 - 15th International
Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11187},
pages = {3--10},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-02508-3\_1},
doi = {10.1007/978-3-030-02508-3\_1},
timestamp = {Mon, 16 Sep 2019 15:27:43 +0200},
biburl = {https://dblp.org/rec/conf/ictac/Bertot18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1809-00559,
author = {Yves Bertot},
title = {Formal Verification of a Geometry Algorithm: {A} Quest for Abstract
Views and Symmetry in Coq Proofs},
journal = {CoRR},
volume = {abs/1809.00559},
year = {2018},
url = {http://arxiv.org/abs/1809.00559},
eprinttype = {arXiv},
eprint = {1809.00559},
timestamp = {Fri, 05 Oct 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1809-00559.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2017,
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610},
doi = {10.1145/3018610},
isbn = {978-1-4503-4705-1},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2017.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1709-01743,
author = {Yves Bertot and
Laurence Rideau and
Laurent Th{\'{e}}ry},
title = {Distant decimals of {\textdollar}{\(\pi\)}{\textdollar}},
journal = {CoRR},
volume = {abs/1709.01743},
year = {2017},
url = {http://arxiv.org/abs/1709.01743},
eprinttype = {arXiv},
eprint = {1709.01743},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1709-01743.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BernardBRS16,
author = {Sophie Bernard and
Yves Bertot and
Laurence Rideau and
Pierre{-}Yves Strub},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Formal proofs of transcendence for e and pi as an application of multivariate
and symmetric polynomials},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {76--87},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854072},
doi = {10.1145/2854065.2854072},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BernardBRS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Bertot15,
author = {Yves Bertot},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Fixed Precision Patterns for the Formal Verification of Mathematical
Constant Approximations},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {147--155},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693172},
doi = {10.1145/2676724.2693172},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Bertot15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BernardBRS15,
author = {Sophie Bernard and
Yves Bertot and
Laurence Rideau and
Pierre{-}Yves Strub},
title = {Formal Proofs of Transcendence for e and {\textdollar}{\(\pi\)}{\textdollar}
as an Application of Multivariate and Symmetric Polynomials},
journal = {CoRR},
volume = {abs/1512.02791},
year = {2015},
url = {http://arxiv.org/abs/1512.02791},
eprinttype = {arXiv},
eprint = {1512.02791},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BernardBRS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BertotA14,
author = {Yves Bertot and
Guillaume Allais},
title = {Views of {PI:} Definition and computation},
journal = {J. Formaliz. Reason.},
volume = {7},
number = {1},
pages = {105--129},
year = {2014},
url = {https://doi.org/10.6092/issn.1972-5787/4343},
doi = {10.6092/ISSN.1972-5787/4343},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfrea/BertotA14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
author = {Georges Gonthier and
Andrea Asperti and
Jeremy Avigad and
Yves Bertot and
Cyril Cohen and
Fran{\c{c}}ois Garillot and
St{\'{e}}phane Le Roux and
Assia Mahboubi and
Russell O'Connor and
Sidi Ould Biha and
Ioana Pasca and
Laurence Rideau and
Alexey Solovyev and
Enrico Tassi and
Laurent Th{\'{e}}ry},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {A Machine-Checked Proof of the Odd Order Theorem},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {163--179},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_14},
doi = {10.1007/978-3-642-39634-2\_14},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/GonthierAABCGRMOBPRSTT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/BertotGM11,
author = {Yves Bertot and
Fr{\'{e}}d{\'{e}}rique Guilhot and
Assia Mahboubi},
title = {A formal study of Bernstein coefficients and polynomials},
journal = {Math. Struct. Comput. Sci.},
volume = {21},
number = {4},
pages = {731--761},
year = {2011},
url = {https://doi.org/10.1017/S0960129511000090},
doi = {10.1017/S0960129511000090},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/BertotGM11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iccsa/PhamBN11,
author = {Tuan{-}Minh Pham and
Yves Bertot and
Julien Narboux},
editor = {Beniamino Murgante and
Osvaldo Gervasi and
Andr{\'{e}}s Iglesias and
David Taniar and
Bernady O. Apduhan},
title = {A Coq-Based Library for Interactive and Automated Theorem Proving
in Plane Geometry},
booktitle = {Computational Science and Its Applications - {ICCSA} 2011 - International
Conference, Santander, Spain, June 20-23, 2011. Proceedings, Part
{IV}},
series = {Lecture Notes in Computer Science},
volume = {6785},
pages = {368--383},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-21898-9\_32},
doi = {10.1007/978-3-642-21898-9\_32},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/iccsa/PhamBN11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/DufourdB10,
author = {Jean{-}Fran{\c{c}}ois Dufourd and
Yves Bertot},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Formal Study of Plane Delaunay Triangulation},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {211--226},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_16},
doi = {10.1007/978-3-642-14052-5\_16},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/DufourdB10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/PhamB12,
author = {Tuan{-}Minh Pham and
Yves Bertot},
editor = {David Aspinall and
Claudio Sacerdoti Coen},
title = {A Combination of a Dynamic Geometry Software With a Proof Assistant
for Interactive Formal Proofs},
booktitle = {Proceedings of the 9th International Workshop On User Interfaces for
Theorem Provers, {UITP} 2010, Edinburgh, UK, July 15, 2010},
series = {Electronic Notes in Theoretical Computer Science},
volume = {285},
pages = {43--55},
publisher = {Elsevier},
year = {2010},
url = {https://doi.org/10.1016/j.entcs.2012.06.005},
doi = {10.1016/J.ENTCS.2012.06.005},
timestamp = {Fri, 25 Nov 2022 14:25:12 +0100},
biburl = {https://dblp.org/rec/journals/entcs/PhamB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1007-3350,
author = {Jean{-}Fran{\c{c}}ois Dufourd and
Yves Bertot},
title = {Formal study of plane Delaunay triangulation},
journal = {CoRR},
volume = {abs/1007.3350},
year = {2010},
url = {http://arxiv.org/abs/1007.3350},
eprinttype = {arXiv},
eprint = {1007.3350},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1007-3350.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/DenesLBR09,
author = {Maxime D{\'{e}}n{\`{e}}s and
Benjamin Lesage and
Yves Bertot and
Adrien Richard},
editor = {Stephen M. Watt and
Viorel Negru and
Tetsuo Ida and
Tudor Jebelean and
Dana Petcu and
Daniela Zaharie},
title = {Formal Proof of Theorems on Genetic Regulatory Networks},
booktitle = {11th International Symposium on Symbolic and Numeric Algorithms for
Scientific Computing, {SYNASC} 2009, Timisoara, Romania, September
26-29, 2009},
pages = {69--76},
publisher = {{IEEE} Computer Society},
year = {2009},
url = {https://doi.org/10.1109/SYNASC.2009.44},
doi = {10.1109/SYNASC.2009.44},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/synasc/DenesLBR09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0903-3850,
author = {Yves Bertot and
Ekaterina Komendantskaya},
title = {Using Structural Recursion for Corecursion},
journal = {CoRR},
volume = {abs/0903.3850},
year = {2009},
url = {http://arxiv.org/abs/0903.3850},
eprinttype = {arXiv},
eprint = {0903.3850},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0903-3850.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lernet/Bertot08,
author = {Yves Bertot},
editor = {Ana Bove and
Lu{\'{\i}}s Soares Barbosa and
Alberto Pardo and
Jorge Sousa Pinto},
title = {Structural Abstract Interpretation: {A} Formal Study Using Coq},
booktitle = {Language Engineering and Rigorous Software Development, International
LerNet {ALFA} Summer School 2008, Piriapolis, Uruguay, February 24
- March 1, 2008, Revised Tutorial Lectures},
series = {Lecture Notes in Computer Science},
volume = {5520},
pages = {153--194},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-03153-3\_4},
doi = {10.1007/978-3-642-03153-3\_4},
timestamp = {Thu, 14 Oct 2021 10:43:04 +0200},
biburl = {https://dblp.org/rec/conf/lernet/Bertot08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/BertotK08,
author = {Yves Bertot and
Vladimir Komendantsky},
editor = {Sergio Antoy and
Elvira Albert},
title = {Fixed point semantics and partial recursion in Coq},
booktitle = {Proceedings of the 10th International {ACM} {SIGPLAN} Conference on
Principles and Practice of Declarative Programming, July 15-17, 2008,
Valencia, Spain},
pages = {89--96},
publisher = {{ACM}},
year = {2008},
url = {https://doi.org/10.1145/1389449.1389461},
doi = {10.1145/1389449.1389461},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ppdp/BertotK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/Bertot08,
author = {Yves Bertot},
editor = {Otmane A{\"{\i}}t Mohamed and
C{\'{e}}sar A. Mu{\~{n}}oz and
Sofi{\`{e}}ne Tahar},
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},
series = {Lecture Notes in Computer Science},
volume = {5170},
pages = {12--16},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71067-7\_3},
doi = {10.1007/978-3-540-71067-7\_3},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/Bertot08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/BertotGBP08,
author = {Yves Bertot and
Georges Gonthier and
Sidi Ould Biha and
Ioana Pasca},
editor = {Otmane A{\"{\i}}t Mohamed and
C{\'{e}}sar A. Mu{\~{n}}oz and
Sofi{\`{e}}ne Tahar},
title = {Canonical Big Operators},
booktitle = {Theorem Proving in Higher Order Logics, 21st International Conference,
TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5170},
pages = {86--101},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71067-7\_11},
doi = {10.1007/978-3-540-71067-7\_11},
timestamp = {Tue, 23 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BertotGBP08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/BertotK08,
author = {Yves Bertot and
Ekaterina Komendantskaya},
editor = {Stefano Berardi and
Ferruccio Damiani and
Ugo de'Liguoro},
title = {Using Structural Recursion for Corecursion},
booktitle = {Types for Proofs and Programs, International Conference, {TYPES} 2008,
Torino, Italy, March 26-29, 2008, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {5497},
pages = {220--236},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-642-02444-3\_14},
doi = {10.1007/978-3-642-02444-3\_14},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/BertotK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/BertotK08,
author = {Yves Bertot and
Ekaterina Komendantskaya},
editor = {Jir{\'{\i}} Ad{\'{a}}mek and
Clemens Kupke},
title = {Inductive and Coinductive Components of Corecursive Functions in {C}oq},
booktitle = {Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer
Science, {CMCS} 2008, Budapest, Hungary, April 4-6, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {203},
number = {5},
pages = {25--47},
publisher = {Elsevier},
year = {2008},
url = {https://doi.org/10.1016/j.entcs.2008.05.018},
doi = {10.1016/J.ENTCS.2008.05.018},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/entcs/BertotK08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0807-1524,
author = {Yves Bertot and
Ekaterina Komendantskaya},
title = {Inductive and Coinductive Components of Corecursive Functions in {C}oq},
journal = {CoRR},
volume = {abs/0807.1524},
year = {2008},
url = {http://arxiv.org/abs/0807.1524},
eprinttype = {arXiv},
eprint = {0807.1524},
timestamp = {Tue, 18 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0807-1524.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0810-2179,
author = {Yves Bertot},
title = {Structural abstract interpretation, {A} formal study using Coq},
journal = {CoRR},
volume = {abs/0810.2179},
year = {2008},
url = {http://arxiv.org/abs/0810.2179},
eprinttype = {arXiv},
eprint = {0810.2179},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0810-2179.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/Bertot07,
author = {Yves Bertot},
title = {Affine functions and series with co-inductive real numbers},
journal = {Math. Struct. Comput. Sci.},
volume = {17},
number = {1},
pages = {37--63},
year = {2007},
url = {https://doi.org/10.1017/S0960129506005809},
doi = {10.1017/S0960129506005809},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Bertot07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0707-0926,
author = {Yves Bertot},
title = {Theorem proving support in programming language semantics},
journal = {CoRR},
volume = {abs/0707.0926},
year = {2007},
url = {http://arxiv.org/abs/0707.0926},
eprinttype = {arXiv},
eprint = {0707.0926},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0707-0926.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0603117,
author = {Yves Bertot},
title = {Affine functions and series with co-inductive real numbers},
journal = {CoRR},
volume = {abs/cs/0603117},
year = {2006},
url = {http://arxiv.org/abs/cs/0603117},
eprinttype = {arXiv},
eprint = {cs/0603117},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0603117.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0603118,
author = {Yves Bertot},
title = {Coq in a Hurry},
journal = {CoRR},
volume = {abs/cs/0603118},
year = {2006},
url = {http://arxiv.org/abs/cs/0603118},
eprinttype = {arXiv},
eprint = {cs/0603118},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0603118.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0603119,
author = {Yves Bertot},
title = {CoInduction in Coq},
journal = {CoRR},
volume = {abs/cs/0603119},
year = {2006},
url = {http://arxiv.org/abs/cs/0603119},
eprinttype = {arXiv},
eprint = {cs/0603119},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0603119.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-cs-0610055,
author = {Yves Bertot},
title = {Extending the Calculus of Constructions with Tarski's fix-point theorem},
journal = {CoRR},
volume = {abs/cs/0610055},
year = {2006},
url = {http://arxiv.org/abs/cs/0610055},
eprinttype = {arXiv},
eprint = {cs/0610055},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0610055.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tsi/Bertot05,
author = {Yves Bertot},
title = {V{\'{e}}rification formelle d'extractions de racines enti{\`{e}}res},
journal = {Tech. Sci. Informatiques},
volume = {24},
number = {9},
pages = {1161--1185},
year = {2005},
url = {https://doi.org/10.3166/tsi.24.1161-1185},
doi = {10.3166/TSI.24.1161-1185},
timestamp = {Wed, 24 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tsi/Bertot05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/Bertot05,
author = {Yves Bertot},
editor = {Pawel Urzyczyn},
title = {Filters on CoInductive Streams, an Application to Eratosthenes' Sieve},
booktitle = {Typed Lambda Calculi and Applications, 7th International Conference,
{TLCA} 2005, Nara, Japan, April 21-23, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3461},
pages = {102--115},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11417170\_9},
doi = {10.1007/11417170\_9},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/Bertot05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vstte/BertotT05,
author = {Yves Bertot and
Laurent Th{\'{e}}ry},
editor = {Bertrand Meyer and
Jim Woodcock},
title = {Dependent Types, Theorem Proving, and Applications for a Verifying
Compiler},
booktitle = {Verified Software: Theories, Tools, Experiments, First {IFIP} {TC}
2/WG 2.3 Conference, {VSTTE} 2005, Zurich, Switzerland, October 10-13,
2005, Revised Selected Papers and Discussions},
series = {Lecture Notes in Computer Science},
volume = {4171},
pages = {173--181},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/978-3-540-69149-5\_19},
doi = {10.1007/978-3-540-69149-5\_19},
timestamp = {Fri, 17 Feb 2023 09:02:02 +0100},
biburl = {https://dblp.org/rec/conf/vstte/BertotT05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:series/txtcs/BertotC04,
author = {Yves Bertot and
Pierre Cast{\'{e}}ran},
title = {Interactive Theorem Proving and Program Development - Coq'Art: The
Calculus of Inductive Constructions},
series = {Texts in Theoretical Computer Science. An {EATCS} Series},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-662-07964-5},
doi = {10.1007/978-3-662-07964-5},
isbn = {978-3-642-05880-6},
timestamp = {Tue, 16 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/series/txtcs/BertotC04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/BertotGL04,
author = {Yves Bertot and
Benjamin Gr{\'{e}}goire and
Xavier Leroy},
editor = {Jean{-}Christophe Filli{\^{a}}tre and
Christine Paulin{-}Mohring and
Benjamin Werner},
title = {A Structured Approach to Proving Compiler Optimizations Based on Dataflow
Analysis},
booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2004,
Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3839},
pages = {66--81},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/11617990\_5},
doi = {10.1007/11617990\_5},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/BertotGL04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/NiquiB03,
author = {Milad Niqui and
Yves Bertot},
editor = {Stefano Berardi and
Mario Coppo and
Ferruccio Damiani},
title = {QArith: Coq Formalisation of Lazy Rational Arithmetic},
booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2003,
Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3085},
pages = {309--323},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-24849-1\_20},
doi = {10.1007/978-3-540-24849-1\_20},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/NiquiB03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/Bertot03,
author = {Yves Bertot},
editor = {Herman Geuvers and
Fairouz Kamareddine},
title = {Simple canonical representation of rational numbers},
booktitle = {Mathematics, Logic and Computation, Satellite Event of {ICALP} 2003,
Eindhoven, The Netherlands, July 4-5, 2003},
series = {Electronic Notes in Theoretical Computer Science},
volume = {85},
number = {7},
pages = {1--16},
publisher = {Elsevier},
year = {2003},
url = {https://doi.org/10.1016/S1571-0661(04)80754-0},
doi = {10.1016/S1571-0661(04)80754-0},
timestamp = {Thu, 08 Dec 2022 15:22:52 +0100},
biburl = {https://dblp.org/rec/journals/entcs/Bertot03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/BertotGP04,
author = {Yves Bertot and
Fr{\'{e}}d{\'{e}}rique Guilhot and
Loic Pottier},
editor = {David Aspinall and
Christoph L{\"{u}}th},
title = {Visualizing Geometrical Statements with GeoView},
booktitle = {Proceedings of the User Interfaces for Theorem Provers Workshop, UITP@TPHOLs
2003, Rome, Italy, September 8, 2003},
series = {Electronic Notes in Theoretical Computer Science},
volume = {103},
pages = {49--65},
publisher = {Elsevier},
year = {2003},
url = {https://doi.org/10.1016/j.entcs.2004.09.013},
doi = {10.1016/J.ENTCS.2004.09.013},
timestamp = {Fri, 09 Dec 2022 11:35:00 +0100},
biburl = {https://dblp.org/rec/journals/entcs/BertotGP04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BertotMZ02,
author = {Yves Bertot and
Nicolas Magaud and
Paul Zimmermann},
title = {A Proof of {GMP} Square Root},
journal = {J. Autom. Reason.},
volume = {29},
number = {3-4},
pages = {225--252},
year = {2002},
url = {https://doi.org/10.1023/A:1021987403425},
doi = {10.1023/A:1021987403425},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/BertotMZ02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/BertotCB02,
author = {Yves Bertot and
Venanzio Capretta and
Kuntal Das Barman},
editor = {Victor Carre{\~{n}}o and
C{\'{e}}sar A. Mu{\~{n}}oz and
Sofi{\`{e}}ne Tahar},
title = {Type-Theoretic Functional Semantics},
booktitle = {Theorem Proving in Higher Order Logics, 15th International Conference,
TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2410},
pages = {83--98},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45685-6\_7},
doi = {10.1007/3-540-45685-6\_7},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BertotCB02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/Bertot01,
author = {Yves Bertot},
editor = {G{\'{e}}rard Berry and
Hubert Comon and
Alain Finkel},
title = {Formalizing a {JVML} Verifier for Initialization in a Theorem Prover},
booktitle = {Computer Aided Verification, 13th International Conference, {CAV}
2001, Paris, France, July 18-22, 2001, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2102},
pages = {14--24},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-44585-4\_3},
doi = {10.1007/3-540-44585-4\_3},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/Bertot01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jfla/MagaudB01,
author = {Nicolas Magaud and
Yves Bertot},
editor = {Pierre Cast{\'{e}}ran},
title = {Changement de repr{\'{e}}sentation des structures de donn{\'{e}}es
en Coq: le cas des entiers naturels},
booktitle = {Journ{\'{e}}es francophones des langages applicatifs (JFLA'01),
Pontarlier, France, Janvier, 2001},
series = {Collection Didactique},
pages = {1--16},
publisher = {{INRIA}},
year = {2001},
timestamp = {Thu, 09 Feb 2006 12:05:13 +0100},
biburl = {https://dblp.org/rec/conf/jfla/MagaudB01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/PichardieB01,
author = {David Pichardie and
Yves Bertot},
editor = {Richard J. Boulton and
Paul B. Jackson},
title = {Formalizing Convex Hull Algorithms},
booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference,
TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2152},
pages = {346--361},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-44755-5\_24},
doi = {10.1007/3-540-44755-5\_24},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/PichardieB01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/BalaaB00,
author = {Antonia Balaa and
Yves Bertot},
editor = {Mark D. Aagaard and
John Harrison},
title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
booktitle = {Theorem Proving in Higher Order Logics, 13th International Conference,
TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1869},
pages = {1--16},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/3-540-44659-1\_1},
doi = {10.1007/3-540-44659-1\_1},
timestamp = {Tue, 15 Aug 2023 09:02:05 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BalaaB00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/MagaudB00,
author = {Nicolas Magaud and
Yves Bertot},
editor = {Paul Callaghan and
Zhaohui Luo and
James McKinna and
Robert Pollack},
title = {Changing Data Structures in Type Theory: {A} Study of Natural Numbers},
booktitle = {Types for Proofs and Programs, International Workshop, {TYPES} 2000,
Durham, UK, December 8-12, 2000, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {2277},
pages = {181--196},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/3-540-45842-5\_12},
doi = {10.1007/3-540-45842-5\_12},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/types/MagaudB00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cca/Group99,
author = {Yves Bertot and
Laurence Rideau and
Lo{\"{\i}}c Pottier and
Laurent Thiry},
title = {CtCoq: an environment for mathematical reasoning},
journal = {{SIGSAM} Bull.},
volume = {33},
number = {3},
pages = {21--22},
year = {1999},
url = {https://doi.org/10.1145/347127.347405},
doi = {10.1145/347127.347405},
timestamp = {Mon, 18 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cca/Group99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/Bertot99,
author = {Yves Bertot},
title = {The CtCoq System: Design and Architecture},
journal = {Formal Aspects Comput.},
volume = {11},
number = {3},
pages = {225--243},
year = {1999},
url = {https://doi.org/10.1007/s001650050049},
doi = {10.1007/S001650050049},
timestamp = {Mon, 09 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fac/Bertot99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tphol/1999,
editor = {Yves Bertot and
Gilles Dowek and
Andr{\'{e}} Hirschowitz and
Christine Paulin{-}Mohring and
Laurent Th{\'{e}}ry},
title = {Theorem Proving in Higher Order Logics, 12th International Conference,
TPHOLs'99, Nice, France, September, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1690},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48256-3},
doi = {10.1007/3-540-48256-3},
isbn = {3-540-66463-7},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tphol/1999.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsc/BertotT98,
author = {Yves Bertot and
Laurent Th{\'{e}}ry},
title = {A Generic Approach to Building User Interfaces for Theorem Provers},
journal = {J. Symb. Comput.},
volume = {25},
number = {2},
pages = {161--194},
year = {1998},
url = {https://doi.org/10.1006/jsco.1997.0171},
doi = {10.1006/JSCO.1997.0171},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jsc/BertotT98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/amast/Bertot97,
author = {Yves Bertot},
editor = {Michael Johnson},
title = {Head-Tactics Simplification},
booktitle = {Algebraic Methodology and Software Technology, 6th International Conference,
{AMAST} '97, Sydney, Australia, December 13-17, 1997, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1349},
pages = {16--29},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/BFb0000460},
doi = {10.1007/BFB0000460},
timestamp = {Tue, 14 May 2019 10:00:38 +0200},
biburl = {https://dblp.org/rec/conf/amast/Bertot97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/amast/BertotB96,
author = {Janet Bertot and
Yves Bertot},
editor = {Martin Wirsing and
Maurice Nivat},
title = {CtCoq: {A} System Presentation},
booktitle = {Algebraic Methodology and Software Technology, 5th International Conference,
{AMAST} '96, Munich, Germany, July 1-5, 1996, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1101},
pages = {600--603},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/BFb0014352},
doi = {10.1007/BFB0014352},
timestamp = {Tue, 14 May 2019 10:00:38 +0200},
biburl = {https://dblp.org/rec/conf/amast/BertotB96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BertotB96,
author = {Janet Bertot and
Yves Bertot},
editor = {Michael A. McRobbie and
John K. Slaney},
title = {CtCoq: {A} System Presentation},
booktitle = {Automated Deduction - CADE-13, 13th International Conference on Automated
Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1104},
pages = {231--234},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61511-3\_85},
doi = {10.1007/3-540-61511-3\_85},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/BertotB96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tapsoft/BertotF95,
author = {Yves Bertot and
Ranan Fraer},
editor = {Peter D. Mosses and
Mogens Nielsen and
Michael I. Schwartzbach},
title = {Reasoning with Executable Specifications},
booktitle = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {915},
pages = {531--545},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-59293-8\_218},
doi = {10.1007/3-540-59293-8\_218},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/tapsoft/BertotF95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacs/BertotKT94,
author = {Yves Bertot and
Gilles Kahn and
Laurent Th{\'{e}}ry},
editor = {Masami Hagiya and
John C. Mitchell},
title = {Proof by Pointing},
booktitle = {Theoretical Aspects of Computer Software, International Conference
{TACS} '94, Sendai, Japan, April 19-22, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {789},
pages = {141--160},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-57887-0\_94},
doi = {10.1007/3-540-57887-0\_94},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/tacs/BertotKT94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/caap/Bertot92,
author = {Yves Bertot},
editor = {Jean{-}Claude Raoult},
title = {Origin Functions in Lambda-Calculus and Term Rewriting Systems},
booktitle = {{CAAP} '92, 17th Colloquium on Trees in Algebra and Programming, Rennes,
France, February 26-28, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {581},
pages = {49--65},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-55251-0\_3},
doi = {10.1007/3-540-55251-0\_3},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/caap/Bertot92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sde/TheryBK92,
author = {Laurent Th{\'{e}}ry and
Yves Bertot and
Gilles Kahn},
editor = {Ian Thomas},
title = {Real theorem provers deserve real user-interfaces},
booktitle = {5th {ACM} {SIGSOFT} Symposium on Software Development Environments,
{SDE} 1992, Washington, DC, USA, December 9-11, 1992},
pages = {120--129},
publisher = {{ACM}},
year = {1992},
url = {https://doi.org/10.1145/142868.143760},
doi = {10.1145/142868.143760},
timestamp = {Mon, 14 Feb 2022 14:46:35 +0100},
biburl = {https://dblp.org/rec/conf/sde/TheryBK92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/Bertot91,
author = {Yves Bertot},
editor = {David S. Wise},
title = {Occurences in Debugger Specifications},
booktitle = {Proceedings of the {ACM} SIGPLAN'91 Conference on Programming Language
Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28,
1991},
pages = {327--337},
publisher = {{ACM}},
year = {1991},
url = {https://doi.org/10.1145/113445.113473},
doi = {10.1145/113445.113473},
timestamp = {Fri, 09 Jul 2021 14:03:46 +0200},
biburl = {https://dblp.org/rec/conf/pldi/Bertot91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/Bertot90,
author = {Yves Bertot},
editor = {Neil D. Jones},
title = {Implementation of an Interpreter for a Parallel Language in Centaur},
booktitle = {ESOP'90, 3rd European Symposium on Programming, Copenhagen, Denmark,
May 15-18, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {432},
pages = {57--69},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52592-0\_55},
doi = {10.1007/3-540-52592-0\_55},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/esop/Bertot90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-04-21 17:27 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
