Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "stream:conf/cpp:"
download as .bib file
@inproceedings{DBLP:conf/cpp/AdjedjLMPP24,
author = {Arthur Adjedj and
Meven Lennon{-}Bertrand and
Kenji Maillard and
Pierre{-}Marie P{\'{e}}drot and
Lo{\"{\i}}c Pujet},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Martin-L{\"{o}}f {\`{a}} la Coq},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {230--245},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636951},
doi = {10.1145/3636501.3636951},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AdjedjLMPP24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AhrensMWW24,
author = {Benedikt Ahrens and
Ralph Matthes and
Niels van der Weide and
Kobe Wullaert},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Displayed Monoidal Categories for the Semantics of Linear Logic},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {260--273},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636956},
doi = {10.1145/3636501.3636956},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AhrensMWW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AppelK24,
author = {Andrew W. Appel and
Ariel Kellison},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {VCFloat2: Floating-Point Error Analysis in Coq},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {14--29},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636953},
doi = {10.1145/3636501.3636953},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AppelK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BorgesBRRBJ24,
author = {Ana de Almeida Borges and
Mireia Gonz{\'{a}}lez Bedmar and
Juan Jos{\'{e}} Conejero Rodr{\'{\i}}guez and
Eduardo Hermo Reyes and
Joaquim Casals Bu{\~{n}}uel and
Joost J. Joosten},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {{UTC} Time, Formally Verified},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {2--13},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636958},
doi = {10.1145/3636501.3636958},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BorgesBRRBJ24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ChavanonBN24,
author = {Cl{\'{e}}ment Chavanon and
Fr{\'{e}}d{\'{e}}ric Besson and
Tristan Ninet},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {PfComp: {A} Verified Compiler for Packet Filtering Leveraging Binary
Decision Diagrams},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {89--102},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636954},
doi = {10.1145/3636501.3636954},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ChavanonBN24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/EdmondsP24,
author = {Chelsea Edmonds and
Lawrence C. Paulson},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Formal Probabilistic Methods for Combinatorial Structures using the
Lov{\'{a}}sz Local Lemma},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {132--146},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636946},
doi = {10.1145/3636501.3636946},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/EdmondsP24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Eremondi24,
author = {Joseph Eremondi},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple
Arguments},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {205--217},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636948},
doi = {10.1145/3636501.3636948},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Eremondi24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Frutos-Fernandez24,
author = {Mar{\'{\i}}a In{\'{e}}s de Frutos{-}Fern{\'{a}}ndez and
Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {A Formalization of Complete Discrete Valuation Rings and Local Fields},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {190--204},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636942},
doi = {10.1145/3636501.3636942},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Frutos-Fernandez24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GadgilT24,
author = {Siddhartha Gadgil and
Anand Rao Tadipatri},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {177--189},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636947},
doi = {10.1145/3636501.3636947},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/GadgilT24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HaselwarterHHWH24,
author = {Philipp G. Haselwarter and
Benjamin Salling Hvass and
Lasse Letager Hansen and
Th{\'{e}}o Winterhalter and
Catalin Hritcu and
Bas Spitters},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed
Cryptography},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {30--44},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636961},
doi = {10.1145/3636501.3636961},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HaselwarterHHWH24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HirokawaKST24,
author = {Nao Hirokawa and
Dohan Kim and
Kiraku Shintani and
Ren{\'{e}} Thiemann},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical
Pairs},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {147--161},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636949},
doi = {10.1145/3636501.3636949},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HirokawaKST24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KudasovRW24,
author = {Nikolai Kudasov and
Emily Riehl and
Jonathan Weinberger},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Formalizing the {\(\infty\)}-Categorical Yoneda Lemma},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {274--290},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636945},
doi = {10.1145/3636501.3636945},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KudasovRW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Monniaux24,
author = {David Monniaux},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Memory Simulations, Security and Optimization in a Verified Compiler},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {103--117},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636952},
doi = {10.1145/3636501.3636952},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Monniaux24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MulderK24,
author = {Ike Mulder and
Robbert Krebbers},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Unification for Subformula Linking under Quantifiers},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {75--88},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636950},
doi = {10.1145/3636501.3636950},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MulderK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/NguyenBMW24,
author = {Duc{-}Than Nguyen and
Lennart Beringer and
William Mansky and
Shengyi Wang},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Compositional Verification of Concurrent {C} Programs with Search
Structure Templates},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {60--74},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636940},
doi = {10.1145/3636501.3636940},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/NguyenBMW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Raad24,
author = {Azalea Raad},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Under-Approximation for Scalable Bug Detection (Keynote)},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {1},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3637683},
doi = {10.1145/3636501.3637683},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Raad24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ShillitoK24,
author = {Ian Shillito and
Dominik Kirst},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness
of Bi-intuitionistic Logic},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {218--229},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636957},
doi = {10.1145/3636501.3636957},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ShillitoK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WeideRAN24,
author = {Niels van der Weide and
Nima Rasekh and
Benedikt Ahrens and
Paige Randall North},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Univalent Double Categories},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {246--259},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636955},
doi = {10.1145/3636501.3636955},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WeideRAN24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WhiteTSM24,
author = {Lauren M. White and
Laura Titolo and
J. Tanner Slagel and
C{\'{e}}sar A. Mu{\~{n}}oz},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {A Temporal Differential Dynamic Logic Formal Embedding},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {162--176},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636943},
doi = {10.1145/3636501.3636943},
timestamp = {Mon, 03 Jun 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WhiteTSM24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ZhaoPA0S24,
author = {Qiyuan Zhao and
George P{\^{\i}}rlea and
Zhendong Ang and
Umang Mathur and
Ilya Sergey},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees
in Separation Logic},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {45--59},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636944},
doi = {10.1145/3636501.3636944},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ZhaoPA0S24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ZhuchkoVE24,
author = {Ekaterina Zhuchko and
Margus Veanes and
Gabriel Ebner},
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Lean Formalization of Extended Regular Expression Matching with Lookarounds},
booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
pages = {118--131},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501.3636959},
doi = {10.1145/3636501.3636959},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ZhuchkoVE24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2024,
editor = {Amin Timany and
Dmitriy Traytel and
Brigitte Pientka and
Sandrine Blazy},
title = {Proceedings of the 13th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2024, London, UK, January 15-16,
2024},
publisher = {{ACM}},
year = {2024},
url = {https://doi.org/10.1145/3636501},
doi = {10.1145/3636501},
timestamp = {Thu, 11 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2024.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/0002JS23,
author = {Yannick Forster and
Felix Jahn and
Gert Smolka},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem
in Constructive Type Theory (Proof Pearl)},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {159--166},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575690},
doi = {10.1145/3573105.3575690},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/0002JS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AffeldtCS23,
author = {Reynald Affeldt and
Cyril Cohen and
Ayumu Saito},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in Coq},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {3--16},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575691},
doi = {10.1145/3573105.3575691},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AffeldtCS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AllamigeonCS23,
author = {Xavier Allamigeon and
Quentin Canu and
Pierre{-}Yves Strub},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Formal Disproof of Hirsch Conjecture},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {17--29},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575678},
doi = {10.1145/3573105.3575678},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AllamigeonCS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ArasuRRSFHPR23,
author = {Arvind Arasu and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Aymeric Fromherz and
Kesha Hietala and
Bryan Parno and
Ravi Ramamurthy},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {FastVer2: {A} Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {30--46},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575687},
doi = {10.1145/3573105.3575687},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ArasuRRSFHPR23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BaanenBCD23,
author = {Anne Baanen and
Alex J. Best and
Nirvana Coppola and
Sander R. Dahmen},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Formalized Class Group Computations and Integral Points on Mordell
Elliptic Curves},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {47--62},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575682},
doi = {10.1145/3573105.3575682},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BaanenBCD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Blazy23,
author = {Sandrine Blazy},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {CompCert: {A} Journey through the Landscape of Mechanized Semantics
for Verified Compilation (Keynote)},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {1},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3579107},
doi = {10.1145/3573105.3579107},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Blazy23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Blot0CPKMV23,
author = {Valentin Blot and
Denis Cousineau and
Enzo Crance and
Louise Dubois de Prisque and
Chantal Keller and
Assia Mahboubi and
Pierre Vial},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Compositional Pre-processing for Automated Reasoning in Dependent
Type Theory},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {63--77},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575676},
doi = {10.1145/3573105.3575676},
timestamp = {Tue, 07 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Blot0CPKMV23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BordgM23,
author = {Anthony Bordg and
Adri{\'{a}}n Do{\~{n}}a Mateo},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Encoding Dependently-Typed Constructions into Simple Type Theory},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {78--89},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575679},
doi = {10.1145/3573105.3575679},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BordgM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Clune23,
author = {Joshua Clune},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Formalized Reduction of Keller's Conjecture},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {90--101},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575669},
doi = {10.1145/3573105.3575669},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Clune23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DaggittAKKA23,
author = {Matthew L. Daggitt and
Robert Atkey and
Wen Kokke and
Ekaterina Komendantskaya and
Luca Arnaboldi},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Compiling Higher-Order Specifications to {SMT} Solvers: How to Deal
with Rejection Constructively},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {102--120},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575674},
doi = {10.1145/3573105.3575674},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DaggittAKKA23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoornMN23,
author = {Floris van Doorn and
Patrick Massot and
Oliver Nash},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Formalising the h-Principle and Sphere Eversion},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {121--134},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575688},
doi = {10.1145/3573105.3575688},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DoornMN23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Farber23,
author = {Michael F{\"{a}}rber},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Terms for Efficient Proof Checking and Parsing},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {135--147},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575686},
doi = {10.1145/3573105.3575686},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Farber23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FereeG23,
author = {Hugo F{\'{e}}r{\'{e}}e and
Sam van Gool},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Formalizing and Computing Propositional Quantifiers},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {148--158},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575668},
doi = {10.1145/3573105.3575668},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FereeG23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GregoireLT23,
author = {Benjamin Gr{\'{e}}goire and
Jean{-}Christophe L{\'{e}}chenet and
Enrico Tassi},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Practical and Sound Equality Tests, Automatically: Deriving eqType
Instances for Jasmin's Data Types with Coq-Elpi},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {167--181},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575683},
doi = {10.1145/3573105.3575683},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/GregoireLT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HerklotzDB23,
author = {Yann Herklotz and
Delphine Demange and
Sandrine Blazy},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Mechanised Semantics for Gated Static Single Assignment},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {182--196},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575681},
doi = {10.1145/3573105.3575681},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/HerklotzDB23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kaliszyk23,
author = {Cezary Kaliszyk},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Improved Assistance for Interactive Proof (Keynote)},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {2},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3579108},
doi = {10.1145/3573105.3579108},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Kaliszyk23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KohlM23,
author = {Christina Kohl and
Aart Middeldorp},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Formalization of the Development Closedness Criterion for Left-Linear
Term Rewrite Systems},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {197--210},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575667},
doi = {10.1145/3573105.3575667},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KohlM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KosaianTP23,
author = {Katherine Kosaian and
Yong Kiam Tan and
Andr{\'{e}} Platzer},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {211--224},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575672},
doi = {10.1145/3573105.3575672},
timestamp = {Mon, 27 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KosaianTP23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Koutsoukou-Argyraki23,
author = {Angeliki Koutsoukou{-}Argyraki and
Mantas Baksys and
Chelsea Edmonds},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Formalisation of the Balog-Szemer{\'{e}}di-Gowers Theorem in
Isabelle/HOL},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {225--238},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575680},
doi = {10.1145/3573105.3575680},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Koutsoukou-Argyraki23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LamiauxLM23,
author = {Thomas Lamiaux and
Axel Ljungstr{\"{o}}m and
Anders M{\"{o}}rtberg},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Computing Cohomology Rings in Cubical Agda},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {239--252},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575677},
doi = {10.1145/3573105.3575677},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/LamiauxLM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LimpergF23,
author = {Jannis Limperg and
Asta Halkj{\ae}r From},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Aesop: White-Box Best-First Proof Search for Lean},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {253--266},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575671},
doi = {10.1145/3573105.3575671},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LimpergF23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Mehta23,
author = {Bhavik Mehta},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Formalising Sharkovsky's Theorem (Proof Pearl)},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {267--274},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575689},
doi = {10.1145/3573105.3575689},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Mehta23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/NiDFRS23,
author = {Haobin Ni and
Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and
Tahina Ramananandro and
Nikhil Swamy},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {ASN1*: Provably Correct, Non-malleable Parsing for {ASN.1} {DER}},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {275--289},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575684},
doi = {10.1145/3573105.3575684},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/NiDFRS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/NielsenAS23,
author = {Eske Hoy Nielsen and
Danil Annenkov and
Bas Spitters},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Formalising Decentralised Exchanges in Coq},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {290--302},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575685},
doi = {10.1145/3573105.3575685},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/NielsenAS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PetersonCCISDAF23,
author = {Rudy Peterson and
Eric Hayden Campbell and
John Chen and
Natalie Isak and
Calvin Shyu and
Ryan Doenges and
Parisa Ataei and
Nate Foster},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {P4Cub: {A} Little Language for Big Routers},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {303--319},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575670},
doi = {10.1145/3573105.3575670},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/PetersonCCISDAF23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WebbHU23,
author = {Brae J. Webb and
Ian J. Hayes and
Mark Utting},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Verifying Term Graph Optimizations using Isabelle/HOL},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {320--333},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575673},
doi = {10.1145/3573105.3575673},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/WebbHU23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/YingD23,
author = {Kexing Ying and
R{\'{e}}my Degenne},
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {A Formalization of Doob's Martingale Convergence Theorems in mathlib},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
pages = {334--347},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105.3575675},
doi = {10.1145/3573105.3575675},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/YingD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2023,
editor = {Robbert Krebbers and
Dmitriy Traytel and
Brigitte Pientka and
Steve Zdancewic},
title = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January
16-17, 2023},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3573105},
doi = {10.1145/3573105},
timestamp = {Fri, 13 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2023.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AhrensMM22,
author = {Benedikt Ahrens and
Ralph Matthes and
Anders M{\"{o}}rtberg},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Implementing a category-theoretic framework for typed abstract syntax},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {307--323},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503678},
doi = {10.1145/3497775.3503678},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AhrensMM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AmbalLS22,
author = {Guillaume Ambal and
Sergue{\"{\i}} Lenglet and
Alan Schmitt},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Certified abstract machines for skeletal semantics},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {55--67},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503676},
doi = {10.1145/3497775.3503676},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AmbalLS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Andronick22,
author = {June Andronick},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {The sel4 verification: the art and craft of proof and the reality
of commercial support (invited talk)},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {1},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3505265},
doi = {10.1145/3497775.3505265},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Andronick22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Appel22,
author = {Andrew W. Appel},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Coq's vibrant ecosystem for verification engineering (invited talk)},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {2--11},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503951},
doi = {10.1145/3497775.3503951},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Appel22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AvigadGLST22,
author = {Jeremy Avigad and
Lior Goldberg and
David Levit and
Yoav Seginer and
Alon Titelman},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {A verified algebraic representation of cairo program execution},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {153--165},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503675},
doi = {10.1145/3497775.3503675},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/AvigadGLST22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CarbonneauxZKON22,
author = {Quentin Carbonneaux and
Noam Zilberstein and
Christoph Klee and
Peter W. O'Hearn and
Francesco Zappa Nardelli},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Applying formal verification to microkernel {IPC} at meta},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {116--129},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503681},
doi = {10.1145/3497775.3503681},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CarbonneauxZKON22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Chan22,
author = {Hing{-}Lun Chan},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Windmills of the minds: an algorithm for fermat's two squares theorem},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {251--264},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503673},
doi = {10.1145/3497775.3503673},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Chan22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CheungOR22,
author = {Louis Cheung and
Liam O'Connor and
Christine Rizkallah},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Overcoming restraint: composing verification of foreign functions
with cogent},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {13--26},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503686},
doi = {10.1145/3497775.3503686},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CheungOR22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ConradTGPD22,
author = {Esther Conrad and
Laura Titolo and
Dimitra Giannakopoulou and
Thomas Pressburger and
Aaron Dutle},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {A compositional proof framework for FRETish requirements},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {68--81},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503685},
doi = {10.1145/3497775.3503685},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ConradTGPD22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DonatoSW22,
author = {Pablo Donato and
Pierre{-}Yves Strub and
Benjamin Werner},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {A drag-and-drop proof tactic},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {197--209},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503692},
doi = {10.1145/3497775.3503692},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DonatoSW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/EgolfLF22,
author = {Derek Egolf and
Sam Lasser and
Kathleen Fisher},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Verbatim++: verified, optimized, and semantically rich lexing with
derivatives},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {27--39},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503694},
doi = {10.1145/3497775.3503694},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/EgolfLF22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Farber22,
author = {Michael F{\"{a}}rber},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Safe, fast, concurrent proof checking for the lambda-pi calculus modulo
rewriting},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {225--238},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503683},
doi = {10.1145/3497775.3503683},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Farber22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FirsovU22,
author = {Denis Firsov and
Dominique Unruh},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Reflection, rewinding, and coin-toss in EasyCrypt},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {166--179},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503693},
doi = {10.1145/3497775.3503693},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FirsovU22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Frumin22,
author = {Dan Frumin},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Semantic cut elimination for the logic of bunched implications, formalized
in Coq},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {291--306},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503690},
doi = {10.1145/3497775.3503690},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Frumin22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/JohannG22,
author = {Patricia Johann and
Enrico Ghiorzi},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {(Deep) induction rules for GADTs},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {324--337},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503680},
doi = {10.1145/3497775.3503680},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/JohannG22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KanLRS22,
author = {Shuanglong Kan and
Anthony Widjaja Lin and
Philipp R{\"{u}}mmer and
Micha Schrader},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {CertiStr: a certified string solver},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {210--224},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503691},
doi = {10.1145/3497775.3503691},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KanLRS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kellison22,
author = {Ariel Kellison},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {A machine-checked direct proof of the Steiner-lehmus theorem},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {265--273},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503682},
doi = {10.1145/3497775.3503682},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Kellison22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KochK22,
author = {Mark Koch and
Dominik Kirst},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Undecidability, incompleteness, and completeness of second-order logic
in Coq},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {274--290},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503684},
doi = {10.1145/3497775.3503684},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KochK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Milehins22,
author = {Mihails Milehins},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {An extension of the framework types-to-sets for Isabelle/HOL},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {180--196},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503674},
doi = {10.1145/3497775.3503674},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Milehins22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MoineCP22,
author = {Alexandre Moine and
Arthur Chargu{\'{e}}raud and
Fran{\c{c}}ois Pottier},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Specification and verification of a transient stack},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {82--99},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503677},
doi = {10.1145/3497775.3503677},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MoineCP22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Munoz22,
author = {C{\'{e}}sar Mu{\~{n}}oz},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Structural embeddings revisited (invited talk)},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {12},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503949},
doi = {10.1145/3497775.3503949},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Munoz22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Nash22,
author = {Oliver Nash},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Formalising lie algebras},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {239--250},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503672},
doi = {10.1145/3497775.3503672},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Nash22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Prieto-Cubides22,
author = {Jonathan Prieto{-}Cubides},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {On homotopy of walks and spherical maps in homotopy type theory},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {338--351},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503671},
doi = {10.1145/3497775.3503671},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Prieto-Cubides22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchultzDT22,
author = {William Schultz and
Ian Dardik and
Stavros Tripakis},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Formal verification of a distributed dynamic reconfiguration protocol},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {143--152},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503688},
doi = {10.1145/3497775.3503688},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/SchultzDT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SixGBMFN22,
author = {Cyril Six and
L{\'{e}}o Gourdin and
Sylvain Boulm{\'{e}} and
David Monniaux and
Justus Fasse and
Nicolas Nardino},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Formally verified superblock scheduling},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {40--54},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503679},
doi = {10.1145/3497775.3503679},
timestamp = {Sat, 19 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SixGBMFN22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SpallMT22,
author = {Sarah Spall and
Neil Mitchell and
Sam Tobin{-}Hochstadt},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Forward build systems, formally},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {130--142},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503687},
doi = {10.1145/3497775.3503687},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/SpallMT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/VindumFB22,
author = {Simon Friis Vindum and
Dan Frumin and
Lars Birkedal},
editor = {Andrei Popescu and
Steve Zdancewic},
title = {Mechanized verification of a fine-grained concurrent queue from meta's
folly library},
booktitle = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
pages = {100--115},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775.3503689},
doi = {10.1145/3497775.3503689},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/VindumFB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2022,
editor = {Andrei Popescu and
Steve Zdancewic},
title = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3497775},
doi = {10.1145/3497775},
isbn = {978-1-4503-9182-5},
timestamp = {Mon, 17 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2022.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AnnenkovMNS21,
author = {Danil Annenkov and
Mikkel Milo and
Jakob Botsch Nielsen and
Bas Spitters},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Extracting smart contracts tested and verified in Coq},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {105--121},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439934},
doi = {10.1145/3437992.3439934},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AnnenkovMNS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BeckerBGDM21,
author = {Heiko Becker and
Nathaniel Bos and
Ivan Gavran and
Eva Darulova and
Rupak Majumdar},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Lassie: {HOL4} tactics by example},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {212--223},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439925},
doi = {10.1145/3437992.3439925},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BeckerBGDM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BegayCM21,
author = {Pierre{-}L{\'{e}}o B{\'{e}}gay and
Pierre Cr{\'{e}}gut and
Jean{-}Fran{\c{c}}ois Monin},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Developing and certifying Datalog optimizations in coq/mathcomp},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {163--177},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439913},
doi = {10.1145/3437992.3439913},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BegayCM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BenzakenCCKZ21,
author = {V{\'{e}}ronique Benzaken and
Sarah Cohen{-}Boulakia and
Evelyne Contejean and
Chantal Keller and
R{\'{e}}becca Zucchini},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A Coq formalization of data provenance},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {152--162},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439920},
doi = {10.1145/3437992.3439920},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BenzakenCCKZ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CattN21,
author = {Elliot Catt and
Michael Norrish},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {On the formalisation of Kolmogorov complexity},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {291--299},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439921},
doi = {10.1145/3437992.3439921},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CattN21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ChhakTA21,
author = {C. H. R. Chhak and
Andrew Tolmach and
Sean Noble Anderson},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Towards formally verified compilation of tag-based policy enforcement},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {137--151},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439929},
doi = {10.1145/3437992.3439929},
timestamp = {Mon, 04 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ChhakTA21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CommelinL21,
author = {Johan Commelin and
Robert Y. Lewis},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Formalizing the ring of Witt vectors},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {264--277},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439919},
doi = {10.1145/3437992.3439919},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CommelinL21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DesharnaisB21,
author = {Martin Desharnais and
Stefan Brunthaler},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Towards efficient and verified virtual machines for dynamic languages},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {61--75},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439923},
doi = {10.1145/3437992.3439923},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DesharnaisB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HaslbeckT21,
author = {Max W. Haslbeck and
Ren{\'{e}} Thiemann},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {An Isabelle/HOL formalization of AProVE's termination method for {LLVM}
{IR}},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {238--249},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439935},
doi = {10.1145/3437992.3439935},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/HaslbeckT21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HinrichsenLKB21,
author = {Jonas Kastberg Hinrichsen and
Dani{\"{e}}l Louwrink and
Robbert Krebbers and
Jesper Bengtson},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Machine-checked semantic session typing},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {178--198},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439914},
doi = {10.1145/3437992.3439914},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HinrichsenLKB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HuC21,
author = {Jason Z. S. Hu and
Jacques Carette},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Formalizing category theory in Agda},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {327--342},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439922},
doi = {10.1145/3437992.3439922},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HuC21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KirstR21,
author = {Dominik Kirst and
Felix Rech},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {The generalised continuum hypothesis implies the axiom of choice in
Coq},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {313--326},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439932},
doi = {10.1145/3437992.3439932},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KirstR21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Laurent21,
author = {Olivier Laurent},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {An anti-locally-nameless approach to formalizing quantifiers},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {300--312},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439926},
doi = {10.1145/3437992.3439926},
timestamp = {Mon, 06 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Laurent21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Limperg21,
author = {Jannis Limperg},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A novice-friendly induction tactic for lean},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {199--211},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439928},
doi = {10.1145/3437992.3439928},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Limperg21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LochmannMMF21,
author = {Alexander Lochmann and
Aart Middeldorp and
Fabian Mitterwallner and
Bertram Felgenhauer},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A verified decision procedure for the first-order theory of rewriting
for linear variable-separated rewrite systems},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {250--263},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439918},
doi = {10.1145/3437992.3439918},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LochmannMMF21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Loow21,
author = {Andreas L{\"{o}}{\"{o}}w},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Lutsig: a verified Verilog compiler for verified circuit development},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {46--60},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439916},
doi = {10.1145/3437992.3439916},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Loow21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MiraldoCMSS21,
author = {Victor Cacciari Miraldo and
Harold Carr and
Mark Moir and
Lisandra Silva and
Guy L. Steele Jr.},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Formal verification of authenticated, append-only skip lists in Agda},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {122--136},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439924},
doi = {10.1145/3437992.3439924},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MiraldoCMSS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Myreen21,
author = {Magnus O. Myreen},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A minimalistic verified bootstrapped compiler (proof pearl)},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {32--45},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439915},
doi = {10.1145/3437992.3439915},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Myreen21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Nipkow21,
author = {Tobias Nipkow},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Teaching algorithms and data structures with a proof assistant (invited
talk)},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {1--3},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439910},
doi = {10.1145/3437992.3439910},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Nipkow21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Sewell21,
author = {Peter Sewell},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Underpinning the foundations: sail-based semantics, testing, and reasoning
for production and CHERI-enabled architectures (invited talk)},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {4},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439911},
doi = {10.1145/3437992.3439911},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Sewell21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SlagelWD21,
author = {J. Tanner Slagel and
Lauren M. White and
Aaron Dutle},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Formal verification of semi-algebraic sets and real analytic functions},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {278--290},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439933},
doi = {10.1145/3437992.3439933},
timestamp = {Mon, 03 Jun 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SlagelWD21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TassarottiV0T21,
author = {Joseph Tassarotti and
Koundinya Vajjha and
Anindya Banerjee and
Jean{-}Baptiste Tristan},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A formal proof of {PAC} learnability for decision stumps},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {5--17},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439917},
doi = {10.1145/3437992.3439917},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/TassarottiV0T21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TimanyB21,
author = {Amin Timany and
Lars Birkedal},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Reasoning about monotonicity in separation logic},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {91--104},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439931},
doi = {10.1145/3437992.3439931},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/TimanyB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TourretB21,
author = {Sophie Tourret and
Jasmin Blanchette},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A modular Isabelle framework for verifying saturation provers},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {224--237},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439912},
doi = {10.1145/3437992.3439912},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/TourretB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/VajjhaSTPF21,
author = {Koundinya Vajjha and
Avraham Shinnar and
Barry M. Trager and
Vasily Pestun and
Nathan Fulton},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {CertRL: formalizing convergence proofs for value and policy iteration
in Coq},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {18--31},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439927},
doi = {10.1145/3437992.3439927},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/VajjhaSTPF21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/VindumB21,
author = {Simon Friis Vindum and
Lars Birkedal},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {Contextual refinement of the Michael-Scott queue (proof pearl)},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {76--90},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439930},
doi = {10.1145/3437992.3439930},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/VindumB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2021,
editor = {Catalin Hritcu and
Andrei Popescu},
title = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992},
doi = {10.1145/3437992},
isbn = {978-1-4503-8299-1},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2021.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/00020G20,
author = {David Butler and
David Aspinall and
Adri{\`{a}} Gasc{\'{o}}n},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Formalising oblivious transfer in the semi-honest and malicious model
in CryptHOL},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {229--243},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373815},
doi = {10.1145/3372885.3373815},
timestamp = {Sun, 02 Oct 2022 15:58:04 +0200},
biburl = {https://dblp.org/rec/conf/cpp/00020G20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/0002KW20,
author = {Yannick Forster and
Fabian Kunze and
Maxi Wuttke},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Verified programming of Turing machines in Coq},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {114--128},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373816},
doi = {10.1145/3372885.3373816},
timestamp = {Fri, 31 Mar 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/0002KW20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/0002S20,
author = {Yannick Forster and
Kathrin Stark},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Coq {\`{a}} la carte: a practical approach to modular syntax with
binders},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {186--200},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373817},
doi = {10.1145/3372885.3373817},
timestamp = {Sat, 05 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/0002S20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AltmanningerP20,
author = {Johannes Altmanninger and
Adrian Rebola{-}Pardo},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Frying the egg, roasting the chicken: unit deletions in {DRAT} proofs},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {61--70},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373821},
doi = {10.1145/3372885.3373821},
timestamp = {Wed, 30 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AltmanningerP20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AnnenkovNS20,
author = {Danil Annenkov and
Jakob Botsch Nielsen and
Bas Spitters},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {ConCert: a smart contract certification framework in Coq},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {215--228},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373829},
doi = {10.1145/3372885.3373829},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AnnenkovNS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BlaudeauS20,
author = {Clement Blaudeau and
Natarajan Shankar},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {A verified packrat parser interpreter for parsing expression grammars},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {3--17},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373836},
doi = {10.1145/3372885.3373836},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BlaudeauS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BuzzardCM20,
author = {Kevin Buzzard and
Johan Commelin and
Patrick Massot},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Formalising perfectoid spaces},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {299--312},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373830},
doi = {10.1145/3372885.3373830},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BuzzardCM20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Chlipala20,
author = {Adam Chlipala},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Proof assistants at the hardware-software interface (invited talk)},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {2},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3378575},
doi = {10.1145/3372885.3378575},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Chlipala20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DiazOT20,
author = {Tom{\'{a}}s D{\'{\i}}az and
Federico Olmedo and
{\'{E}}ric Tanter},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {A mechanized formalization of GraphQL},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {201--214},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373822},
doi = {10.1145/3372885.3373822},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DiazOT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoczkalP20,
author = {Christian Doczkal and
Damien Pous},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Completeness of an axiomatization of graph isomorphism via graph rewriting
in Coq},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {325--337},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373831},
doi = {10.1145/3372885.3373831},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DoczkalP20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FirsovBTL20,
author = {Denis Firsov and
Ahto Buldas and
Ahto Truu and
Risto Laanoja},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Verified security of {BLT} signature scheme},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {244--257},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373828},
doi = {10.1145/3372885.3373828},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FirsovBTL20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ForsbergXG20,
author = {Fredrik Nordvall Forsberg and
Chuangjie Xu and
Neil Ghani},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Three equivalent ordinal notation systems in cubical Agda},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {172--185},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373835},
doi = {10.1145/3372885.3373835},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ForsbergXG20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GoelSSS20,
author = {Shilpi Goel and
Anna Slobodov{\'{a}} and
Rob Sumners and
Sol Swords},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Verifying x86 instruction implementations},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {47--60},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373811},
doi = {10.1145/3372885.3373811},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/GoelSSS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HanD20,
author = {Jesse Michael Han and
Floris van Doorn},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {A formal proof of the independence of the continuum hypothesis},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {353--366},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373826},
doi = {10.1145/3372885.3373826},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/HanD20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ImmlerT20,
author = {Fabian Immler and
Yong Kiam Tan},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {The Poincar{\'{e}}-Bendixson theorem in Isabelle/HOL},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {338--352},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373833},
doi = {10.1145/3372885.3373833},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ImmlerT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LetanR20,
author = {Thomas Letan and
Yann R{\'{e}}gis{-}Gianas},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {FreeSpec: specifying, verifying, and executing impure computations
in Coq},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {32--46},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373812},
doi = {10.1145/3372885.3373812},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LetanR20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MortbergP20,
author = {Anders M{\"{o}}rtberg and
Lo{\"{\i}}c Pujet},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Cubical synthetic homotopy theory},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {158--171},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373825},
doi = {10.1145/3372885.3373825},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MortbergP20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/NipkowS20,
author = {Tobias Nipkow and
Thomas Sewell},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Proof pearl: Braun trees},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {18--31},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373834},
doi = {10.1145/3372885.3373834},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/NipkowS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Overbeek20,
author = {Roy Overbeek},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Formalizing determinacy of concurrent revisions},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {258--269},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373820},
doi = {10.1145/3372885.3373820},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Overbeek20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RingerSGL20,
author = {Talia Ringer and
Alex Sanchez{-}Stern and
Dan Grossman and
Sorin Lerner},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {REPLica: {REPL} instrumentation for Coq analysis},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {99--113},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373823},
doi = {10.1145/3372885.3373823},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/RingerSGL20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Rosu020,
author = {Grigore Rosu and
Xiaohong Chen},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Matching logic: the foundation of the {K} framework (invited talk)},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {1},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3378574},
doi = {10.1145/3372885.3378574},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Rosu020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RouvoetPKV20,
author = {Arjen Rouvoet and
Casper Bach Poulsen and
Robbert Krebbers and
Eelco Visser},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Intrinsically-typed definitional interpreters for linear, session-typed
languages},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {284--298},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373818},
doi = {10.1145/3372885.3373818},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/RouvoetPKV20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SinghN20,
author = {Abhishek Kr Singh and
Raja Natarajan},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {A constructive formalization of the weak perfect graph theorem},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {313--324},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373819},
doi = {10.1145/3372885.3373819},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SinghN20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Spies020,
author = {Simon Spies and
Yannick Forster},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Undecidability of higher-order unification formalised in Coq},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {143--157},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373832},
doi = {10.1145/3372885.3373832},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Spies020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TranMH20,
author = {Linh Tran and
Anshuman Mohan and
Aquinas Hobor},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {A functional proof pearl: inverting the Ackermann hierarchy},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {129--142},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373837},
doi = {10.1145/3372885.3373837},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/TranMH20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/VeltriV20,
author = {Niccol{\`{o}} Veltri and
Andrea Vezzosi},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Formalizing {\(\pi\)}-calculus in guarded cubical Agda},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {270--283},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373814},
doi = {10.1145/3372885.3373814},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/VeltriV20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WangBKU20,
author = {Qingxiang Wang and
Chad E. Brown and
Cezary Kaliszyk and
Josef Urban},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Exploration of neural machine translation in autoformalization of
mathematics in Mizar},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {85--98},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373827},
doi = {10.1145/3372885.3373827},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/WangBKU20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/X20,
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {The lean mathematical library},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {367--381},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373824},
doi = {10.1145/3372885.3373824},
timestamp = {Thu, 23 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/X20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ZakowskiHHZ20,
author = {Yannick Zakowski and
Paul He and
Chung{-}Kil Hur and
Steve Zdancewic},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {An equational theory for weak bisimulation via generalized parameterized
coinduction},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {71--84},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373813},
doi = {10.1145/3372885.3373813},
timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ZakowskiHHZ20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2020,
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885},
doi = {10.1145/3372885},
isbn = {978-1-4503-7097-4},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/2020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/0002KS19,
author = {Yannick Forster and
Dominik Kirst and
Gert Smolka},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {On synthetic undecidability in coq, with an application to the entscheidungsproblem},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {38--51},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294091},
doi = {10.1145/3293880.3294091},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/0002KS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BenzakenC19,
author = {V{\'{e}}ronique Benzaken and
Evelyne Contejean},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A Coq mechanised formal semantics for realistic {SQL} queries: formally
reconciling {SQL} and bag relational algebra},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {249--261},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294107},
doi = {10.1145/3293880.3294107},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BenzakenC19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Blanchette19,
author = {Jasmin Christian Blanchette},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Formalizing the metatheory of logical calculi and automatic provers
in Isabelle/HOL (invited talk)},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {1--13},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294087},
doi = {10.1145/3293880.3294087},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Blanchette19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BlazyH19,
author = {Sandrine Blazy and
R{\'{e}}mi Hutin},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Formal verification of a program obfuscation based on mixed Boolean-arithmetic
expressions},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {196--208},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294103},
doi = {10.1145/3293880.3294103},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BlazyH19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ChaudhuriM019,
author = {Kaustuv Chaudhuri and
Matteo Manighetti and
Dale Miller},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A proof-theoretic approach to certifying skolemization},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {78--90},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294094},
doi = {10.1145/3293880.3294094},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ChaudhuriM019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Eberl19,
author = {Manuel Eberl},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Verified solving and asymptotics of linear recurrences},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {27--37},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294090},
doi = {10.1145/3293880.3294090},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Eberl19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FelgenhauerMPR19,
author = {Bertram Felgenhauer and
Aart Middeldorp and
T. V. H. Prathamesh and
Franziska Rapp},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A verified ground confluence tool for linear variable-separated rewrite
systems in Isabelle/HOL},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {132--143},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294098},
doi = {10.1145/3293880.3294098},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FelgenhauerMPR19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Felty19,
author = {Amy P. Felty},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A linear logical framework in hybrid (invited talk)},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {14},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294088},
doi = {10.1145/3293880.3294088},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Felty19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ForsterL19,
author = {Yannick Forster and
Dominique Larchey{-}Wendling},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Certified undecidability of intuitionistic linear logic via binary
stack machines and minsky machines},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {104--117},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294096},
doi = {10.1145/3293880.3294096},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ForsterL19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ForsterSSS19,
author = {Yannick Forster and
Steven Sch{\"{a}}fer and
Simon Spies and
Kathrin Stark},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Call-by-push-value in coq: operational, equational, and denotational
theory},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {118--131},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294097},
doi = {10.1145/3293880.3294097},
timestamp = {Sat, 05 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ForsterSSS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ImmlerZ19,
author = {Fabian Immler and
Bohua Zhan},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Smooth manifolds and types to sets for linear algebra in Isabelle/HOL},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {65--77},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294093},
doi = {10.1145/3293880.3294093},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ImmlerZ19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Koh0LXBHMPZ19,
author = {Nicolas Koh and
Yao Li and
Yishuai Li and
Li{-}yao Xia and
Lennart Beringer and
Wolf Honor{\'{e}} and
William Mansky and
Benjamin C. Pierce and
Steve Zdancewic},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {From {C} to interaction trees: specifying, verifying, and testing
a networked server},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {234--248},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294106},
doi = {10.1145/3293880.3294106},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Koh0LXBHMPZ19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Lewis19,
author = {Robert Y. Lewis},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A formal proof of hensel's lemma over the p-adic integers},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {15--26},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294089},
doi = {10.1145/3293880.3294089},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Lewis19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LiP19,
author = {Wenda Li and
Lawrence C. Paulson},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier
theorem},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {52--64},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294092},
doi = {10.1145/3293880.3294092},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LiP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LochmannS19,
author = {Alexander Lochmann and
Christian Sternagel},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Certified {ACKBO}},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {144--151},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294099},
doi = {10.1145/3293880.3294099},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LochmannS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ManskyG19,
author = {Susannah Mansky and
Elsa L. Gunter},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Dynamic class initialization semantics: a jinja extension},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {209--221},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294104},
doi = {10.1145/3293880.3294104},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ManskyG19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RoessleVR19,
author = {Ian Roessle and
Freek Verbeek and
Binoy Ravindran},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Formally verified big step semantics out of x86-64 binaries},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {181--195},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294102},
doi = {10.1145/3293880.3294102},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/RoessleVR19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchlichtkrullBT19,
author = {Anders Schlichtkrull and
Jasmin Christian Blanchette and
Dmitriy Traytel},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A verified prover based on ordered resolution},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {152--165},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294100},
doi = {10.1145/3293880.3294100},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SchlichtkrullBT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/StarkSK19,
author = {Kathrin Stark and
Steven Sch{\"{a}}fer and
Jonas Kaiser},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector
substitutions},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {166--180},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294101},
doi = {10.1145/3293880.3294101},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/StarkSK19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WinterhalterST19,
author = {Th{\'{e}}o Winterhalter and
Matthieu Sozeau and
Nicolas Tabareau},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Eliminating reflection from type theory},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {91--103},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294095},
doi = {10.1145/3293880.3294095},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WinterhalterST19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/YeD19,
author = {Qianchuan Ye and
Benjamin Delaware},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A verified protocol buffer compiler},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {222--233},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294105},
doi = {10.1145/3293880.3294105},
timestamp = {Tue, 07 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/YeD19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2019,
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
publisher = {{ACM}},
year = {2019},
url = {https://dl.acm.org/citation.cfm?id=3293880},
isbn = {978-1-4503-6222-1},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AmaniBBS18,
author = {Sidney Amani and
Myriam B{\'{e}}gel and
Maksym Bortin and
Mark Staples},
editor = {June Andronick and
Amy P. Felty},
title = {Towards verifying ethereum smart contract bytecode in Isabelle/HOL},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {66--77},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167084},
doi = {10.1145/3167084},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AmaniBBS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BonacinaGS18,
author = {Maria Paola Bonacina and
St{\'{e}}phane Graham{-}Lengrand and
Natarajan Shankar},
editor = {June Andronick and
Amy P. Felty},
title = {Proofs in conflict-driven theory combination},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {186--200},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167096},
doi = {10.1145/3167096},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BonacinaGS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Chaudhuri18,
author = {Kaustuv Chaudhuri},
editor = {June Andronick and
Amy P. Felty},
title = {A two-level logic perspective on (simultaneous) substitutions},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {280--292},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167093},
doi = {10.1145/3167093},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Chaudhuri18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DivasonJKT018,
author = {Jose Divas{\'{o}}n and
Sebastiaan J. C. Joosten and
Ondrej Kuncar and
Ren{\'{e}} Thiemann and
Akihisa Yamada},
editor = {June Andronick and
Amy P. Felty},
title = {Efficient certification of complexity proofs: formalizing the Perron-Frobenius
theorem (invited talk paper)},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {2--13},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167103},
doi = {10.1145/3167103},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DivasonJKT018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Djalal18,
author = {Boris Djalal},
editor = {June Andronick and
Amy P. Felty},
title = {A constructive formalisation of Semi-algebraic sets and functions},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {240--251},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167099},
doi = {10.1145/3167099},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Djalal18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoczkalB18,
author = {Christian Doczkal and
Joachim Bard},
editor = {June Andronick and
Amy P. Felty},
title = {Completeness and decidability of converse {PDL} in the constructive
type theory of Coq},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {42--52},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167088},
doi = {10.1145/3167088},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/DoczkalB18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FereeHMMN18,
author = {Hugo F{\'{e}}r{\'{e}}e and
Samuel Hym and
Micaela Mayero and
Jean{-}Yves Moyen and
David Nowak},
editor = {June Andronick and
Amy P. Felty},
title = {Formal proof of polynomial-time complexity with quasi-interpretations},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {146--157},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167097},
doi = {10.1145/3167097},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FereeHMMN18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FirsovS18,
author = {Denis Firsov and
Aaron Stump},
editor = {June Andronick and
Amy P. Felty},
title = {Generic derivation of induction for impredicative encodings in Cedille},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {215--227},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167087},
doi = {10.1145/3167087},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FirsovS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FleuryBL18,
author = {Mathias Fleury and
Jasmin Christian Blanchette and
Peter Lammich},
editor = {June Andronick and
Amy P. Felty},
title = {A verified {SAT} solver with watched literals using imperative {HOL}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {158--171},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167080},
doi = {10.1145/3167080},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FleuryBL18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FruminGGW18,
author = {Dan Frumin and
Herman Geuvers and
L{\'{e}}on Gondelman and
Niels van der Weide},
editor = {June Andronick and
Amy P. Felty},
title = {Finite sets in homotopy type theory},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {201--214},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167085},
doi = {10.1145/3167085},
timestamp = {Sat, 05 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FruminGGW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GrimmMFHMPRRSB18,
author = {Niklas Grimm and
Kenji Maillard and
C{\'{e}}dric Fournet and
Catalin Hritcu and
Matteo Maffei and
Jonathan Protzenko and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Santiago Zanella B{\'{e}}guelin},
editor = {June Andronick and
Amy P. Felty},
title = {A monadic framework for relational verification: applied to information
security, program equivalence, and optimizations},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {130--145},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167090},
doi = {10.1145/3167090},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/GrimmMFHMPRRSB18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaiserSS18,
author = {Jonas Kaiser and
Steven Sch{\"{a}}fer and
Kathrin Stark},
editor = {June Andronick and
Amy P. Felty},
title = {Binder aware recursion over well-scoped de Bruijn syntax},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {293--306},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167098},
doi = {10.1145/3167098},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaiserSS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaliszykP18,
author = {Cezary Kaliszyk and
Julian Parsert},
editor = {June Andronick and
Amy P. Felty},
title = {Formal microeconomic foundations and the first welfare theorem},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {91--101},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167100},
doi = {10.1145/3167100},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaliszykP18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KirstS18,
author = {Dominik Kirst and
Gert Smolka},
editor = {June Andronick and
Amy P. Felty},
title = {Large model constructions for second-order {ZF} in dependent type
theory},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {228--239},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167095},
doi = {10.1145/3167095},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KirstS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LengletS18,
author = {Sergue{\"{\i}} Lenglet and
Alan Schmitt},
editor = {June Andronick and
Amy P. Felty},
title = {HO{\(\pi\)} in Coq},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {252--265},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167083},
doi = {10.1145/3167083},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LengletS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/McLaughlinMS18,
author = {Craig McLaughlin and
James McKinna and
Ian Stark},
editor = {June Andronick and
Amy P. Felty},
title = {Triangulating context lemmas},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {102--114},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167081},
doi = {10.1145/3167081},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/McLaughlinMS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MullenPWTG18,
author = {Eric Mullen and
Stuart Pernsteiner and
James R. Wilcox and
Zachary Tatlock and
Dan Grossman},
editor = {June Andronick and
Amy P. Felty},
title = {{\OE}uf: minimizing the Coq extraction {TCB}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {172--185},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167089},
doi = {10.1145/3167089},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MullenPWTG18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Pientka18,
author = {Brigitte Pientka},
editor = {June Andronick and
Amy P. Felty},
title = {POPLMark reloaded: mechanizing logical relations proofs (invited talk)},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {1},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167102},
doi = {10.1145/3167102},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Pientka18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PirleaS18,
author = {George P{\^{\i}}rlea and
Ilya Sergey},
editor = {June Andronick and
Amy P. Felty},
title = {Mechanising blockchain consensus},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {78--90},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167086},
doi = {10.1145/3167086},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/PirleaS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RingerYLG18,
author = {Talia Ringer and
Nathaniel Yazdani and
John Leo and
Dan Grossman},
editor = {June Andronick and
Amy P. Felty},
title = {Adapting proof automation to adapt proofs},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {115--129},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167094},
doi = {10.1145/3167094},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/RingerYLG18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Rouhling18,
author = {Damien Rouhling},
editor = {June Andronick and
Amy P. Felty},
title = {A formal proof in Coq of a control function for the inverted pendulum},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {28--41},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167101},
doi = {10.1145/3167101},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Rouhling18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Spector-Zabusky18,
author = {Antal Spector{-}Zabusky and
Joachim Breitner and
Christine Rizkallah and
Stephanie Weirich},
editor = {June Andronick and
Amy P. Felty},
title = {Total Haskell is reasonable Coq},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {14--27},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167092},
doi = {10.1145/3167092},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Spector-Zabusky18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Watt18,
author = {Conrad Watt},
editor = {June Andronick and
Amy P. Felty},
title = {Mechanising and verifying the WebAssembly specification},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {53--65},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167082},
doi = {10.1145/3167082},
timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Watt18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WieczorekB18,
author = {Pawel Wieczorek and
Dariusz Biernacki},
editor = {June Andronick and
Amy P. Felty},
title = {A Coq formalization of normalization by evaluation for Martin-L{\"{o}}f
type theory},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {266--279},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167091},
doi = {10.1145/3167091},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WieczorekB18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2018,
editor = {June Andronick and
Amy P. Felty},
title = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
publisher = {{ACM}},
year = {2018},
url = {http://dl.acm.org/citation.cfm?id=3176245},
isbn = {978-1-4503-5586-5},
timestamp = {Sat, 30 Dec 2017 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AffeldtC17,
author = {Reynald Affeldt and
Cyril Cohen},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Formal foundations of 3D geometry to model robot manipulators},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {30--42},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018629},
doi = {10.1145/3018610.3018629},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AffeldtC17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Allais0MM17,
author = {Guillaume Allais and
James Chapman and
Conor McBride and
James McKinna},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Type-and-scope safe programs and their proofs},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {195--207},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018613},
doi = {10.1145/3018610.3018613},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Allais0MM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AmaniABLRT17,
author = {Sidney Amani and
June Andronick and
Maksym Bortin and
Corey Lewis and
Christine Rizkallah and
Joseph Tuong},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Complx: a verification framework for concurrent imperative programs},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {138--150},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018627},
doi = {10.1145/3018610.3018627},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AmaniABLRT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BauerGLSSS17,
author = {Andrej Bauer and
Jason Gross and
Peter LeFanu Lumsdaine and
Michael Shulman and
Matthieu Sozeau and
Bas Spitters},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {The HoTT library: a formalization of homotopy type theory in Coq},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {164--172},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018615},
doi = {10.1145/3018610.3018615},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BauerGLSSS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BohrerRVVP17,
author = {Rose Bohrer and
Vincent Rahli and
Ivana Vukotic and
Marcus V{\"{o}}lp and
Andr{\'{e}} Platzer},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Formally verified differential dynamic logic},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {208--221},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018616},
doi = {10.1145/3018610.3018616},
timestamp = {Tue, 10 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BohrerRVVP17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoldoCFMM17,
author = {Sylvie Boldo and
Fran{\c{c}}ois Cl{\'{e}}ment and
Florian Faissole and
Vincent Martin and
Micaela Mayero},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {A Coq formal proof of the LaxMilgram theorem},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {79--89},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018625},
doi = {10.1145/3018610.3018625},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BoldoCFMM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoulierPT17,
author = {Simon Boulier and
Pierre{-}Marie P{\'{e}}drot and
Nicolas Tabareau},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {The next 700 syntactical models of type theory},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {182--194},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018620},
doi = {10.1145/3018610.3018620},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BoulierPT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CockxD17,
author = {Jesper Cockx and
Dominique Devriese},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Lifting proof-relevant unification to higher dimensions},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {173--181},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018612},
doi = {10.1145/3018610.3018612},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CockxD17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DivasonJT017,
author = {Jose Divas{\'{o}}n and
Sebastiaan J. C. Joosten and
Ren{\'{e}} Thiemann and
Akihisa Yamada},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {A formalization of the Berlekamp-Zassenhaus factorization algorithm},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {17--29},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018617},
doi = {10.1145/3018610.3018617},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DivasonJT017.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Feng17,
author = {Xinyu Feng},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Mechanized verification of preemptive {OS} kernels (invited talk)},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {2},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3023367},
doi = {10.1145/3018610.3023367},
timestamp = {Mon, 28 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Feng17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FoxMTK17,
author = {Anthony C. J. Fox and
Magnus O. Myreen and
Yong Kiam Tan and
Ramana Kumar},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Verified compilation of CakeML to multiple machine-code targets},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {125--137},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018621},
doi = {10.1145/3018610.3018621},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FoxMTK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Gilbert17,
author = {Ga{\"{e}}tan Gilbert},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Formalising real numbers in homotopy type theory},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {112--124},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018614},
doi = {10.1145/3018610.3018614},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Gilbert17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Holzl17,
author = {Johannes H{\"{o}}lzl},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Markov processes in Isabelle/HOL},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {100--111},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018628},
doi = {10.1145/3018610.3018628},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Holzl17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/JakubuvU17,
author = {Jan Jakubuv and
Josef Urban},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {BliStrTune: hierarchical invention of theorem proving strategies},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {43--52},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018619},
doi = {10.1145/3018610.3018619},
timestamp = {Sun, 02 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/JakubuvU17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaiserTS17,
author = {Jonas Kaiser and
Tobias Tebbi and
Gert Smolka},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Equivalence of system f and {\'{z}}2 in Coq based on context
morphism lemmas},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {222--234},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018618},
doi = {10.1145/3018610.3018618},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaiserTS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ManskyPZD17,
author = {William Mansky and
Yuanfeng Peng and
Steve Zdancewic and
Joseph Devietti},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Verifying dynamic race detection},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {151--163},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018611},
doi = {10.1145/3018610.3018611},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ManskyPZD17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Martin-DorelR17,
author = {{\'{E}}rik Martin{-}Dorel and
Pierre Roux},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {A reflexive tactic for polynomial positivity using numerical solvers
and floating-point computations},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {90--99},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018622},
doi = {10.1145/3018610.3018622},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Martin-DorelR17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Paulson17,
author = {Lawrence C. Paulson},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Porting the {HOL} light analysis library: some lessons (invited talk)},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {1},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3023366},
doi = {10.1145/3018610.3023366},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Paulson17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Pottier17,
author = {Fran{\c{c}}ois Pottier},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Verifying a hash table and its iterators in higher-order separation
logic},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {3--16},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018624},
doi = {10.1145/3018610.3018624},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Pottier17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RoweB17,
author = {Reuben N. S. Rowe and
James Brotherston},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Automatic cyclic termination proofs for recursive procedures in separation
logic},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {53--65},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018623},
doi = {10.1145/3018610.3018623},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/RoweB17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/YamamotoSM17,
author = {Mitsuharu Yamamoto and
Shogo Sekine and
Saki Matsumoto},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Formalization of Karp-Miller tree construction on petri nets},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {66--78},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018626},
doi = {10.1145/3018610.3018626},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/YamamotoSM17.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}
}
@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/BlazyT16,
author = {Sandrine Blazy and
Alix Trieu},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Formal verification of control-flow graph flattening},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {176--187},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854082},
doi = {10.1145/2854065.2854082},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BlazyT16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Chargueraud16,
author = {Arthur Chargu{\'{e}}raud},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Higher-order representation predicates in separation logic},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {3--14},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854068},
doi = {10.1145/2854065.2854068},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Chargueraud16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CohenD16,
author = {Cyril Cohen and
Boris Djalal},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Formalization of a newton series representation of polynomials},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {100--109},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854075},
doi = {10.1145/2854065.2854075},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CohenD16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Czajka16,
author = {Lukasz Czajka},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Improving automation in interactive theorem provers by efficient encoding
of lambda-abstractions},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {49--57},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854069},
doi = {10.1145/2854065.2854069},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Czajka16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Doorn16,
author = {Floris van Doorn},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Constructing the propositional truncation using non-recursive HITs},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {122--129},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854076},
doi = {10.1145/2854065.2854076},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Doorn16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Friedman16,
author = {Harvey M. Friedman},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Perspectives on formal verification (invited talk)},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {1},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2858808},
doi = {10.1145/2854065.2858808},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Friedman16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FultonP16,
author = {Nathan Fulton and
Andr{\'{e}} Platzer},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {A logic of proofs for differential dynamic logic: toward independently
checkable proof certificates for dynamic logics},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {110--121},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854078},
doi = {10.1145/2854065.2854078},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FultonP16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaliszykPU16,
author = {Cezary Kaliszyk and
Karol Pak and
Josef Urban},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Towards a mizar environment for isabelle: foundations and language},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {58--65},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854070},
doi = {10.1145/2854065.2854070},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaliszykPU16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KotelnikovKRV16,
author = {Evgenii Kotelnikov and
Laura Kov{\'{a}}cs and
Giles Reger and
Andrei Voronkov},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {The vampire and the {FOOL}},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {37--48},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854071},
doi = {10.1145/2854065.2854071},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KotelnikovKRV16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Lammich16,
author = {Peter Lammich},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Refinement based verification of imperative data structures},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {27--36},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854067},
doi = {10.1145/2854065.2854067},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Lammich16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LiP16,
author = {Wenda Li and
Lawrence C. Paulson},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {A modular, efficient formalisation of real algebraic numbers},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {66--75},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854074},
doi = {10.1145/2854065.2854074},
timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LiP16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Moura16,
author = {Leonardo Mendon{\c{c}}a de Moura},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Dependent type practice (invited talk)},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {2},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2858809},
doi = {10.1145/2854065.2858809},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Moura16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PohjolaP16,
author = {Johannes {\AA}man Pohjola and
Joachim Parrow},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Bisimulation up-to techniques for psi-calculi},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {142--153},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854080},
doi = {10.1145/2854065.2854080},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/PohjolaP16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RahliB16,
author = {Vincent Rahli and
Mark Bickford},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {A nominal exploration of intuitionism},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {130--141},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854077},
doi = {10.1145/2854065.2854077},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/RahliB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RamananandroMML16,
author = {Tahina Ramananandro and
Paul Mountcastle and
Beno{\^{\i}}t Meister and
Richard Lethin},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {A unified Coq framework for verifying {C} programs with floating-point
computations},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {15--26},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854066},
doi = {10.1145/2854065.2854066},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/RamananandroMML16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchaferSS16,
author = {Steven Sch{\"{a}}fer and
Sigurd Schneider and
Gert Smolka},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Axiomatic semantics for compiler verification},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {188--196},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854083},
doi = {10.1145/2854065.2854083},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/SchaferSS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/St-MartinF16,
author = {Michel St{-}Martin and
Amy P. Felty},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {A verified algorithm for detecting conflicts in {XACML} access control
rules},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {166--175},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854079},
doi = {10.1145/2854065.2854079},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/St-MartinF16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Thiemann016,
author = {Ren{\'{e}} Thiemann and
Akihisa Yamada},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Formalizing jordan normal forms in Isabelle/HOL},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {88--99},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854073},
doi = {10.1145/2854065.2854073},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Thiemann016.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WoosWATEA16,
author = {Doug Woos and
James R. Wilcox and
Steve Anton and
Zachary Tatlock and
Michael D. Ernst and
Thomas E. Anderson},
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Planning for change in a formal verification of the raft consensus
protocol},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
pages = {154--165},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854081},
doi = {10.1145/2854065.2854081},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/WoosWATEA16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2016,
editor = {Jeremy Avigad and
Adam Chlipala},
title = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
publisher = {{ACM}},
year = {2016},
url = {http://dl.acm.org/citation.cfm?id=2854065},
isbn = {978-1-4503-4127-1},
timestamp = {Mon, 18 Jan 2016 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2016.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Asperti15,
author = {Andrea Asperti},
editor = {Xavier Leroy and
Alwen Tiu},
title = {The Speedup Theorem in a Primitive Recursive Framework},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {175--182},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693178},
doi = {10.1145/2676724.2693178},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Asperti15.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}
}
@inproceedings{DBLP:conf/cpp/BlazyMP15,
author = {Sandrine Blazy and
Andr{\'{e}} Maroneze and
David Pichardie},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Verified Validation of Program Slicing},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {109--117},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693169},
doi = {10.1145/2676724.2693169},
timestamp = {Mon, 16 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BlazyMP15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BodinJS15,
author = {Martin Bodin and
Thomas P. Jensen and
Alan Schmitt},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Certified Abstract Interpretation with Pretty-Big-Step Semantics},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {29--40},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693174},
doi = {10.1145/2676724.2693174},
timestamp = {Mon, 17 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/BodinJS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CaoFF15,
author = {Jingyuan Cao and
Ming Fu and
Xinyu Feng},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Practical Tactics for Verifying {C} Programs in Coq},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {97--108},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693162},
doi = {10.1145/2676724.2693162},
timestamp = {Mon, 28 Feb 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CaoFF15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ChaudhuriCM15,
author = {Kaustuv Chaudhuri and
Matteo Cimini and
Dale Miller},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Lightweight Formalization of the Metatheory of Bisimulation-Up-To},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {157--166},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693170},
doi = {10.1145/2676724.2693170},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ChaudhuriCM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Eberl15,
author = {Manuel Eberl},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {75--83},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693166},
doi = {10.1145/2676724.2693166},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Eberl15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FirsovU15,
author = {Denis Firsov and
Tarmo Uustalu},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Certified Normalization of Context-Free Grammars},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {167--174},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693177},
doi = {10.1145/2676724.2693177},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FirsovU15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GauthierK15,
author = {Thibault Gauthier and
Cezary Kaliszyk},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Premise Selection and External Provers for {HOL4}},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {49--57},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693173},
doi = {10.1145/2676724.2693173},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/GauthierK15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Immler15,
author = {Fabian Immler},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {129--136},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693164},
doi = {10.1145/2676724.2693164},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Immler15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/JiaLV15,
author = {Xiao Jia and
Wei Li and
Viktor Vafeiadis},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Proving Lock-Freedom Easily and Automatically},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {119--127},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693179},
doi = {10.1145/2676724.2693179},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/JiaLV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaliszykUV15,
author = {Cezary Kaliszyk and
Josef Urban and
Jir{\'{\i}} Vyskocil},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Certified Connection Tableaux Proofs for {HOL} Light and {TPTP}},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {59--66},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693176},
doi = {10.1145/2676724.2693176},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaliszykUV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KrebbersW15,
author = {Robbert Krebbers and
Freek Wiedijk},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Typed {C11} Semantics for Interactive Theorem Proving},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {15--27},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693571},
doi = {10.1145/2676724.2693571},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KrebbersW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kuncar15,
author = {Ondrej Kuncar},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading
in Proof Assistants},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {85--94},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693175},
doi = {10.1145/2676724.2693175},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Kuncar15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LammichN15,
author = {Peter Lammich and
Ren{\'{e}} Neumann},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Framework for Verifying Depth-First Search Algorithms},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {137--146},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693165},
doi = {10.1145/2676724.2693165},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/LammichN15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RamananandroSWKF15,
author = {Tahina Ramananandro and
Zhong Shao and
Shu{-}Chun Weng and
J{\'{e}}r{\'{e}}mie Koenig and
Yuchen Fu},
editor = {Xavier Leroy and
Alwen Tiu},
title = {A Compositional Semantics for Verified Separate Compilation and Linking},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {3--14},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693167},
doi = {10.1145/2676724.2693167},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/RamananandroSWKF15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchaferST15,
author = {Steven Sch{\"{a}}fer and
Gert Smolka and
Tobias Tebbi},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Completeness and Decidability of de Bruijn Substitution Algebra in
Coq},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {67--73},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693163},
doi = {10.1145/2676724.2693163},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/SchaferST15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Shao15,
author = {Zhong Shao},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Clean-Slate Development of Certified {OS} Kernels},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {95--96},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693180},
doi = {10.1145/2676724.2693180},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Shao15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SternagelWZ15,
author = {Thomas Sternagel and
Sarah Winkler and
Harald Zankl},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Recording Completion for Certificates in Equational Reasoning},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {41--47},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693171},
doi = {10.1145/2676724.2693171},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/SternagelWZ15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Vafeiadis15,
author = {Viktor Vafeiadis},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Formal Reasoning about the {C11} Weak Memory Model},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {1--2},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693181},
doi = {10.1145/2676724.2693181},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Vafeiadis15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2015,
editor = {Xavier Leroy and
Alwen Tiu},
title = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
publisher = {{ACM}},
year = {2015},
url = {http://dl.acm.org/citation.cfm?id=2676724},
isbn = {978-1-4503-3296-5},
timestamp = {Thu, 22 Jan 2015 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2015.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/0001HN13,
author = {Andrei Popescu and
Johannes H{\"{o}}lzl and
Tobias Nipkow},
editor = {Georges Gonthier and
Michael Norrish},
title = {Formalizing Probabilistic Noninterference},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {259--275},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_17},
doi = {10.1007/978-3-319-03545-1\_17},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/0001HN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Asperti13,
author = {Andrea Asperti},
editor = {Georges Gonthier and
Michael Norrish},
title = {A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {163--177},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_11},
doi = {10.1007/978-3-319-03545-1\_11},
timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Asperti13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BelangerMP13,
author = {Olivier Savary B{\'{e}}langer and
Stefan Monnier and
Brigitte Pientka},
editor = {Georges Gonthier and
Michael Norrish},
title = {Programming Type-Safe Transformations Using Higher-Order Abstract
Syntax},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {243--258},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_16},
doi = {10.1007/978-3-319-03545-1\_16},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BelangerMP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Bell13,
author = {Christian J. Bell},
editor = {Georges Gonthier and
Michael Norrish},
title = {Certifiably Sound Parallelizing Transformations},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {227--242},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_15},
doi = {10.1007/978-3-319-03545-1\_15},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Bell13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CohenDM13,
author = {Cyril Cohen and
Maxime D{\'{e}}n{\`{e}}s and
Anders M{\"{o}}rtberg},
editor = {Georges Gonthier and
Michael Norrish},
title = {Refinements for Free!},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {147--162},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_10},
doi = {10.1007/978-3-319-03545-1\_10},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CohenDM13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoczkalKS13,
author = {Christian Doczkal and
Jan{-}Oliver Kaiser and
Gert Smolka},
editor = {Georges Gonthier and
Michael Norrish},
title = {A Constructive Theory of Regular Languages in Coq},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {82--97},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_6},
doi = {10.1007/978-3-319-03545-1\_6},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DoczkalKS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoddsA13,
author = {Josiah Dodds and
Andrew W. Appel},
editor = {Georges Gonthier and
Michael Norrish},
title = {Mostly Sound Type System Improves a Foundational Program Verifier},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {17--32},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_2},
doi = {10.1007/978-3-319-03545-1\_2},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DoddsA13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FirsovU13,
author = {Denis Firsov and
Tarmo Uustalu},
editor = {Georges Gonthier and
Michael Norrish},
title = {Certified Parsing of Regular Languages},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {98--113},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_7},
doi = {10.1007/978-3-319-03545-1\_7},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FirsovU13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HuangM13,
author = {Daniel Huang and
Greg Morrisett},
editor = {Georges Gonthier and
Michael Norrish},
title = {Formalizing the SAFECode Type System},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {211--226},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_14},
doi = {10.1007/978-3-319-03545-1\_14},
timestamp = {Sun, 12 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HuangM13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HuffmanK13,
author = {Brian Huffman and
Ondrej Kuncar},
editor = {Georges Gonthier and
Michael Norrish},
title = {Lifting and Transfer: {A} Modular Design for Quotients in Isabelle/HOL},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {131--146},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_9},
doi = {10.1007/978-3-319-03545-1\_9},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HuffmanK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KhakpourSD13,
author = {Narges Khakpour and
Oliver Schwarz and
Mads Dam},
editor = {Georges Gonthier and
Michael Norrish},
title = {Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {276--291},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_18},
doi = {10.1007/978-3-319-03545-1\_18},
timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KhakpourSD13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Krebbers13,
author = {Robbert Krebbers},
editor = {Georges Gonthier and
Michael Norrish},
title = {Aliasing Restrictions of {C11} Formalized in Coq},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {50--65},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_4},
doi = {10.1007/978-3-319-03545-1\_4},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Krebbers13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LicataB13,
author = {Daniel R. Licata and
Guillaume Brunerie},
editor = {Georges Gonthier and
Michael Norrish},
title = {{\(\pi\)} n {(S} n {)} in Homotopy Type Theory},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {1--16},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_1},
doi = {10.1007/978-3-319-03545-1\_1},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/LicataB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MillerT13,
author = {Dale Miller and
Alwen Tiu},
editor = {Georges Gonthier and
Michael Norrish},
title = {Extracting Proofs from Tabled Proof Search},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {194--210},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_13},
doi = {10.1007/978-3-319-03545-1\_13},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/MillerT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MyreenC13,
author = {Magnus O. Myreen and
Gregorio Curello},
editor = {Georges Gonthier and
Michael Norrish},
title = {Proof Pearl: {A} Verified Bignum Implementation in x86-64 Machine
Code},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {66--81},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_5},
doi = {10.1007/978-3-319-03545-1\_5},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/MyreenC13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchroppP13,
author = {Andreas Schropp and
Andrei Popescu},
editor = {Georges Gonthier and
Michael Norrish},
title = {Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {114--130},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_8},
doi = {10.1007/978-3-319-03545-1\_8},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SchroppP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Sternagel13,
author = {Christian Sternagel},
editor = {Georges Gonthier and
Michael Norrish},
title = {Certified Kruskal's Tree Theorem},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {178--193},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_12},
doi = {10.1007/978-3-319-03545-1\_12},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Sternagel13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Stewart13,
author = {Gordon Stewart},
editor = {Georges Gonthier and
Michael Norrish},
title = {Computational Verification of Network Programs in Coq},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {33--49},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_3},
doi = {10.1007/978-3-319-03545-1\_3},
timestamp = {Tue, 14 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Stewart13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WuZU13,
author = {Chunhan Wu and
Xingyuan Zhang and
Christian Urban},
editor = {Georges Gonthier and
Michael Norrish},
title = {A Formal Model and Correctness Proof for an Access Control Policy
Framework},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {292--307},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_19},
doi = {10.1007/978-3-319-03545-1\_19},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WuZU13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2013,
editor = {Georges Gonthier and
Michael Norrish},
title = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1},
doi = {10.1007/978-3-319-03545-1},
isbn = {978-3-319-03544-4},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/2013.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Accattoli12,
author = {Beniamino Accattoli},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Proof Pearl: Abella Formalization of {\(\lambda\)}-Calculus Cube Property},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {173--187},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_15},
doi = {10.1007/978-3-642-35308-6\_15},
timestamp = {Wed, 07 Dec 2022 23:14:04 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Accattoli12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/AspertiR12,
author = {Andrea Asperti and
Wilmer Ricciotti},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Rating Disambiguation Errors},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {240--255},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_19},
doi = {10.1007/978-3-642-35308-6\_19},
timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/AspertiR12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BartheGKLB12,
author = {Gilles Barthe and
Benjamin Gr{\'{e}}goire and
C{\'{e}}sar Kunz and
Yassine Lakhnech and
Santiago Zanella B{\'{e}}guelin},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {7--8},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_3},
doi = {10.1007/978-3-642-35308-6\_3},
timestamp = {Sun, 25 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BartheGKLB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoldoLM12,
author = {Sylvie Boldo and
Catherine Lelay and
Guillaume Melquiond},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Improving Real Analysis in Coq: {A} User-Friendly Approach to Integrals
and Derivatives},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {289--304},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_22},
doi = {10.1007/978-3-642-35308-6\_22},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BoldoLM12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Bulwahn12,
author = {Lukas Bulwahn},
editor = {Chris Hawblitzel and
Dale Miller},
title = {The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic
Testing under One Roof},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {92--108},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_10},
doi = {10.1007/978-3-642-35308-6\_10},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Bulwahn12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Campbell12,
author = {Brian Campbell},
editor = {Chris Hawblitzel and
Dale Miller},
title = {An Executable Semantics for CompCert {C}},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {60--75},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_8},
doi = {10.1007/978-3-642-35308-6\_8},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Campbell12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ChanN12,
author = {Hing{-}Lun Chan and
Michael Norrish},
editor = {Chris Hawblitzel and
Dale Miller},
title = {A String of Pearls: Proofs of Fermat's Little Theorem},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {188--207},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_16},
doi = {10.1007/978-3-642-35308-6\_16},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/ChanN12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Chaudhuri12,
author = {Kaustuv Chaudhuri},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Compact Proof Certificates for Linear Logic},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {208--223},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_17},
doi = {10.1007/978-3-642-35308-6\_17},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Chaudhuri12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CoquandMS12,
author = {Thierry Coquand and
Anders M{\"{o}}rtberg and
Vincent Siles},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Coherent and Strongly Discrete Rings in Type Theory},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {273--288},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_21},
doi = {10.1007/978-3-642-35308-6\_21},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CoquandMS12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoczkalS12,
author = {Christian Doczkal and
Gert Smolka},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Constructive Completeness for Modal Logic with Transitive Closure},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {224--239},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_18},
doi = {10.1007/978-3-642-35308-6\_18},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DoczkalS12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kobayashi12,
author = {Naoki Kobayashi},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Program Certification by Higher-Order Model Checking},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {9--10},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_4},
doi = {10.1007/978-3-642-35308-6\_4},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Kobayashi12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Leroy12,
author = {Xavier Leroy},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Mechanized Semantics for Compiler Verification},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {4--6},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_2},
doi = {10.1007/978-3-642-35308-6\_2},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Leroy12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Morrisett12,
author = {Greg Morrisett},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Scalable Formal Machine Models},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {1--3},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_1},
doi = {10.1007/978-3-642-35308-6\_1},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Morrisett12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MulliganC12,
author = {Dominic P. Mulligan and
Claudio Sacerdoti Coen},
editor = {Chris Hawblitzel and
Dale Miller},
title = {On the Correctness of an Optimising Assembler for the Intel {MCS-51}
Microprocessor},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {43--59},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_7},
doi = {10.1007/978-3-642-35308-6\_7},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MulliganC12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MurrayMBGK12,
author = {Toby C. Murray and
Daniel Matichuk and
Matthew Brassil and
Peter Gammie and
Gerwin Klein},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Noninterference for Operating System Kernels},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {126--142},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_12},
doi = {10.1007/978-3-642-35308-6\_12},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/MurrayMBGK12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Nakano12,
author = {Keisuke Nakano},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Shall We Juggle, Coinductively?},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {160--172},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_14},
doi = {10.1007/978-3-642-35308-6\_14},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Nakano12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Neron12,
author = {Pierre Neron},
editor = {Chris Hawblitzel and
Dale Miller},
title = {A Formal Proof of Square Root and Division Elimination in Embedded
Programs},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {256--272},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_20},
doi = {10.1007/978-3-642-35308-6\_20},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Neron12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PopescuHN12,
author = {Andrei Popescu and
Johannes H{\"{o}}lzl and
Tobias Nipkow},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Proving Concurrent Noninterference},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {109--125},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_11},
doi = {10.1007/978-3-642-35308-6\_11},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/PopescuHN12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/RobertL12,
author = {Valentin Robert and
Xavier Leroy},
editor = {Chris Hawblitzel and
Dale Miller},
title = {A Formally-Verified Alias Analysis},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {11--26},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_5},
doi = {10.1007/978-3-642-35308-6\_5},
timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/RobertL12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TollitteDD12,
author = {Pierre{-}Nicolas Tollitte and
David Delahaye and
Catherine Dubois},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Producing Certified Functional Code from Inductive Specifications},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {76--91},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_9},
doi = {10.1007/978-3-642-35308-6\_9},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/TollitteDD12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/VaynbergS12,
author = {Alexander Vaynberg and
Zhong Shao},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Compositional Verification of a Baby Virtual Memory Manager},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {143--159},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_13},
doi = {10.1007/978-3-642-35308-6\_13},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/VaynbergS12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ZhaoZ12,
author = {Jianzhou Zhao and
Steve Zdancewic},
editor = {Chris Hawblitzel and
Dale Miller},
title = {Mechanized Verification of Computing Dominators for Formalizing Compilers},
booktitle = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
pages = {27--42},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6\_6},
doi = {10.1007/978-3-642-35308-6\_6},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ZhaoZ12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2012,
editor = {Chris Hawblitzel and
Dale Miller},
title = {Certified Programs and Proofs - Second International Conference, {CPP}
2012, Kyoto, Japan, December 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7679},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35308-6},
doi = {10.1007/978-3-642-35308-6},
isbn = {978-3-642-35307-9},
timestamp = {Wed, 07 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Appel11,
author = {Andrew W. Appel},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {VeriSmall: Verified Smallfoot Shape Analysis},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {231--246},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_18},
doi = {10.1007/978-3-642-25379-9\_18},
timestamp = {Thu, 14 Oct 2021 10:14:33 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Appel11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ArmandFGKTW11,
author = {Micha{\"{e}}l Armand and
Germain Faure and
Benjamin Gr{\'{e}}goire and
Chantal Keller and
Laurent Th{\'{e}}ry and
Benjamin Werner},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {A Modular Integration of {SAT/SMT} Solvers to Coq through Proof Witnesses},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {135--150},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_12},
doi = {10.1007/978-3-642-25379-9\_12},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ArmandFGKTW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BackesHT11,
author = {Michael Backes and
Catalin Hritcu and
Thorsten Tarrach},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Automatically Verifying Typing Constraints for a Data Processing Language},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {296--313},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_22},
doi = {10.1007/978-3-642-25379-9\_22},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BackesHT11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BessonCP11,
author = {Fr{\'{e}}d{\'{e}}ric Besson and
Pierre{-}Emmanuel Cornilleau and
David Pichardie},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Modular {SMT} Proofs for Fast Reflexive Checking Inside Coq},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {151--166},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_13},
doi = {10.1007/978-3-642-25379-9\_13},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BessonCP11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Bjorner11,
author = {Nikolaj S. Bj{\o}rner},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Engineering Theories with {Z3}},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {1--2},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_1},
doi = {10.1007/978-3-642-25379-9\_1},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Bjorner11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BoespflugDG11,
author = {Mathieu Boespflug and
Maxime D{\'{e}}n{\`{e}}s and
Benjamin Gr{\'{e}}goire},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Full Reduction at Full Throttle},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {362--377},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_26},
doi = {10.1007/978-3-642-25379-9\_26},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BoespflugDG11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BohmeFSW11,
author = {Sascha B{\"{o}}hme and
Anthony C. J. Fox and
Thomas Sewell and
Tjark Weber},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Reconstruction of Z3's Bit-Vector Proofs in {HOL4} and Isabelle/HOL},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {183--198},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_15},
doi = {10.1007/978-3-642-25379-9\_15},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BohmeFSW11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Braibant11,
author = {Thomas Braibant},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Coquet: {A} Coq Library for Verifying Hardware},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {330--345},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_24},
doi = {10.1007/978-3-642-25379-9\_24},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Braibant11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/BraibantP11,
author = {Thomas Braibant and
Damien Pous},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Tactics for Reasoning Modulo {AC} in Coq},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {167--182},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_14},
doi = {10.1007/978-3-642-25379-9\_14},
timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/BraibantP11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CheneyU11,
author = {James Cheney and
Christian Urban},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Mechanizing the Metatheory of mini-XQuery},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {280--295},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_21},
doi = {10.1007/978-3-642-25379-9\_21},
timestamp = {Wed, 07 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/CheneyU11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CoquandS11,
author = {Thierry Coquand and
Vincent Siles},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {A Decision Procedure for Regular Expression Equivalence in Type Theory},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {119--134},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_11},
doi = {10.1007/978-3-642-25379-9\_11},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CoquandS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/CorbineauDL11,
author = {Pierre Corbineau and
Mathilde Duclos and
Yassine Lakhnech},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Certified Security Proofs of Cryptographic Protocols in the Computational
Model: An Application to Intrusion Resilience},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {378--393},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_27},
doi = {10.1007/978-3-642-25379-9\_27},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/CorbineauDL11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DoczkalS11,
author = {Christian Doczkal and
Gert Smolka},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Constructive Formalization of Hybrid Logic with Eventualities},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {5--20},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_3},
doi = {10.1007/978-3-642-25379-9\_3},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DoczkalS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/GenevauxNS11,
author = {Jean{-}David G{\'{e}}nevaux and
Julien Narboux and
Pascal Schreck},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Formalization of Wu's Simple Method in Coq},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {71--86},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_8},
doi = {10.1007/978-3-642-25379-9\_8},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/GenevauxNS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HenzH11,
author = {Martin Henz and
Aquinas Hobor},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Teaching Experience: Logic and Formal Methods with Coq},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {199--215},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_16},
doi = {10.1007/978-3-642-25379-9\_16},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HenzH11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/JiangN11,
author = {Dongchen Jiang and
Tobias Nipkow},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Proof Pearl: The Marriage Theorem},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {394--399},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_28},
doi = {10.1007/978-3-642-25379-9\_28},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/JiangN11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kahl11,
author = {Wolfram Kahl},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {The Teaching Tool CalcCheck {A} Proof-Checker for Gries and Schneider's
"Logical Approach to Discrete Math"},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {216--230},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_17},
doi = {10.1007/978-3-642-25379-9\_17},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Kahl11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KaliszykB11,
author = {Cezary Kaliszyk and
Henk Barendregt},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Reasoning about Constants in Nominal Isabelle or How to Formalize
the Second Fixed Point Theorem},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {87--102},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_9},
doi = {10.1007/978-3-642-25379-9\_9},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/KaliszykB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KimR11,
author = {Jieung Kim and
Sukyoung Ryu},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Coq Mechanization of Featherweight Fortress with Multiple Dispatch
and Multiple Inheritance},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {264--279},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_20},
doi = {10.1007/978-3-642-25379-9\_20},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KimR11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/LeiQ11,
author = {Jinjiang Lei and
Zongyan Qiu},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Verification of Scalable Synchronous Queue},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {247--263},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_19},
doi = {10.1007/978-3-642-25379-9\_19},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/LeiQ11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Miller11,
author = {Dale Miller},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {A Proposal for Broad Spectrum Proof Certificates},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {54--69},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_6},
doi = {10.1007/978-3-642-25379-9\_6},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Miller11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/NguyenM11,
author = {Thi Minh Tuyen Nguyen and
Claude March{\'{e}}},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Hardware-Dependent Proofs of Numerical Programs},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {314--329},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_23},
doi = {10.1007/978-3-642-25379-9\_23},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/NguyenM11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/OHearn11,
author = {Peter W. O'Hearn},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Algebra, Logic, Locality, Concurrency},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {3--4},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_2},
doi = {10.1007/978-3-642-25379-9\_2},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/OHearn11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/PfenningCT11,
author = {Frank Pfenning and
Lu{\'{\i}}s Caires and
Bernardo Toninho},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Proof-Carrying Code in a Session-Typed Process Calculus},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {21--36},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_4},
doi = {10.1007/978-3-642-25379-9\_4},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/PfenningCT11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Ridge11,
author = {Tom Ridge},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Simple, Functional, Sound and Complete Parsing for All Context-Free
Grammars},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {103--118},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_10},
doi = {10.1007/978-3-642-25379-9\_10},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Ridge11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/ShiMTB11,
author = {Xiaomu Shi and
Jean{-}Fran{\c{c}}ois Monin and
Fr{\'{e}}d{\'{e}}ric Tuong and
Fr{\'{e}}d{\'{e}}ric Blanqui},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {First Steps towards the Certification of an {ARM} Simulator Using
Compcert},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {346--361},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_25},
doi = {10.1007/978-3-642-25379-9\_25},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/ShiMTB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/StratulatD11,
author = {Sorin Stratulat and
Vincent Demange},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Automated Certification of Implicit Induction Proofs},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {37--53},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_5},
doi = {10.1007/978-3-642-25379-9\_5},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/StratulatD11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Voevodsky11,
author = {Vladimir Voevodsky},
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Univalent Semantics of Constructive Type Theories},
booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
pages = {70},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9\_7},
doi = {10.1007/978-3-642-25379-9\_7},
timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Voevodsky11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2011,
editor = {Jean{-}Pierre Jouannaud and
Zhong Shao},
title = {Certified Programs and Proofs - First International Conference, {CPP}
2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7086},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25379-9},
doi = {10.1007/978-3-642-25379-9},
isbn = {978-3-642-25378-2},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/2011.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.
retrieved on 2024-07-12 20:23 CEST from data curated 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:
