CPP '21: "Towards Formally Verified ..."
Towards Formally Verified Compilation of Tag-Based Policy Enforcement
CHR Chhak, Andrew Tolmach, and Sean Anderson
(Portland State University, USA)
@InProceedings{CPP21p232,
author = {CHR Chhak and Andrew Tolmach and Sean Anderson},
title = {Towards Formally Verified Compilation of Tag-Based Policy Enforcement},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {232-231},
doi = {10.1145/3437992.3439929},
year = {2021},
}
Publisher's Version
CPP '21: "Extracting Smart Contracts ..."
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP21p190,
author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters},
title = {Extracting Smart Contracts Tested and Verified in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3437992.3439934},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Formal Proof of PAC Learnability ..."
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)
@InProceedings{CPP21p43,
author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan},
title = {A Formal Proof of PAC Learnability for Decision Stumps},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {43-42},
doi = {10.1145/3437992.3439917},
year = {2021},
}
Publisher's Version
CPP '21: "Lassie: HOL4 Tactics by Example ..."
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)
@InProceedings{CPP21p337,
author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar},
title = {Lassie: HOL4 Tactics by Example},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3437992.3439925},
year = {2021},
}
Publisher's Version
CPP '21: "Developing and Certifying ..."
Developing and Certifying Datalog Optimizations in Coq/MathComp
Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin
(Orange Labs, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)
@InProceedings{CPP21p274,
author = {Pierre-Léo Bégay and Pierre Crégut and Jean-François Monin},
title = {Developing and Certifying Datalog Optimizations in Coq/MathComp},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {274-273},
doi = {10.1145/3437992.3439913},
year = {2021},
}
Publisher's Version
CPP '21: "Machine-Checked Semantic Session ..."
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
@InProceedings{CPP21p295,
author = {Jonas Kastberg Hinrichsen and Daniël Louwrink and Robbert Krebbers and Jesper Bengtson},
title = {Machine-Checked Semantic Session Typing},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {295-294},
doi = {10.1145/3437992.3439914},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Coq Formalization of Data ..."
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)
@InProceedings{CPP21p253,
author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini},
title = {A Coq Formalization of Data Provenance},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3437992.3439920},
year = {2021},
}
Publisher's Version
CPP '21: "Contextual Refinement of the ..."
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)
@InProceedings{CPP21p148,
author = {Simon Friis Vindum and Lars Birkedal},
title = {Contextual Refinement of the Michael-Scott Queue (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {148-147},
doi = {10.1145/3437992.3439930},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Reasoning about Monotonicity ..."
Reasoning about Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
(Aarhus University, Denmark)
@InProceedings{CPP21p169,
author = {Amin Timany and Lars Birkedal},
title = {Reasoning about Monotonicity in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {169-168},
doi = {10.1145/3437992.3439931},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Modular Isabelle Framework ..."
A Modular Isabelle Framework for Verifying Saturation Provers
Sophie Tourret and Jasmin Blanchette
(MPI-INF, Germany; Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP21p358,
author = {Sophie Tourret and Jasmin Blanchette},
title = {A Modular Isabelle Framework for Verifying Saturation Provers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {358-357},
doi = {10.1145/3437992.3439912},
year = {2021},
}
Publisher's Version
CPP '21: "Lassie: HOL4 Tactics by Example ..."
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)
@InProceedings{CPP21p337,
author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar},
title = {Lassie: HOL4 Tactics by Example},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3437992.3439925},
year = {2021},
}
Publisher's Version
CPP '21: "Towards Efficient and Verified ..."
Towards Efficient and Verified Virtual Machines for Dynamic Languages
Martin Desharnais and Stefan Brunthaler
(Bundeswehr University Munich, Germany)
@InProceedings{CPP21p127,
author = {Martin Desharnais and Stefan Brunthaler},
title = {Towards Efficient and Verified Virtual Machines for Dynamic Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3437992.3439923},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formal Verification of Authenticated, ..."
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)
@InProceedings{CPP21p211,
author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {211-210},
doi = {10.1145/3437992.3439924},
year = {2021},
}
Publisher's Version
CPP '21: "Formalizing Category Theory ..."
Formalizing Category Theory in Agda
Jason Z. S. Hu and Jacques Carette
(McGill University, Canada; McMaster University, Canada)
@InProceedings{CPP21p526,
author = {Jason Z. S. Hu and Jacques Carette},
title = {Formalizing Category Theory in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {526-525},
doi = {10.1145/3437992.3439922},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formal Verification of Authenticated, ..."
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)
@InProceedings{CPP21p211,
author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {211-210},
doi = {10.1145/3437992.3439924},
year = {2021},
}
Publisher's Version
CPP '21: "On the Formalisation of Kolmogorov ..."
On the Formalisation of Kolmogorov Complexity
Elliot Catt and Michael Norrish
(Australian National University, Australia; Data61 at CSIRO, Australia)
@InProceedings{CPP21p463,
author = {Elliot Catt and Michael Norrish},
title = {On the Formalisation of Kolmogorov Complexity},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {463-462},
doi = {10.1145/3437992.3439921},
year = {2021},
}
Publisher's Version
CPP '21: "Towards Formally Verified ..."
Towards Formally Verified Compilation of Tag-Based Policy Enforcement
CHR Chhak, Andrew Tolmach, and Sean Anderson
(Portland State University, USA)
@InProceedings{CPP21p232,
author = {CHR Chhak and Andrew Tolmach and Sean Anderson},
title = {Towards Formally Verified Compilation of Tag-Based Policy Enforcement},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {232-231},
doi = {10.1145/3437992.3439929},
year = {2021},
}
Publisher's Version
CPP '21: "A Coq Formalization of Data ..."
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)
@InProceedings{CPP21p253,
author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini},
title = {A Coq Formalization of Data Provenance},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3437992.3439920},
year = {2021},
}
Publisher's Version
CPP '21: "Formalizing the Ring of Witt ..."
Formalizing the Ring of Witt Vectors
Johan Commelin and Robert Y. Lewis
(University of Freiburg, Germany; Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP21p421,
author = {Johan Commelin and Robert Y. Lewis},
title = {Formalizing the Ring of Witt Vectors},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {421-420},
doi = {10.1145/3437992.3439919},
year = {2021},
}
Publisher's Version
CPP '21: "A Coq Formalization of Data ..."
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)
@InProceedings{CPP21p253,
author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini},
title = {A Coq Formalization of Data Provenance},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3437992.3439920},
year = {2021},
}
Publisher's Version
CPP '21: "Developing and Certifying ..."
Developing and Certifying Datalog Optimizations in Coq/MathComp
Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin
(Orange Labs, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)
@InProceedings{CPP21p274,
author = {Pierre-Léo Bégay and Pierre Crégut and Jean-François Monin},
title = {Developing and Certifying Datalog Optimizations in Coq/MathComp},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {274-273},
doi = {10.1145/3437992.3439913},
year = {2021},
}
Publisher's Version
CPP '21: "Lassie: HOL4 Tactics by Example ..."
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)
@InProceedings{CPP21p337,
author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar},
title = {Lassie: HOL4 Tactics by Example},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3437992.3439925},
year = {2021},
}
Publisher's Version
CPP '21: "Towards Efficient and Verified ..."
Towards Efficient and Verified Virtual Machines for Dynamic Languages
Martin Desharnais and Stefan Brunthaler
(Bundeswehr University Munich, Germany)
@InProceedings{CPP21p127,
author = {Martin Desharnais and Stefan Brunthaler},
title = {Towards Efficient and Verified Virtual Machines for Dynamic Languages},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {127-126},
doi = {10.1145/3437992.3439923},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formal Verification of Semi-algebraic ..."
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
J. Tanner Slagel, Lauren White, and Aaron Dutle
(NASA Langley Research Center, USA; Kansas State University, USA)
@InProceedings{CPP21p442,
author = {J. Tanner Slagel and Lauren White and Aaron Dutle},
title = {Formal Verification of Semi-algebraic Sets and Real Analytic Functions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {442-441},
doi = {10.1145/3437992.3439933},
year = {2021},
}
Publisher's Version
CPP '21: "A Verified Decision Procedure ..."
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)
@InProceedings{CPP21p400,
author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer},
title = {A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {400-399},
doi = {10.1145/3437992.3439918},
year = {2021},
}
Publisher's Version
CPP '21: "CertRL: Formalizing Convergence ..."
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
@InProceedings{CPP21p64,
author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton},
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {64-63},
doi = {10.1145/3437992.3439927},
year = {2021},
}
Publisher's Version
CPP '21: "Lassie: HOL4 Tactics by Example ..."
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)
@InProceedings{CPP21p337,
author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar},
title = {Lassie: HOL4 Tactics by Example},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3437992.3439925},
year = {2021},
}
Publisher's Version
CPP '21: "An Isabelle/HOL Formalization ..."
An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR
Max W. Haslbeck and René Thiemann
(University of Innsbruck, Austria)
@InProceedings{CPP21p379,
author = {Max W. Haslbeck and René Thiemann},
title = {An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {379-378},
doi = {10.1145/3437992.3439935},
year = {2021},
}
Publisher's Version
CPP '21: "Machine-Checked Semantic Session ..."
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
@InProceedings{CPP21p295,
author = {Jonas Kastberg Hinrichsen and Daniël Louwrink and Robbert Krebbers and Jesper Bengtson},
title = {Machine-Checked Semantic Session Typing},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {295-294},
doi = {10.1145/3437992.3439914},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formalizing Category Theory ..."
Formalizing Category Theory in Agda
Jason Z. S. Hu and Jacques Carette
(McGill University, Canada; McMaster University, Canada)
@InProceedings{CPP21p526,
author = {Jason Z. S. Hu and Jacques Carette},
title = {Formalizing Category Theory in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {526-525},
doi = {10.1145/3437992.3439922},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Coq Formalization of Data ..."
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)
@InProceedings{CPP21p253,
author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini},
title = {A Coq Formalization of Data Provenance},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3437992.3439920},
year = {2021},
}
Publisher's Version
CPP '21: "The Generalised Continuum ..."
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Dominik Kirst and Felix Rech
(Saarland University, Germany)
@InProceedings{CPP21p505,
author = {Dominik Kirst and Felix Rech},
title = {The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {505-504},
doi = {10.1145/3437992.3439932},
year = {2021},
}
Publisher's Version
CPP '21: "Machine-Checked Semantic Session ..."
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
@InProceedings{CPP21p295,
author = {Jonas Kastberg Hinrichsen and Daniël Louwrink and Robbert Krebbers and Jesper Bengtson},
title = {Machine-Checked Semantic Session Typing},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {295-294},
doi = {10.1145/3437992.3439914},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "An Anti-Locally-Nameless Approach ..."
An Anti-Locally-Nameless Approach to Formalizing Quantifiers
Olivier Laurent
(CNRS, France; ENS Lyon, France)
@InProceedings{CPP21p484,
author = {Olivier Laurent},
title = {An Anti-Locally-Nameless Approach to Formalizing Quantifiers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {484-483},
doi = {10.1145/3437992.3439926},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formalizing the Ring of Witt ..."
Formalizing the Ring of Witt Vectors
Johan Commelin and Robert Y. Lewis
(University of Freiburg, Germany; Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP21p421,
author = {Johan Commelin and Robert Y. Lewis},
title = {Formalizing the Ring of Witt Vectors},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {421-420},
doi = {10.1145/3437992.3439919},
year = {2021},
}
Publisher's Version
CPP '21: "A Novice-Friendly Induction ..."
A Novice-Friendly Induction Tactic for Lean
Jannis Limperg
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP21p316,
author = {Jannis Limperg},
title = {A Novice-Friendly Induction Tactic for Lean},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {316-315},
doi = {10.1145/3437992.3439928},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Verified Decision Procedure ..."
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)
@InProceedings{CPP21p400,
author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer},
title = {A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {400-399},
doi = {10.1145/3437992.3439918},
year = {2021},
}
Publisher's Version
CPP '21: "Lutsig: A Verified Verilog ..."
Lutsig: A Verified Verilog Compiler for Verified Circuit Development
Andreas Lööw
(Chalmers University of Technology, Sweden)
@InProceedings{CPP21p106,
author = {Andreas Lööw},
title = {Lutsig: A Verified Verilog Compiler for Verified Circuit Development},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {106-105},
doi = {10.1145/3437992.3439916},
year = {2021},
}
Publisher's Version
CPP '21: "Machine-Checked Semantic Session ..."
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
@InProceedings{CPP21p295,
author = {Jonas Kastberg Hinrichsen and Daniël Louwrink and Robbert Krebbers and Jesper Bengtson},
title = {Machine-Checked Semantic Session Typing},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {295-294},
doi = {10.1145/3437992.3439914},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Lassie: HOL4 Tactics by Example ..."
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany; McGill University, Canada)
@InProceedings{CPP21p337,
author = {Heiko Becker and Nathaniel Bos and Ivan Gavran and Eva Darulova and Rupak Majumdar},
title = {Lassie: HOL4 Tactics by Example},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {337-336},
doi = {10.1145/3437992.3439925},
year = {2021},
}
Publisher's Version
CPP '21: "A Verified Decision Procedure ..."
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)
@InProceedings{CPP21p400,
author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer},
title = {A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {400-399},
doi = {10.1145/3437992.3439918},
year = {2021},
}
Publisher's Version
CPP '21: "Extracting Smart Contracts ..."
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP21p190,
author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters},
title = {Extracting Smart Contracts Tested and Verified in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3437992.3439934},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "A Verified Decision Procedure ..."
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)
@InProceedings{CPP21p400,
author = {Alexander Lochmann and Aart Middeldorp and Fabian Mitterwallner and Bertram Felgenhauer},
title = {A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {400-399},
doi = {10.1145/3437992.3439918},
year = {2021},
}
Publisher's Version
CPP '21: "Formal Verification of Authenticated, ..."
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)
@InProceedings{CPP21p211,
author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {211-210},
doi = {10.1145/3437992.3439924},
year = {2021},
}
Publisher's Version
CPP '21: "Developing and Certifying ..."
Developing and Certifying Datalog Optimizations in Coq/MathComp
Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin
(Orange Labs, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)
@InProceedings{CPP21p274,
author = {Pierre-Léo Bégay and Pierre Crégut and Jean-François Monin},
title = {Developing and Certifying Datalog Optimizations in Coq/MathComp},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {274-273},
doi = {10.1145/3437992.3439913},
year = {2021},
}
Publisher's Version
CPP '21: "A Minimalistic Verified Bootstrapped ..."
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)
Magnus O. Myreen
(Chalmers University of Technology, Sweden)
@InProceedings{CPP21p85,
author = {Magnus O. Myreen},
title = {A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {85-84},
doi = {10.1145/3437992.3439915},
year = {2021},
}
Publisher's Version
CPP '21: "Extracting Smart Contracts ..."
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP21p190,
author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters},
title = {Extracting Smart Contracts Tested and Verified in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3437992.3439934},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Teaching Algorithms and Data ..."
Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)
Tobias Nipkow
(TU Munich, Germany)
@InProceedings{CPP21p1,
author = {Tobias Nipkow},
title = {Teaching Algorithms and Data Structures with a Proof Assistant (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3437992.3439910},
year = {2021},
}
Publisher's Version
CPP '21: "On the Formalisation of Kolmogorov ..."
On the Formalisation of Kolmogorov Complexity
Elliot Catt and Michael Norrish
(Australian National University, Australia; Data61 at CSIRO, Australia)
@InProceedings{CPP21p463,
author = {Elliot Catt and Michael Norrish},
title = {On the Formalisation of Kolmogorov Complexity},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {463-462},
doi = {10.1145/3437992.3439921},
year = {2021},
}
Publisher's Version
CPP '21: "CertRL: Formalizing Convergence ..."
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
@InProceedings{CPP21p64,
author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton},
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {64-63},
doi = {10.1145/3437992.3439927},
year = {2021},
}
Publisher's Version
CPP '21: "The Generalised Continuum ..."
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Dominik Kirst and Felix Rech
(Saarland University, Germany)
@InProceedings{CPP21p505,
author = {Dominik Kirst and Felix Rech},
title = {The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {505-504},
doi = {10.1145/3437992.3439932},
year = {2021},
}
Publisher's Version
CPP '21: "Underpinning the Foundations: ..."
Underpinning the Foundations: Sail-Based Semantics, Testing, and Reasoning for Production and CHERI-Enabled Architectures (Invited Talk)
Peter Sewell
(University of Cambridge, UK)
@InProceedings{CPP21p22,
author = {Peter Sewell},
title = {Underpinning the Foundations: Sail-Based Semantics, Testing, and Reasoning for Production and CHERI-Enabled Architectures (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {22-21},
doi = {10.1145/3437992.3439911},
year = {2021},
}
Publisher's Version
CPP '21: "CertRL: Formalizing Convergence ..."
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
@InProceedings{CPP21p64,
author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton},
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {64-63},
doi = {10.1145/3437992.3439927},
year = {2021},
}
Publisher's Version
CPP '21: "Formal Verification of Authenticated, ..."
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)
@InProceedings{CPP21p211,
author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {211-210},
doi = {10.1145/3437992.3439924},
year = {2021},
}
Publisher's Version
CPP '21: "Formal Verification of Semi-algebraic ..."
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
J. Tanner Slagel, Lauren White, and Aaron Dutle
(NASA Langley Research Center, USA; Kansas State University, USA)
@InProceedings{CPP21p442,
author = {J. Tanner Slagel and Lauren White and Aaron Dutle},
title = {Formal Verification of Semi-algebraic Sets and Real Analytic Functions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {442-441},
doi = {10.1145/3437992.3439933},
year = {2021},
}
Publisher's Version
CPP '21: "Extracting Smart Contracts ..."
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP21p190,
author = {Danil Annenkov and Mikkel Milo and Jakob Botsch Nielsen and Bas Spitters},
title = {Extracting Smart Contracts Tested and Verified in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {190-189},
doi = {10.1145/3437992.3439934},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formal Verification of Authenticated, ..."
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Dfinity Foundation, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; INESC TEC, Portugal)
@InProceedings{CPP21p211,
author = {Victor Cacciari Miraldo and Harold Carr and Mark Moir and Lisandra Silva and Guy L. Steele Jr.},
title = {Formal Verification of Authenticated, Append-Only Skip Lists in Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {211-210},
doi = {10.1145/3437992.3439924},
year = {2021},
}
Publisher's Version
CPP '21: "A Formal Proof of PAC Learnability ..."
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)
@InProceedings{CPP21p43,
author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan},
title = {A Formal Proof of PAC Learnability for Decision Stumps},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {43-42},
doi = {10.1145/3437992.3439917},
year = {2021},
}
Publisher's Version
CPP '21: "An Isabelle/HOL Formalization ..."
An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR
Max W. Haslbeck and René Thiemann
(University of Innsbruck, Austria)
@InProceedings{CPP21p379,
author = {Max W. Haslbeck and René Thiemann},
title = {An Isabelle/HOL Formalization of AProVE’s Termination Method for LLVM IR},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {379-378},
doi = {10.1145/3437992.3439935},
year = {2021},
}
Publisher's Version
CPP '21: "Reasoning about Monotonicity ..."
Reasoning about Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
(Aarhus University, Denmark)
@InProceedings{CPP21p169,
author = {Amin Timany and Lars Birkedal},
title = {Reasoning about Monotonicity in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {169-168},
doi = {10.1145/3437992.3439931},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Towards Formally Verified ..."
Towards Formally Verified Compilation of Tag-Based Policy Enforcement
CHR Chhak, Andrew Tolmach, and Sean Anderson
(Portland State University, USA)
@InProceedings{CPP21p232,
author = {CHR Chhak and Andrew Tolmach and Sean Anderson},
title = {Towards Formally Verified Compilation of Tag-Based Policy Enforcement},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {232-231},
doi = {10.1145/3437992.3439929},
year = {2021},
}
Publisher's Version
CPP '21: "A Modular Isabelle Framework ..."
A Modular Isabelle Framework for Verifying Saturation Provers
Sophie Tourret and Jasmin Blanchette
(MPI-INF, Germany; Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP21p358,
author = {Sophie Tourret and Jasmin Blanchette},
title = {A Modular Isabelle Framework for Verifying Saturation Provers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {358-357},
doi = {10.1145/3437992.3439912},
year = {2021},
}
Publisher's Version
CPP '21: "CertRL: Formalizing Convergence ..."
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
@InProceedings{CPP21p64,
author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton},
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {64-63},
doi = {10.1145/3437992.3439927},
year = {2021},
}
Publisher's Version
CPP '21: "A Formal Proof of PAC Learnability ..."
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)
@InProceedings{CPP21p43,
author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan},
title = {A Formal Proof of PAC Learnability for Decision Stumps},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {43-42},
doi = {10.1145/3437992.3439917},
year = {2021},
}
Publisher's Version
CPP '21: "A Formal Proof of PAC Learnability ..."
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)
@InProceedings{CPP21p43,
author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan},
title = {A Formal Proof of PAC Learnability for Decision Stumps},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {43-42},
doi = {10.1145/3437992.3439917},
year = {2021},
}
Publisher's Version
CPP '21: "CertRL: Formalizing Convergence ..."
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
@InProceedings{CPP21p64,
author = {Koundinya Vajjha and Avraham Shinnar and Barry Trager and Vasily Pestun and Nathan Fulton},
title = {CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {64-63},
doi = {10.1145/3437992.3439927},
year = {2021},
}
Publisher's Version
CPP '21: "Contextual Refinement of the ..."
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)
@InProceedings{CPP21p148,
author = {Simon Friis Vindum and Lars Birkedal},
title = {Contextual Refinement of the Michael-Scott Queue (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {148-147},
doi = {10.1145/3437992.3439930},
year = {2021},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '21: "Formal Verification of Semi-algebraic ..."
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
J. Tanner Slagel, Lauren White, and Aaron Dutle
(NASA Langley Research Center, USA; Kansas State University, USA)
@InProceedings{CPP21p442,
author = {J. Tanner Slagel and Lauren White and Aaron Dutle},
title = {Formal Verification of Semi-algebraic Sets and Real Analytic Functions},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {442-441},
doi = {10.1145/3437992.3439933},
year = {2021},
}
Publisher's Version
CPP '21: "A Coq Formalization of Data ..."
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini
(LRI, France; University of Paris-Saclay, France; CNRS, France)
@InProceedings{CPP21p253,
author = {Véronique Benzaken and Sarah Cohen-Boulakia and Évelyne Contejean and Chantal Keller and Rébecca Zucchini},
title = {A Coq Formalization of Data Provenance},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {253-252},
doi = {10.1145/3437992.3439920},
year = {2021},
}
Publisher's Version