Powered by
9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), January 20–21, 2020,
New Orleans, LA, USA
9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)
Frontmatter
Invited Talks
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
Program Verification
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
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
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
Automated Verification and SAT Solving
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
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
Proof Engineering and User Interaction
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
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
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
Decidability and Complexity
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
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
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
Homotopy Type Theory
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
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
Mechanized Metatheory
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
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
Verified Cryptography
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
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
Concurrency and Linearity
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
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
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
Formalized Mathematics 1
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
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
Formalized Mathematics 2
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
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
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
proc time: 0.8