Workshop CPP 2020 – Author Index

A B C D F G H I K L M N O P R S T U V W X Z

	Altmanninger, Johannes	CPP '20: "Frying the Egg, Roasting the ..." Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs Johannes Altmanninger and Adrián Rebola Pardo (TU Vienna, Austria) @InProceedings{CPP20p109, author = {Johannes Altmanninger and Adrián Rebola Pardo}, title = {Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {109-108}, doi = {10.1145/3372885.3373821}, year = {2020}, } Publisher's Version
	Annenkov, Danil	CPP '20: "ConCert: A Smart Contract ..." ConCert: A Smart Contract Certification Framework in Coq Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters (Aarhus University, Denmark) @InProceedings{CPP20p307, author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters}, title = {ConCert: A Smart Contract Certification Framework in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {307-306}, doi = {10.1145/3372885.3373829}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Aspinall, David	CPP '20: "Formalising Oblivious Transfer ..." Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL David Butler, David Aspinall, and Adrià Gascón (Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK) @InProceedings{CPP20p325, author = {David Butler and David Aspinall and Adrià Gascón}, title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {325-324}, doi = {10.1145/3372885.3373815}, year = {2020}, } Publisher's Version
	Bach Poulsen, Casper	CPP '20: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands) @InProceedings{CPP20p397, author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser}, title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3372885.3373818}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Blaudeau, Clement	CPP '20: "A Verified Packrat Parser ..." A Verified Packrat Parser Interpreter for Parsing Expression Grammars Clement Blaudeau and Natarajan Shankar (École Polytechnique, France; SRI International, USA) @InProceedings{CPP20p37, author = {Clement Blaudeau and Natarajan Shankar}, title = {A Verified Packrat Parser Interpreter for Parsing Expression Grammars}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {37-36}, doi = {10.1145/3372885.3373836}, year = {2020}, } Publisher's Version
	Brown, Chad	CPP '20: "Exploration of Neural Machine ..." Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban (University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland) @InProceedings{CPP20p145, author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban}, title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {145-144}, doi = {10.1145/3372885.3373827}, year = {2020}, } Publisher's Version
	Buldas, Ahto	CPP '20: "Verified Security of BLT Signature ..." Verified Security of BLT Signature Scheme Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja (Tallinn University of Technology, Estonia; Guardtime, Estonia) @InProceedings{CPP20p343, author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja}, title = {Verified Security of BLT Signature Scheme}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3372885.3373828}, year = {2020}, } Publisher's Version
	Butler, David	CPP '20: "Formalising Oblivious Transfer ..." Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL David Butler, David Aspinall, and Adrià Gascón (Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK) @InProceedings{CPP20p325, author = {David Butler and David Aspinall and Adrià Gascón}, title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {325-324}, doi = {10.1145/3372885.3373815}, year = {2020}, } Publisher's Version
	Buzzard, Kevin	CPP '20: "Formalising Perfectoid Spaces ..." Formalising Perfectoid Spaces Kevin Buzzard, Johan Commelin, and Patrick Massot (Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France) @InProceedings{CPP20p415, author = {Kevin Buzzard and Johan Commelin and Patrick Massot}, title = {Formalising Perfectoid Spaces}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {415-414}, doi = {10.1145/3372885.3373830}, year = {2020}, } Publisher's Version
	Chen, Xiaohong	CPP '20: "Matching Logic: The Foundation ..." Matching Logic: The Foundation of the K Framework (Invited Talk) Grigore Roşu and Xiaohong Chen (University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA) @InProceedings{CPP20p1, author = {Grigore Roşu and Xiaohong Chen}, title = {Matching Logic: The Foundation of the K Framework (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3372885.3378574}, year = {2020}, } Publisher's Version
	Chlipala, Adam	CPP '20: "Proof Assistants at the Hardware-Software ..." Proof Assistants at the Hardware-Software Interface (Invited Talk) Adam Chlipala (Massachusetts Institute of Technology, USA) @InProceedings{CPP20p19, author = {Adam Chlipala}, title = {Proof Assistants at the Hardware-Software Interface (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {19-18}, doi = {10.1145/3372885.3378575}, year = {2020}, } Publisher's Version
	Commelin, Johan	CPP '20: "Formalising Perfectoid Spaces ..." Formalising Perfectoid Spaces Kevin Buzzard, Johan Commelin, and Patrick Massot (Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France) @InProceedings{CPP20p415, author = {Kevin Buzzard and Johan Commelin and Patrick Massot}, title = {Formalising Perfectoid Spaces}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {415-414}, doi = {10.1145/3372885.3373830}, year = {2020}, } Publisher's Version
	Díaz, Tomás	CPP '20: "A Mechanized Formalization ..." A Mechanized Formalization of GraphQL Tomás Díaz, Federico Olmedo, and Éric Tanter (IMFD, Chile; University of Chile, Chile; Inria, France) @InProceedings{CPP20p289, author = {Tomás Díaz and Federico Olmedo and Éric Tanter}, title = {A Mechanized Formalization of GraphQL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {289-288}, doi = {10.1145/3372885.3373822}, year = {2020}, } Publisher's Version
	Doczkal, Christian	CPP '20: "Completeness of an Axiomatization ..." Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq Christian Doczkal and Damien Pous (University of Côte d'Azur, France; Inria, France; University of Lyon, France; CNRS, France; ENS Lyon, France) @InProceedings{CPP20p451, author = {Christian Doczkal and Damien Pous}, title = {Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {10.1145/3372885.3373831}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Firsov, Denis	CPP '20: "Verified Security of BLT Signature ..." Verified Security of BLT Signature Scheme Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja (Tallinn University of Technology, Estonia; Guardtime, Estonia) @InProceedings{CPP20p343, author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja}, title = {Verified Security of BLT Signature Scheme}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3372885.3373828}, year = {2020}, } Publisher's Version
	Forsberg, Fredrik Nordvall	CPP '20: "Three Equivalent Ordinal Notation ..." Three Equivalent Ordinal Notation Systems in Cubical Agda Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani (University of Strathclyde, UK; LMU Munich, Germany) @InProceedings{CPP20p253, author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani}, title = {Three Equivalent Ordinal Notation Systems in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253-252}, doi = {10.1145/3372885.3373835}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Forster, Yannick	CPP '20: "Verified Programming of Turing ..." Verified Programming of Turing Machines in Coq Yannick Forster, Fabian Kunze, and Maximilian Wuttke (Saarland University, Germany) @InProceedings{CPP20p181, author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke}, title = {Verified Programming of Turing Machines in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181-180}, doi = {10.1145/3372885.3373816}, year = {2020}, } Publisher's Version CPP '20: "Undecidability of Higher-Order ..." Undecidability of Higher-Order Unification Formalised in Coq Simon Spies and Yannick Forster (Saarland University, Germany) @InProceedings{CPP20p217, author = {Simon Spies and Yannick Forster}, title = {Undecidability of Higher-Order Unification Formalised in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {217-216}, doi = {10.1145/3372885.3373832}, year = {2020}, } Publisher's Version CPP '20: "Coq à la Carte: A Practical ..." Coq à la Carte: A Practical Approach to Modular Syntax with Binders Yannick Forster and Kathrin Stark (Saarland University, Germany) @InProceedings{CPP20p271, author = {Yannick Forster and Kathrin Stark}, title = {Coq à la Carte: A Practical Approach to Modular Syntax with Binders}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {271-270}, doi = {10.1145/3372885.3373817}, year = {2020}, } Publisher's Version
	Gascón, Adrià	CPP '20: "Formalising Oblivious Transfer ..." Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL David Butler, David Aspinall, and Adrià Gascón (Alan Turing Institute, UK; University of Edinburgh, UK; Google, UK) @InProceedings{CPP20p325, author = {David Butler and David Aspinall and Adrià Gascón}, title = {Formalising Oblivious Transfer in the Semi-honest and Malicious Model in CryptHOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {325-324}, doi = {10.1145/3372885.3373815}, year = {2020}, } Publisher's Version
	Ghani, Neil	CPP '20: "Three Equivalent Ordinal Notation ..." Three Equivalent Ordinal Notation Systems in Cubical Agda Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani (University of Strathclyde, UK; LMU Munich, Germany) @InProceedings{CPP20p253, author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani}, title = {Three Equivalent Ordinal Notation Systems in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253-252}, doi = {10.1145/3372885.3373835}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Goel, Shilpi	CPP '20: "Verifying x86 Instruction ..." Verifying x86 Instruction Implementations Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords (Centaur Technology, USA) @InProceedings{CPP20p91, author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords}, title = {Verifying x86 Instruction Implementations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3372885.3373811}, year = {2020}, } Publisher's Version
	Grossman, Dan	CPP '20: "REPLica: REPL Instrumentation ..." REPLica: REPL Instrumentation for Coq Analysis Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner (University of Washington, USA; University of California at San Diego, USA) @InProceedings{CPP20p163, author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner}, title = {REPLica: REPL Instrumentation for Coq Analysis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {163-162}, doi = {10.1145/3372885.3373823}, year = {2020}, } Publisher's Version
	Han, Jesse Michael	CPP '20: "A Formal Proof of the Independence ..." A Formal Proof of the Independence of the Continuum Hypothesis Jesse Michael Han and Floris van Doorn (University of Pittsburgh, USA) @InProceedings{CPP20p487, author = {Jesse Michael Han and Floris van Doorn}, title = {A Formal Proof of the Independence of the Continuum Hypothesis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {487-486}, doi = {10.1145/3372885.3373826}, year = {2020}, } Publisher's Version
	He, Paul	CPP '20: "An Equational Theory for Weak ..." An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea) @InProceedings{CPP20p127, author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic}, title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3372885.3373813}, year = {2020}, } Publisher's Version
	Hobor, Aquinas	CPP '20: "A Functional Proof Pearl: ..." A Functional Proof Pearl: Inverting the Ackermann Hierarchy Linh Tran, Anshuman Mohan, and Aquinas Hobor (Yale University, USA; National University of Singapore, Singapore) @InProceedings{CPP20p199, author = {Linh Tran and Anshuman Mohan and Aquinas Hobor}, title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {10.1145/3372885.3373837}, year = {2020}, } Publisher's Version
	Hur, Chung-Kil	CPP '20: "An Equational Theory for Weak ..." An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea) @InProceedings{CPP20p127, author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic}, title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3372885.3373813}, year = {2020}, } Publisher's Version
	Immler, Fabian	CPP '20: "The Poincaré-Bendixson Theorem ..." The Poincaré-Bendixson Theorem in Isabelle/HOL Fabian Immler and Yong Kiam Tan (Carnegie Mellon University, USA) @InProceedings{CPP20p469, author = {Fabian Immler and Yong Kiam Tan}, title = {The Poincaré-Bendixson Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {469-468}, doi = {10.1145/3372885.3373833}, year = {2020}, } Publisher's Version
	Kaliszyk, Cezary	CPP '20: "Exploration of Neural Machine ..." Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban (University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland) @InProceedings{CPP20p145, author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban}, title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {145-144}, doi = {10.1145/3372885.3373827}, year = {2020}, } Publisher's Version
	Krebbers, Robbert	CPP '20: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands) @InProceedings{CPP20p397, author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser}, title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3372885.3373818}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Kunze, Fabian	CPP '20: "Verified Programming of Turing ..." Verified Programming of Turing Machines in Coq Yannick Forster, Fabian Kunze, and Maximilian Wuttke (Saarland University, Germany) @InProceedings{CPP20p181, author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke}, title = {Verified Programming of Turing Machines in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181-180}, doi = {10.1145/3372885.3373816}, year = {2020}, } Publisher's Version
	Laanoja, Risto	CPP '20: "Verified Security of BLT Signature ..." Verified Security of BLT Signature Scheme Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja (Tallinn University of Technology, Estonia; Guardtime, Estonia) @InProceedings{CPP20p343, author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja}, title = {Verified Security of BLT Signature Scheme}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3372885.3373828}, year = {2020}, } Publisher's Version
	Lerner, Sorin	CPP '20: "REPLica: REPL Instrumentation ..." REPLica: REPL Instrumentation for Coq Analysis Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner (University of Washington, USA; University of California at San Diego, USA) @InProceedings{CPP20p163, author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner}, title = {REPLica: REPL Instrumentation for Coq Analysis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {163-162}, doi = {10.1145/3372885.3373823}, year = {2020}, } Publisher's Version
	Letan, Thomas	CPP '20: "FreeSpec: Specifying, Verifying, ..." FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq Thomas Letan and Yann Régis-Gianas (ANSSI, France; University of Paris, France; IRIF, France; Inria, France) @InProceedings{CPP20p73, author = {Thomas Letan and Yann Régis-Gianas}, title = {FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {73-72}, doi = {10.1145/3372885.3373812}, year = {2020}, } Publisher's Version
	Massot, Patrick	CPP '20: "Formalising Perfectoid Spaces ..." Formalising Perfectoid Spaces Kevin Buzzard, Johan Commelin, and Patrick Massot (Imperial College London, UK; University of Freiburg, Germany; University of Paris-Sud, France; CNRS, France) @InProceedings{CPP20p415, author = {Kevin Buzzard and Johan Commelin and Patrick Massot}, title = {Formalising Perfectoid Spaces}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {415-414}, doi = {10.1145/3372885.3373830}, year = {2020}, } Publisher's Version
	Mohan, Anshuman	CPP '20: "A Functional Proof Pearl: ..." A Functional Proof Pearl: Inverting the Ackermann Hierarchy Linh Tran, Anshuman Mohan, and Aquinas Hobor (Yale University, USA; National University of Singapore, Singapore) @InProceedings{CPP20p199, author = {Linh Tran and Anshuman Mohan and Aquinas Hobor}, title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {10.1145/3372885.3373837}, year = {2020}, } Publisher's Version
	Mörtberg, Anders	CPP '20: "Cubical Synthetic Homotopy ..." Cubical Synthetic Homotopy Theory Anders Mörtberg and Loïc Pujet (Stockholm University, Sweden; Inria, France) @InProceedings{CPP20p235, author = {Anders Mörtberg and Loïc Pujet}, title = {Cubical Synthetic Homotopy Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {235-234}, doi = {10.1145/3372885.3373825}, year = {2020}, } Publisher's Version
	Natarajan, Raja	CPP '20: "A Constructive Formalization ..." A Constructive Formalization of the Weak Perfect Graph Theorem Abhishek Kr Singh and Raja Natarajan (Tata Institute of Fundamental Research, India) @InProceedings{CPP20p433, author = {Abhishek Kr Singh and Raja Natarajan}, title = {A Constructive Formalization of the Weak Perfect Graph Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {433-432}, doi = {10.1145/3372885.3373819}, year = {2020}, } Publisher's Version
	Nielsen, Jakob Botsch	CPP '20: "ConCert: A Smart Contract ..." ConCert: A Smart Contract Certification Framework in Coq Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters (Aarhus University, Denmark) @InProceedings{CPP20p307, author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters}, title = {ConCert: A Smart Contract Certification Framework in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {307-306}, doi = {10.1145/3372885.3373829}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Nipkow, Tobias	CPP '20: "Proof Pearl: Braun Trees ..." Proof Pearl: Braun Trees Tobias Nipkow and Thomas Sewell (TU Munich, Germany; Chalmers University of Technology, Sweden) @InProceedings{CPP20p55, author = {Tobias Nipkow and Thomas Sewell}, title = {Proof Pearl: Braun Trees}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {55-54}, doi = {10.1145/3372885.3373834}, year = {2020}, } Publisher's Version
	Olmedo, Federico	CPP '20: "A Mechanized Formalization ..." A Mechanized Formalization of GraphQL Tomás Díaz, Federico Olmedo, and Éric Tanter (IMFD, Chile; University of Chile, Chile; Inria, France) @InProceedings{CPP20p289, author = {Tomás Díaz and Federico Olmedo and Éric Tanter}, title = {A Mechanized Formalization of GraphQL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {289-288}, doi = {10.1145/3372885.3373822}, year = {2020}, } Publisher's Version
	Overbeek, Roy	CPP '20: "Formalizing Determinacy of ..." Formalizing Determinacy of Concurrent Revisions Roy Overbeek (Vrije Universiteit Amsterdam, Netherlands) @InProceedings{CPP20p361, author = {Roy Overbeek}, title = {Formalizing Determinacy of Concurrent Revisions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {361-360}, doi = {10.1145/3372885.3373820}, year = {2020}, } Publisher's Version
	Pous, Damien	CPP '20: "Completeness of an Axiomatization ..." Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq Christian Doczkal and Damien Pous (University of Côte d'Azur, France; Inria, France; University of Lyon, France; CNRS, France; ENS Lyon, France) @InProceedings{CPP20p451, author = {Christian Doczkal and Damien Pous}, title = {Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {10.1145/3372885.3373831}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Pujet, Loïc	CPP '20: "Cubical Synthetic Homotopy ..." Cubical Synthetic Homotopy Theory Anders Mörtberg and Loïc Pujet (Stockholm University, Sweden; Inria, France) @InProceedings{CPP20p235, author = {Anders Mörtberg and Loïc Pujet}, title = {Cubical Synthetic Homotopy Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {235-234}, doi = {10.1145/3372885.3373825}, year = {2020}, } Publisher's Version
	Rebola Pardo, Adrián	CPP '20: "Frying the Egg, Roasting the ..." Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs Johannes Altmanninger and Adrián Rebola Pardo (TU Vienna, Austria) @InProceedings{CPP20p109, author = {Johannes Altmanninger and Adrián Rebola Pardo}, title = {Frying the Egg, Roasting the Chicken: Unit Deletions in DRAT Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {109-108}, doi = {10.1145/3372885.3373821}, year = {2020}, } Publisher's Version
	Régis-Gianas, Yann	CPP '20: "FreeSpec: Specifying, Verifying, ..." FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq Thomas Letan and Yann Régis-Gianas (ANSSI, France; University of Paris, France; IRIF, France; Inria, France) @InProceedings{CPP20p73, author = {Thomas Letan and Yann Régis-Gianas}, title = {FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {73-72}, doi = {10.1145/3372885.3373812}, year = {2020}, } Publisher's Version
	Ringer, Talia	CPP '20: "REPLica: REPL Instrumentation ..." REPLica: REPL Instrumentation for Coq Analysis Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner (University of Washington, USA; University of California at San Diego, USA) @InProceedings{CPP20p163, author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner}, title = {REPLica: REPL Instrumentation for Coq Analysis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {163-162}, doi = {10.1145/3372885.3373823}, year = {2020}, } Publisher's Version
	Roşu, Grigore	CPP '20: "Matching Logic: The Foundation ..." Matching Logic: The Foundation of the K Framework (Invited Talk) Grigore Roşu and Xiaohong Chen (University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA) @InProceedings{CPP20p1, author = {Grigore Roşu and Xiaohong Chen}, title = {Matching Logic: The Foundation of the K Framework (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3372885.3378574}, year = {2020}, } Publisher's Version
	Rouvoet, Arjen	CPP '20: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands) @InProceedings{CPP20p397, author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser}, title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3372885.3373818}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Sanchez-Stern, Alex	CPP '20: "REPLica: REPL Instrumentation ..." REPLica: REPL Instrumentation for Coq Analysis Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner (University of Washington, USA; University of California at San Diego, USA) @InProceedings{CPP20p163, author = {Talia Ringer and Alex Sanchez-Stern and Dan Grossman and Sorin Lerner}, title = {REPLica: REPL Instrumentation for Coq Analysis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {163-162}, doi = {10.1145/3372885.3373823}, year = {2020}, } Publisher's Version
	Sewell, Thomas	CPP '20: "Proof Pearl: Braun Trees ..." Proof Pearl: Braun Trees Tobias Nipkow and Thomas Sewell (TU Munich, Germany; Chalmers University of Technology, Sweden) @InProceedings{CPP20p55, author = {Tobias Nipkow and Thomas Sewell}, title = {Proof Pearl: Braun Trees}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {55-54}, doi = {10.1145/3372885.3373834}, year = {2020}, } Publisher's Version
	Shankar, Natarajan	CPP '20: "A Verified Packrat Parser ..." A Verified Packrat Parser Interpreter for Parsing Expression Grammars Clement Blaudeau and Natarajan Shankar (École Polytechnique, France; SRI International, USA) @InProceedings{CPP20p37, author = {Clement Blaudeau and Natarajan Shankar}, title = {A Verified Packrat Parser Interpreter for Parsing Expression Grammars}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {37-36}, doi = {10.1145/3372885.3373836}, year = {2020}, } Publisher's Version
	Singh, Abhishek Kr	CPP '20: "A Constructive Formalization ..." A Constructive Formalization of the Weak Perfect Graph Theorem Abhishek Kr Singh and Raja Natarajan (Tata Institute of Fundamental Research, India) @InProceedings{CPP20p433, author = {Abhishek Kr Singh and Raja Natarajan}, title = {A Constructive Formalization of the Weak Perfect Graph Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {433-432}, doi = {10.1145/3372885.3373819}, year = {2020}, } Publisher's Version
	Slobodova, Anna	CPP '20: "Verifying x86 Instruction ..." Verifying x86 Instruction Implementations Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords (Centaur Technology, USA) @InProceedings{CPP20p91, author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords}, title = {Verifying x86 Instruction Implementations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3372885.3373811}, year = {2020}, } Publisher's Version
	Spies, Simon	CPP '20: "Undecidability of Higher-Order ..." Undecidability of Higher-Order Unification Formalised in Coq Simon Spies and Yannick Forster (Saarland University, Germany) @InProceedings{CPP20p217, author = {Simon Spies and Yannick Forster}, title = {Undecidability of Higher-Order Unification Formalised in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {217-216}, doi = {10.1145/3372885.3373832}, year = {2020}, } Publisher's Version
	Spitters, Bas	CPP '20: "ConCert: A Smart Contract ..." ConCert: A Smart Contract Certification Framework in Coq Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters (Aarhus University, Denmark) @InProceedings{CPP20p307, author = {Danil Annenkov and Jakob Botsch Nielsen and Bas Spitters}, title = {ConCert: A Smart Contract Certification Framework in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {307-306}, doi = {10.1145/3372885.3373829}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Stark, Kathrin	CPP '20: "Coq à la Carte: A Practical ..." Coq à la Carte: A Practical Approach to Modular Syntax with Binders Yannick Forster and Kathrin Stark (Saarland University, Germany) @InProceedings{CPP20p271, author = {Yannick Forster and Kathrin Stark}, title = {Coq à la Carte: A Practical Approach to Modular Syntax with Binders}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {271-270}, doi = {10.1145/3372885.3373817}, year = {2020}, } Publisher's Version
	Sumners, Rob	CPP '20: "Verifying x86 Instruction ..." Verifying x86 Instruction Implementations Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords (Centaur Technology, USA) @InProceedings{CPP20p91, author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords}, title = {Verifying x86 Instruction Implementations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3372885.3373811}, year = {2020}, } Publisher's Version
	Swords, Sol	CPP '20: "Verifying x86 Instruction ..." Verifying x86 Instruction Implementations Shilpi Goel, Anna Slobodova, Rob Sumners, and Sol Swords (Centaur Technology, USA) @InProceedings{CPP20p91, author = {Shilpi Goel and Anna Slobodova and Rob Sumners and Sol Swords}, title = {Verifying x86 Instruction Implementations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {91-90}, doi = {10.1145/3372885.3373811}, year = {2020}, } Publisher's Version
	Tan, Yong Kiam	CPP '20: "The Poincaré-Bendixson Theorem ..." The Poincaré-Bendixson Theorem in Isabelle/HOL Fabian Immler and Yong Kiam Tan (Carnegie Mellon University, USA) @InProceedings{CPP20p469, author = {Fabian Immler and Yong Kiam Tan}, title = {The Poincaré-Bendixson Theorem in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {469-468}, doi = {10.1145/3372885.3373833}, year = {2020}, } Publisher's Version
	Tanter, Éric	CPP '20: "A Mechanized Formalization ..." A Mechanized Formalization of GraphQL Tomás Díaz, Federico Olmedo, and Éric Tanter (IMFD, Chile; University of Chile, Chile; Inria, France) @InProceedings{CPP20p289, author = {Tomás Díaz and Federico Olmedo and Éric Tanter}, title = {A Mechanized Formalization of GraphQL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {289-288}, doi = {10.1145/3372885.3373822}, year = {2020}, } Publisher's Version
	The mathlib Community	CPP '20: "The Lean Mathematical Library ..." The Lean Mathematical Library The mathlib Community @InProceedings{CPP20p505, author = { The mathlib Community}, title = {The Lean Mathematical Library}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {505-504}, doi = {10.1145/3372885.3373824}, year = {2020}, } Publisher's Version
	Tran, Linh	CPP '20: "A Functional Proof Pearl: ..." A Functional Proof Pearl: Inverting the Ackermann Hierarchy Linh Tran, Anshuman Mohan, and Aquinas Hobor (Yale University, USA; National University of Singapore, Singapore) @InProceedings{CPP20p199, author = {Linh Tran and Anshuman Mohan and Aquinas Hobor}, title = {A Functional Proof Pearl: Inverting the Ackermann Hierarchy}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {10.1145/3372885.3373837}, year = {2020}, } Publisher's Version
	Truu, Ahto	CPP '20: "Verified Security of BLT Signature ..." Verified Security of BLT Signature Scheme Denis Firsov, Ahto Buldas, Ahto Truu, and Risto Laanoja (Tallinn University of Technology, Estonia; Guardtime, Estonia) @InProceedings{CPP20p343, author = {Denis Firsov and Ahto Buldas and Ahto Truu and Risto Laanoja}, title = {Verified Security of BLT Signature Scheme}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3372885.3373828}, year = {2020}, } Publisher's Version
	Urban, Josef	CPP '20: "Exploration of Neural Machine ..." Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban (University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland) @InProceedings{CPP20p145, author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban}, title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {145-144}, doi = {10.1145/3372885.3373827}, year = {2020}, } Publisher's Version
	Van Doorn, Floris	CPP '20: "A Formal Proof of the Independence ..." A Formal Proof of the Independence of the Continuum Hypothesis Jesse Michael Han and Floris van Doorn (University of Pittsburgh, USA) @InProceedings{CPP20p487, author = {Jesse Michael Han and Floris van Doorn}, title = {A Formal Proof of the Independence of the Continuum Hypothesis}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {487-486}, doi = {10.1145/3372885.3373826}, year = {2020}, } Publisher's Version
	Veltri, Niccolò	CPP '20: "Formalizing 𝜋-Calculus ..." Formalizing 𝜋-Calculus in Guarded Cubical Agda Niccolò Veltri and Andrea Vezzosi (Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark) @InProceedings{CPP20p379, author = {Niccolò Veltri and Andrea Vezzosi}, title = {Formalizing 𝜋-Calculus in Guarded Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {379-378}, doi = {10.1145/3372885.3373814}, year = {2020}, } Publisher's Version
	Vezzosi, Andrea	CPP '20: "Formalizing 𝜋-Calculus ..." Formalizing 𝜋-Calculus in Guarded Cubical Agda Niccolò Veltri and Andrea Vezzosi (Tallinn University of Technology, Estonia; IT University of Copenhagen, Denmark) @InProceedings{CPP20p379, author = {Niccolò Veltri and Andrea Vezzosi}, title = {Formalizing 𝜋-Calculus in Guarded Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {379-378}, doi = {10.1145/3372885.3373814}, year = {2020}, } Publisher's Version
	Visser, Eelco	CPP '20: "Intrinsically-Typed Definitional ..." Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser (Delft University of Technology, Netherlands) @InProceedings{CPP20p397, author = {Arjen Rouvoet and Casper Bach Poulsen and Robbert Krebbers and Eelco Visser}, title = {Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {397-396}, doi = {10.1145/3372885.3373818}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Wang, Qingxiang	CPP '20: "Exploration of Neural Machine ..." Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban (University of Innsbruck, Austria; Czech Technical University in Prague, Czechia; University of Warsaw, Poland) @InProceedings{CPP20p145, author = {Qingxiang Wang and Chad Brown and Cezary Kaliszyk and Josef Urban}, title = {Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {145-144}, doi = {10.1145/3372885.3373827}, year = {2020}, } Publisher's Version
	Wuttke, Maximilian	CPP '20: "Verified Programming of Turing ..." Verified Programming of Turing Machines in Coq Yannick Forster, Fabian Kunze, and Maximilian Wuttke (Saarland University, Germany) @InProceedings{CPP20p181, author = {Yannick Forster and Fabian Kunze and Maximilian Wuttke}, title = {Verified Programming of Turing Machines in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {181-180}, doi = {10.1145/3372885.3373816}, year = {2020}, } Publisher's Version
	Xu, Chuangjie	CPP '20: "Three Equivalent Ordinal Notation ..." Three Equivalent Ordinal Notation Systems in Cubical Agda Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani (University of Strathclyde, UK; LMU Munich, Germany) @InProceedings{CPP20p253, author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani}, title = {Three Equivalent Ordinal Notation Systems in Cubical Agda}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {253-252}, doi = {10.1145/3372885.3373835}, year = {2020}, } Publisher's Version Published Artifact Artifacts Available
	Zakowski, Yannick	CPP '20: "An Equational Theory for Weak ..." An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea) @InProceedings{CPP20p127, author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic}, title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3372885.3373813}, year = {2020}, } Publisher's Version
	Zdancewic, Steve	CPP '20: "An Equational Theory for Weak ..." An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic (University of Pennsylvania, USA; Seoul National University, South Korea) @InProceedings{CPP20p127, author = {Yannick Zakowski and Paul He and Chung-Kil Hur and Steve Zdancewic}, title = {An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {127-126}, doi = {10.1145/3372885.3373813}, year = {2020}, } Publisher's Version

74 authors

proc time: 0.04