CPP 2017 – Author Index

A B C D F G H J K L M P R S T U V Y Z

	Affeldt, Reynald	CPP '17: "Formal Foundations of 3D Geometry ..." Formal Foundations of 3D Geometry to Model Robot Manipulators Reynald Affeldt and Cyril Cohen (AIST, Japan; Inria, France) @InProceedings{CPP17p227, author = {Reynald Affeldt and Cyril Cohen}, title = {Formal Foundations of 3D Geometry to Model Robot Manipulators}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {227-226}, doi = {}, year = {2017}, } Article: cpp17main-mainid39-p (type: Full Paper (12 pages + references)) doi:
	Allais, Guillaume	CPP '17: "Type-and-Scope Safe Programs ..." Type-and-Scope Safe Programs and Their Proofs Guillaume Allais, James Chapman, Conor McBride, and James McKinna (Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK) @InProceedings{CPP17p423, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: cpp17main-mainid28-p (type: Full Paper (12 pages + references)) doi:
	Amani, Sidney	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Andronick, June	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Bauer, Andrej	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Bohrer, Brandon	CPP '17: "Formally Verified Differential ..." Formally Verified Differential Dynamic Logic Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer (Carnegie Mellon University, USA; University of Luxembourg, Luxembourg) @InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, } Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:
	Boldo, Sylvie	CPP '17: "A Coq Formal Proof of the ..." A Coq Formal Proof of the Lax–Milgram Theorem Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero (Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France) @InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, } Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:
	Bortin, Maksym	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Boulier, Simon	CPP '17: "The Next 700 Syntactical Models ..." The Next 700 Syntactical Models of Type Theory Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau (Inria, France) @InProceedings{CPP17p409, author = {Simon Boulier and Pierre-Marie Pédrot and Nicolas Tabareau}, title = {The Next 700 Syntactical Models of Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {409-408}, doi = {}, year = {2017}, } Article: cpp17main-mainid34-p (type: Full Paper (12 pages + references)) doi:
	Brotherston, James	CPP '17: "Automatic Cyclic Termination ..." Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic Reuben N. S. Rowe and James Brotherston (University College London, UK) @InProceedings{CPP17p255, author = {Reuben N. S. Rowe and James Brotherston}, title = {Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {255-254}, doi = {}, year = {2017}, } Article: cpp17main-mainid5-p (type: Full Paper (12 pages + references)) doi:
	Chapman, James	CPP '17: "Type-and-Scope Safe Programs ..." Type-and-Scope Safe Programs and Their Proofs Guillaume Allais, James Chapman, Conor McBride, and James McKinna (Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK) @InProceedings{CPP17p423, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: cpp17main-mainid28-p (type: Full Paper (12 pages + references)) doi:
	Clément, François	CPP '17: "A Coq Formal Proof of the ..." A Coq Formal Proof of the Lax–Milgram Theorem Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero (Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France) @InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, } Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:
	Cockx, Jesper	CPP '17: "Lifting Proof-Relevant Unification ..." Lifting Proof-Relevant Unification to Higher Dimensions Jesper Cockx and Dominique Devriese (KU Leuven, Belgium) @InProceedings{CPP17p395, author = {Jesper Cockx and Dominique Devriese}, title = {Lifting Proof-Relevant Unification to Higher Dimensions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {395-394}, doi = {}, year = {2017}, } Article: cpp17main-mainid17-p (type: Full Paper (12 pages + references)) doi:
	Cohen, Cyril	CPP '17: "Formal Foundations of 3D Geometry ..." Formal Foundations of 3D Geometry to Model Robot Manipulators Reynald Affeldt and Cyril Cohen (AIST, Japan; Inria, France) @InProceedings{CPP17p227, author = {Reynald Affeldt and Cyril Cohen}, title = {Formal Foundations of 3D Geometry to Model Robot Manipulators}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {227-226}, doi = {}, year = {2017}, } Article: cpp17main-mainid39-p (type: Full Paper (12 pages + references)) doi:
	Devietti, Joseph	CPP '17: "Verifying Dynamic Race Detection ..." Verifying Dynamic Race Detection William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti (Princeton University, USA; University of Pennsylvania, USA) @InProceedings{CPP17p367, author = {William Mansky and Yuanfeng Peng and Steve Zdancewic and Joseph Devietti}, title = {Verifying Dynamic Race Detection}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {367-366}, doi = {}, year = {2017}, } Article: cpp17main-mainid31-p (type: Full Paper (12 pages + references)) doi:
	Devriese, Dominique	CPP '17: "Lifting Proof-Relevant Unification ..." Lifting Proof-Relevant Unification to Higher Dimensions Jesper Cockx and Dominique Devriese (KU Leuven, Belgium) @InProceedings{CPP17p395, author = {Jesper Cockx and Dominique Devriese}, title = {Lifting Proof-Relevant Unification to Higher Dimensions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {395-394}, doi = {}, year = {2017}, } Article: cpp17main-mainid17-p (type: Full Paper (12 pages + references)) doi:
	Divasón, Jose	CPP '17: "A Formalization of the Berlekamp-Zassenhaus ..." A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada (Universidad de La Rioja, Spain; University of Innsbruck, Austria) @InProceedings{CPP17p213, author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada}, title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213-212}, doi = {}, year = {2017}, } Article: cpp17main-mainid43-p (type: Full Paper (12 pages + references)) doi:
	Faissole, Florian	CPP '17: "A Coq Formal Proof of the ..." A Coq Formal Proof of the Lax–Milgram Theorem Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero (Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France) @InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, } Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:
	Feng, Xinyu	CPP '17: "Mechanized Verification of ..." Mechanized Verification of Preemptive OS Kernels (Invited Talk) Xinyu Feng (University of Science and Technology of China, China) @InProceedings{CPP17p100, author = {Xinyu Feng}, title = {Mechanized Verification of Preemptive OS Kernels (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {100-99}, doi = {}, year = {2017}, } Article: cpp17key-key2-p (type: Invited Talk Abstract) doi:
	Fox, Anthony	CPP '17: "Verified Compilation of CakeML ..." Verified Compilation of CakeML to Multiple Machine-Code Targets Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar (University of Cambridge, UK; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; UNSW, Australia) @InProceedings{CPP17p339, author = {Anthony Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar}, title = {Verified Compilation of CakeML to Multiple Machine-Code Targets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {339-338}, doi = {}, year = {2017}, } Article: cpp17main-mainid14-p (type: Full Paper (12 pages + references)) doi:
	Gilbert, Gaëtan	CPP '17: "Formalising Real Numbers in ..." Formalising Real Numbers in Homotopy Type Theory Gaëtan Gilbert (ENS Lyon, France) @InProceedings{CPP17p325, author = {Gaëtan Gilbert}, title = {Formalising Real Numbers in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {325-324}, doi = {}, year = {2017}, } Article: cpp17main-mainid29-p (type: Full Paper (12 pages + references)) doi:
	Gross, Jason	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Hölzl, Johannes	CPP '17: "Markov Processes in Isabelle/HOL ..." Markov Processes in Isabelle/HOL Johannes Hölzl (TU München, Germany) @InProceedings{CPP17p311, author = {Johannes Hölzl}, title = {Markov Processes in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {311-310}, doi = {}, year = {2017}, } Article: cpp17main-mainid27-p (type: Full Paper (12 pages + references)) doi:
	Jakubův, Jan	CPP '17: "BliStrTune: Hierarchical Invention ..." BliStrTune: Hierarchical Invention of Theorem Proving Strategies Jan Jakubův and Josef Urban (Czech Technical University, Czech Republic) @InProceedings{CPP17p241, author = {Jan Jakubův and Josef Urban}, title = {BliStrTune: Hierarchical Invention of Theorem Proving Strategies}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {241-240}, doi = {}, year = {2017}, } Article: cpp17main-mainid25-p (type: Full Paper (12 pages + references)) doi:
	Joosten, Sebastiaan	CPP '17: "A Formalization of the Berlekamp-Zassenhaus ..." A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada (Universidad de La Rioja, Spain; University of Innsbruck, Austria) @InProceedings{CPP17p213, author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada}, title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213-212}, doi = {}, year = {2017}, } Article: cpp17main-mainid43-p (type: Full Paper (12 pages + references)) doi:
	Kaiser, Jonas	CPP '17: "Equivalence of System F and ..." Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas Jonas Kaiser, Tobias Tebbi, and Gert Smolka (Saarland University, Germany) @InProceedings{CPP17p451, author = {Jonas Kaiser and Tobias Tebbi and Gert Smolka}, title = {Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {}, year = {2017}, } Article: cpp17main-mainid50-p (type: Full Paper (12 pages + references)) doi:
	Kumar, Ramana	CPP '17: "Verified Compilation of CakeML ..." Verified Compilation of CakeML to Multiple Machine-Code Targets Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar (University of Cambridge, UK; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; UNSW, Australia) @InProceedings{CPP17p339, author = {Anthony Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar}, title = {Verified Compilation of CakeML to Multiple Machine-Code Targets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {339-338}, doi = {}, year = {2017}, } Article: cpp17main-mainid14-p (type: Full Paper (12 pages + references)) doi:
	Lewis, Corey	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Lumsdaine, Peter LeFanu	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Mansky, William	CPP '17: "Verifying Dynamic Race Detection ..." Verifying Dynamic Race Detection William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti (Princeton University, USA; University of Pennsylvania, USA) @InProceedings{CPP17p367, author = {William Mansky and Yuanfeng Peng and Steve Zdancewic and Joseph Devietti}, title = {Verifying Dynamic Race Detection}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {367-366}, doi = {}, year = {2017}, } Article: cpp17main-mainid31-p (type: Full Paper (12 pages + references)) doi:
	Martin, Vincent	CPP '17: "A Coq Formal Proof of the ..." A Coq Formal Proof of the Lax–Milgram Theorem Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero (Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France) @InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, } Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:
	Martin-Dorel, Érik	CPP '17: "A Reflexive Tactic for Polynomial ..." A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations Érik Martin-Dorel and Pierre Roux (IRIT, France; Paul Sabatier University, France; ONERA, France) @InProceedings{CPP17p297, author = {Érik Martin-Dorel and Pierre Roux}, title = {A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {297-296}, doi = {}, year = {2017}, } Article: cpp17main-mainid6-p (type: Full Paper (12 pages + references)) doi:
	Matsumoto, Saki	CPP '17: "Formalization of Karp-Miller ..." Formalization of Karp-Miller Tree Construction on Petri Nets Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto (Chiba University, Japan; Acrovision, Japan) @InProceedings{CPP17p269, author = {Mitsuharu Yamamoto and Shogo Sekine and Saki Matsumoto}, title = {Formalization of Karp-Miller Tree Construction on Petri Nets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {269-268}, doi = {}, year = {2017}, } Article: cpp17main-mainid36-p (type: Full Paper (12 pages + references)) doi:
	Mayero, Micaela	CPP '17: "A Coq Formal Proof of the ..." A Coq Formal Proof of the Lax–Milgram Theorem Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero (Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France) @InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, } Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:
	McBride, Conor	CPP '17: "Type-and-Scope Safe Programs ..." Type-and-Scope Safe Programs and Their Proofs Guillaume Allais, James Chapman, Conor McBride, and James McKinna (Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK) @InProceedings{CPP17p423, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: cpp17main-mainid28-p (type: Full Paper (12 pages + references)) doi:
	McKinna, James	CPP '17: "Type-and-Scope Safe Programs ..." Type-and-Scope Safe Programs and Their Proofs Guillaume Allais, James Chapman, Conor McBride, and James McKinna (Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK) @InProceedings{CPP17p423, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, } Article: cpp17main-mainid28-p (type: Full Paper (12 pages + references)) doi:
	Myreen, Magnus O.	CPP '17: "Verified Compilation of CakeML ..." Verified Compilation of CakeML to Multiple Machine-Code Targets Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar (University of Cambridge, UK; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; UNSW, Australia) @InProceedings{CPP17p339, author = {Anthony Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar}, title = {Verified Compilation of CakeML to Multiple Machine-Code Targets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {339-338}, doi = {}, year = {2017}, } Article: cpp17main-mainid14-p (type: Full Paper (12 pages + references)) doi:
	Paulson, Lawrence C.	CPP '17: "Porting the HOL Light Analysis ..." Porting the HOL Light Analysis Library: Some Lessons (Invited Talk) Lawrence C. Paulson (University of Cambridge, UK) @InProceedings{CPP17p1, author = {Lawrence C. Paulson}, title = {Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2017}, } Article: cpp17key-key1-p (type: Invited Talk Abstract) doi:
	Pédrot, Pierre-Marie	CPP '17: "The Next 700 Syntactical Models ..." The Next 700 Syntactical Models of Type Theory Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau (Inria, France) @InProceedings{CPP17p409, author = {Simon Boulier and Pierre-Marie Pédrot and Nicolas Tabareau}, title = {The Next 700 Syntactical Models of Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {409-408}, doi = {}, year = {2017}, } Article: cpp17main-mainid34-p (type: Full Paper (12 pages + references)) doi:
	Peng, Yuanfeng	CPP '17: "Verifying Dynamic Race Detection ..." Verifying Dynamic Race Detection William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti (Princeton University, USA; University of Pennsylvania, USA) @InProceedings{CPP17p367, author = {William Mansky and Yuanfeng Peng and Steve Zdancewic and Joseph Devietti}, title = {Verifying Dynamic Race Detection}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {367-366}, doi = {}, year = {2017}, } Article: cpp17main-mainid31-p (type: Full Paper (12 pages + references)) doi:
	Platzer, André	CPP '17: "Formally Verified Differential ..." Formally Verified Differential Dynamic Logic Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer (Carnegie Mellon University, USA; University of Luxembourg, Luxembourg) @InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, } Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:
	Pottier, François	CPP '17: "Verifying a Hash Table and ..." Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic François Pottier (Inria, France) @InProceedings{CPP17p199, author = {François Pottier}, title = {Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {}, year = {2017}, } Article: cpp17main-mainid7-p (type: Full Paper (12 pages + references)) doi:
	Rahli, Vincent	CPP '17: "Formally Verified Differential ..." Formally Verified Differential Dynamic Logic Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer (Carnegie Mellon University, USA; University of Luxembourg, Luxembourg) @InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, } Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:
	Rizkallah, Christine	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Roux, Pierre	CPP '17: "A Reflexive Tactic for Polynomial ..." A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations Érik Martin-Dorel and Pierre Roux (IRIT, France; Paul Sabatier University, France; ONERA, France) @InProceedings{CPP17p297, author = {Érik Martin-Dorel and Pierre Roux}, title = {A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {297-296}, doi = {}, year = {2017}, } Article: cpp17main-mainid6-p (type: Full Paper (12 pages + references)) doi:
	Rowe, Reuben N. S.	CPP '17: "Automatic Cyclic Termination ..." Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic Reuben N. S. Rowe and James Brotherston (University College London, UK) @InProceedings{CPP17p255, author = {Reuben N. S. Rowe and James Brotherston}, title = {Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {255-254}, doi = {}, year = {2017}, } Article: cpp17main-mainid5-p (type: Full Paper (12 pages + references)) doi:
	Sekine, Shogo	CPP '17: "Formalization of Karp-Miller ..." Formalization of Karp-Miller Tree Construction on Petri Nets Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto (Chiba University, Japan; Acrovision, Japan) @InProceedings{CPP17p269, author = {Mitsuharu Yamamoto and Shogo Sekine and Saki Matsumoto}, title = {Formalization of Karp-Miller Tree Construction on Petri Nets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {269-268}, doi = {}, year = {2017}, } Article: cpp17main-mainid36-p (type: Full Paper (12 pages + references)) doi:
	Shulman, Michael	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Smolka, Gert	CPP '17: "Equivalence of System F and ..." Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas Jonas Kaiser, Tobias Tebbi, and Gert Smolka (Saarland University, Germany) @InProceedings{CPP17p451, author = {Jonas Kaiser and Tobias Tebbi and Gert Smolka}, title = {Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {}, year = {2017}, } Article: cpp17main-mainid50-p (type: Full Paper (12 pages + references)) doi:
	Sozeau, Matthieu	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Spitters, Bas	CPP '17: "The HoTT Library: A Formalization ..." The HoTT Library: A Formalization of Homotopy Type Theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters (University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark) @InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, } Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:
	Tabareau, Nicolas	CPP '17: "The Next 700 Syntactical Models ..." The Next 700 Syntactical Models of Type Theory Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau (Inria, France) @InProceedings{CPP17p409, author = {Simon Boulier and Pierre-Marie Pédrot and Nicolas Tabareau}, title = {The Next 700 Syntactical Models of Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {409-408}, doi = {}, year = {2017}, } Article: cpp17main-mainid34-p (type: Full Paper (12 pages + references)) doi:
	Tan, Yong Kiam	CPP '17: "Verified Compilation of CakeML ..." Verified Compilation of CakeML to Multiple Machine-Code Targets Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar (University of Cambridge, UK; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; UNSW, Australia) @InProceedings{CPP17p339, author = {Anthony Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar}, title = {Verified Compilation of CakeML to Multiple Machine-Code Targets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {339-338}, doi = {}, year = {2017}, } Article: cpp17main-mainid14-p (type: Full Paper (12 pages + references)) doi:
	Tebbi, Tobias	CPP '17: "Equivalence of System F and ..." Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas Jonas Kaiser, Tobias Tebbi, and Gert Smolka (Saarland University, Germany) @InProceedings{CPP17p451, author = {Jonas Kaiser and Tobias Tebbi and Gert Smolka}, title = {Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {}, year = {2017}, } Article: cpp17main-mainid50-p (type: Full Paper (12 pages + references)) doi:
	Thiemann, René	CPP '17: "A Formalization of the Berlekamp-Zassenhaus ..." A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada (Universidad de La Rioja, Spain; University of Innsbruck, Austria) @InProceedings{CPP17p213, author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada}, title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213-212}, doi = {}, year = {2017}, } Article: cpp17main-mainid43-p (type: Full Paper (12 pages + references)) doi:
	Tuong, Joseph	CPP '17: "Complx: A Verification Framework ..." Complx: A Verification Framework for Concurrent Imperative Programs Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong (Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA) @InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, } Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:
	Urban, Josef	CPP '17: "BliStrTune: Hierarchical Invention ..." BliStrTune: Hierarchical Invention of Theorem Proving Strategies Jan Jakubův and Josef Urban (Czech Technical University, Czech Republic) @InProceedings{CPP17p241, author = {Jan Jakubův and Josef Urban}, title = {BliStrTune: Hierarchical Invention of Theorem Proving Strategies}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {241-240}, doi = {}, year = {2017}, } Article: cpp17main-mainid25-p (type: Full Paper (12 pages + references)) doi:
	Völp, Marcus	CPP '17: "Formally Verified Differential ..." Formally Verified Differential Dynamic Logic Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer (Carnegie Mellon University, USA; University of Luxembourg, Luxembourg) @InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, } Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:
	Vukotic, Ivana	CPP '17: "Formally Verified Differential ..." Formally Verified Differential Dynamic Logic Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer (Carnegie Mellon University, USA; University of Luxembourg, Luxembourg) @InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, } Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:
	Yamada, Akihisa	CPP '17: "A Formalization of the Berlekamp-Zassenhaus ..." A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada (Universidad de La Rioja, Spain; University of Innsbruck, Austria) @InProceedings{CPP17p213, author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada}, title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213-212}, doi = {}, year = {2017}, } Article: cpp17main-mainid43-p (type: Full Paper (12 pages + references)) doi:
	Yamamoto, Mitsuharu	CPP '17: "Formalization of Karp-Miller ..." Formalization of Karp-Miller Tree Construction on Petri Nets Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto (Chiba University, Japan; Acrovision, Japan) @InProceedings{CPP17p269, author = {Mitsuharu Yamamoto and Shogo Sekine and Saki Matsumoto}, title = {Formalization of Karp-Miller Tree Construction on Petri Nets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {269-268}, doi = {}, year = {2017}, } Article: cpp17main-mainid36-p (type: Full Paper (12 pages + references)) doi:
	Zdancewic, Steve	CPP '17: "Verifying Dynamic Race Detection ..." Verifying Dynamic Race Detection William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti (Princeton University, USA; University of Pennsylvania, USA) @InProceedings{CPP17p367, author = {William Mansky and Yuanfeng Peng and Steve Zdancewic and Joseph Devietti}, title = {Verifying Dynamic Race Detection}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {367-366}, doi = {}, year = {2017}, } Article: cpp17main-mainid31-p (type: Full Paper (12 pages + references)) doi:

62 authors

proc time: 0.08