CPP '22: "Implementing a Category-Theoretic ..."
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg
(TU Delft, Netherlands; University of Birmingham, UK; IRIT, France; Université de Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)
@InProceedings{CPP22p553,
author = {Benedikt Ahrens and Ralph Matthes and Anders Mörtberg},
title = {Implementing a Category-Theoretic Framework for Typed Abstract Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {553-552},
doi = {10.1145/3497775.3503678},
year = {2022},
}
Publisher's Version
CPP '22: "Certified Abstract Machines ..."
Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)
@InProceedings{CPP22p139,
author = {Guillaume Ambal and Sergueï Lenglet and Alan Schmitt},
title = {Certified Abstract Machines for Skeletal Semantics},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {139-138},
doi = {10.1145/3497775.3503676},
year = {2022},
}
Publisher's Version
CPP '22: "The seL4 Verification: The ..."
The seL4 Verification: The Art and Craft of Proof and the Reality of Commercial Support (Invited Talk)
June Andronick
(Proofcraft, Australia; UNSW, Australia; seL4 Foundation, Australia)
@InProceedings{CPP22p1,
author = {June Andronick},
title = {The seL4 Verification: The Art and Craft of Proof and the Reality of Commercial Support (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3497775.3505265},
year = {2022},
}
Publisher's Version
CPP '22: "Coq’s Vibrant Ecosystem ..."
Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)
Andrew W. Appel
(Princeton University, USA)
@InProceedings{CPP22p24,
author = {Andrew W. Appel},
title = {Coq’s Vibrant Ecosystem for Verification Engineering (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {24-23},
doi = {10.1145/3497775.3503951},
year = {2022},
}
Publisher's Version
CPP '22: "A Verified Algebraic Representation ..."
A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, Israel)
@InProceedings{CPP22p300,
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
title = {A Verified Algebraic Representation of Cairo Program Execution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {300-299},
doi = {10.1145/3497775.3503675},
year = {2022},
}
Publisher's Version
CPP '22: "Mechanized Verification of ..."
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Simon Friis Vindum, Dan Frumin, and Lars Birkedal
(Aarhus University, Denmark; University of Groningen, Netherlands)
@InProceedings{CPP22p208,
author = {Simon Friis Vindum and Dan Frumin and Lars Birkedal},
title = {Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {208-207},
doi = {10.1145/3497775.3503689},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "Applying Formal Verification ..."
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Meta, France; Meta, USA; Cornell University, USA; Meta, UK; University College London, UK)
@InProceedings{CPP22p231,
author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
title = {Applying Formal Verification to Microkernel IPC at Meta},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {231-230},
doi = {10.1145/3497775.3503681},
year = {2022},
}
Publisher's Version
CPP '22: "Windmills of the Minds: An ..."
Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem
Hing Lun Chan
(Australian National University, Australia)
@InProceedings{CPP22p461,
author = {Hing Lun Chan},
title = {Windmills of the Minds: An Algorithm for Fermat’s Two Squares Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {461-460},
doi = {10.1145/3497775.3503673},
year = {2022},
}
Publisher's Version
CPP '22: "Specification and Verification ..."
Specification and Verification of a Transient Stack
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; University of Strasbourg, France; CNRS, France)
@InProceedings{CPP22p185,
author = {Alexandre Moine and Arthur Charguéraud and François Pottier},
title = {Specification and Verification of a Transient Stack},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {185-184},
doi = {10.1145/3497775.3503677},
year = {2022},
}
Publisher's Version
CPP '22: "Overcoming Restraint: Composing ..."
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Louis Cheung, Liam O'Connor, and Christine Rizkallah
(University of Melbourne, Australia; University of Edinburgh, UK)
@InProceedings{CPP22p70,
author = {Louis Cheung and Liam O'Connor and Christine Rizkallah},
title = {Overcoming Restraint: Composing Verification of Foreign Functions with Cogent},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {70-69},
doi = {10.1145/3497775.3503686},
year = {2022},
}
Publisher's Version
CPP '22: "A Compositional Proof Framework ..."
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)
@InProceedings{CPP22p162,
author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle},
title = {A Compositional Proof Framework for FRETish Requirements},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {162-161},
doi = {10.1145/3497775.3503685},
year = {2022},
}
Publisher's Version
CPP '22: "Formal Verification of a Distributed ..."
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)
@InProceedings{CPP22p277,
author = {William Schultz and Ian Dardik and Stavros Tripakis},
title = {Formal Verification of a Distributed Dynamic Reconfiguration Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {277-276},
doi = {10.1145/3497775.3503688},
year = {2022},
}
Publisher's Version
CPP '22: "A Drag-and-Drop Proof Tactic ..."
A Drag-and-Drop Proof Tactic
Pablo Donato, Pierre-Yves Strub, and Benjamin Werner
(École Polytechnique, France)
@InProceedings{CPP22p369,
author = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner},
title = {A Drag-and-Drop Proof Tactic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3497775.3503692},
year = {2022},
}
Publisher's Version
CPP '22: "A Compositional Proof Framework ..."
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)
@InProceedings{CPP22p162,
author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle},
title = {A Compositional Proof Framework for FRETish Requirements},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {162-161},
doi = {10.1145/3497775.3503685},
year = {2022},
}
Publisher's Version
CPP '22: "Verbatim++: Verified, Optimized, ..."
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Derek Egolf, Sam Lasser, and Kathleen Fisher
(Northeastern University, USA; Tufts University, USA)
@InProceedings{CPP22p93,
author = {Derek Egolf and Sam Lasser and Kathleen Fisher},
title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {93-92},
doi = {10.1145/3497775.3503694},
year = {2022},
}
Publisher's Version
CPP '22: "Safe, Fast, Concurrent Proof ..."
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Michael Färber
(University of Innsbruck, Austria)
@InProceedings{CPP22p415,
author = {Michael Färber},
title = {Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {415-414},
doi = {10.1145/3497775.3503683},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "Reflection, Rewinding, and ..."
Reflection, Rewinding, and Coin-Toss in EasyCrypt
Denis Firsov and Dominique Unruh
(Tallinn University of Technology, Estonia; Guardtime, Estonia; University of Tartu, Estonia)
@InProceedings{CPP22p323,
author = {Denis Firsov and Dominique Unruh},
title = {Reflection, Rewinding, and Coin-Toss in EasyCrypt},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {323-322},
doi = {10.1145/3497775.3503693},
year = {2022},
}
Publisher's Version
CPP '22: "Verbatim++: Verified, Optimized, ..."
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Derek Egolf, Sam Lasser, and Kathleen Fisher
(Northeastern University, USA; Tufts University, USA)
@InProceedings{CPP22p93,
author = {Derek Egolf and Sam Lasser and Kathleen Fisher},
title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {93-92},
doi = {10.1145/3497775.3503694},
year = {2022},
}
Publisher's Version
CPP '22: "Mechanized Verification of ..."
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Simon Friis Vindum, Dan Frumin, and Lars Birkedal
(Aarhus University, Denmark; University of Groningen, Netherlands)
@InProceedings{CPP22p208,
author = {Simon Friis Vindum and Dan Frumin and Lars Birkedal},
title = {Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {208-207},
doi = {10.1145/3497775.3503689},
year = {2022},
}
Publisher's Version
CPP '22: "Semantic Cut Elimination for ..."
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan Frumin
(University of Groningen, Netherlands)
@InProceedings{CPP22p530,
author = {Dan Frumin},
title = {Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {530-529},
doi = {10.1145/3497775.3503690},
year = {2022},
}
Publisher's Version
CPP '22: "(Deep) Induction Rules for ..."
(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi
(Appalachian State University, USA)
@InProceedings{CPP22p576,
author = {Patricia Johann and Enrico Ghiorzi},
title = {(Deep) Induction Rules for GADTs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {576-575},
doi = {10.1145/3497775.3503680},
year = {2022},
}
Publisher's Version
CPP '22: "A Compositional Proof Framework ..."
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)
@InProceedings{CPP22p162,
author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle},
title = {A Compositional Proof Framework for FRETish Requirements},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {162-161},
doi = {10.1145/3497775.3503685},
year = {2022},
}
Publisher's Version
CPP '22: "A Verified Algebraic Representation ..."
A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, Israel)
@InProceedings{CPP22p300,
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
title = {A Verified Algebraic Representation of Cairo Program Execution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {300-299},
doi = {10.1145/3497775.3503675},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "(Deep) Induction Rules for ..."
(Deep) Induction Rules for GADTs
Patricia Johann and Enrico Ghiorzi
(Appalachian State University, USA)
@InProceedings{CPP22p576,
author = {Patricia Johann and Enrico Ghiorzi},
title = {(Deep) Induction Rules for GADTs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {576-575},
doi = {10.1145/3497775.3503680},
year = {2022},
}
Publisher's Version
CPP '22: "CertiStr: A Certified String ..."
CertiStr: A Certified String Solver
Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader
(TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
@InProceedings{CPP22p392,
author = {Shuanglong Kan and Anthony Widjaja Lin and Philipp Rümmer and Micha Schrader},
title = {CertiStr: A Certified String Solver},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {392-391},
doi = {10.1145/3497775.3503691},
year = {2022},
}
Publisher's Version
CPP '22: "A Machine-Checked Direct Proof ..."
A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
Ariel Kellison
(Cornell University, USA)
@InProceedings{CPP22p484,
author = {Ariel Kellison},
title = {A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {484-483},
doi = {10.1145/3497775.3503682},
year = {2022},
}
Publisher's Version
CPP '22: "Undecidability, Incompleteness, ..."
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Mark Koch and Dominik Kirst
(Saarland University, Germany)
@InProceedings{CPP22p507,
author = {Mark Koch and Dominik Kirst},
title = {Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {507-506},
doi = {10.1145/3497775.3503684},
year = {2022},
}
Publisher's Version
CPP '22: "Applying Formal Verification ..."
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Meta, France; Meta, USA; Cornell University, USA; Meta, UK; University College London, UK)
@InProceedings{CPP22p231,
author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
title = {Applying Formal Verification to Microkernel IPC at Meta},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {231-230},
doi = {10.1145/3497775.3503681},
year = {2022},
}
Publisher's Version
CPP '22: "Undecidability, Incompleteness, ..."
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Mark Koch and Dominik Kirst
(Saarland University, Germany)
@InProceedings{CPP22p507,
author = {Mark Koch and Dominik Kirst},
title = {Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {507-506},
doi = {10.1145/3497775.3503684},
year = {2022},
}
Publisher's Version
CPP '22: "Verbatim++: Verified, Optimized, ..."
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Derek Egolf, Sam Lasser, and Kathleen Fisher
(Northeastern University, USA; Tufts University, USA)
@InProceedings{CPP22p93,
author = {Derek Egolf and Sam Lasser and Kathleen Fisher},
title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {93-92},
doi = {10.1145/3497775.3503694},
year = {2022},
}
Publisher's Version
CPP '22: "Certified Abstract Machines ..."
Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)
@InProceedings{CPP22p139,
author = {Guillaume Ambal and Sergueï Lenglet and Alan Schmitt},
title = {Certified Abstract Machines for Skeletal Semantics},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {139-138},
doi = {10.1145/3497775.3503676},
year = {2022},
}
Publisher's Version
CPP '22: "A Verified Algebraic Representation ..."
A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, Israel)
@InProceedings{CPP22p300,
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
title = {A Verified Algebraic Representation of Cairo Program Execution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {300-299},
doi = {10.1145/3497775.3503675},
year = {2022},
}
Publisher's Version
CPP '22: "CertiStr: A Certified String ..."
CertiStr: A Certified String Solver
Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader
(TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
@InProceedings{CPP22p392,
author = {Shuanglong Kan and Anthony Widjaja Lin and Philipp Rümmer and Micha Schrader},
title = {CertiStr: A Certified String Solver},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {392-391},
doi = {10.1145/3497775.3503691},
year = {2022},
}
Publisher's Version
CPP '22: "Implementing a Category-Theoretic ..."
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg
(TU Delft, Netherlands; University of Birmingham, UK; IRIT, France; Université de Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)
@InProceedings{CPP22p553,
author = {Benedikt Ahrens and Ralph Matthes and Anders Mörtberg},
title = {Implementing a Category-Theoretic Framework for Typed Abstract Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {553-552},
doi = {10.1145/3497775.3503678},
year = {2022},
}
Publisher's Version
CPP '22: "An Extension of the Framework ..."
An Extension of the Framework Types-To-Sets for Isabelle/HOL
Mihails Milehins
@InProceedings{CPP22p346,
author = {Mihails Milehins},
title = {An Extension of the Framework Types-To-Sets for Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {346-345},
doi = {10.1145/3497775.3503674},
year = {2022},
}
Publisher's Version
CPP '22: "Forward Build Systems, Formally ..."
Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Meta, UK)
@InProceedings{CPP22p254,
author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt},
title = {Forward Build Systems, Formally},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {254-253},
doi = {10.1145/3497775.3503687},
year = {2022},
}
Publisher's Version
CPP '22: "Specification and Verification ..."
Specification and Verification of a Transient Stack
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; University of Strasbourg, France; CNRS, France)
@InProceedings{CPP22p185,
author = {Alexandre Moine and Arthur Charguéraud and François Pottier},
title = {Specification and Verification of a Transient Stack},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {185-184},
doi = {10.1145/3497775.3503677},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "Implementing a Category-Theoretic ..."
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg
(TU Delft, Netherlands; University of Birmingham, UK; IRIT, France; Université de Toulouse, France; CNRS, France; Toulouse INP, France; UT3, France; Stockholm University, Sweden)
@InProceedings{CPP22p553,
author = {Benedikt Ahrens and Ralph Matthes and Anders Mörtberg},
title = {Implementing a Category-Theoretic Framework for Typed Abstract Syntax},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {553-552},
doi = {10.1145/3497775.3503678},
year = {2022},
}
Publisher's Version
CPP '22: "Structural Embeddings Revisited ..."
Structural Embeddings Revisited (Invited Talk)
César Muñoz
(AWS, USA)
@InProceedings{CPP22p47,
author = {César Muñoz},
title = {Structural Embeddings Revisited (Invited Talk)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {47-46},
doi = {10.1145/3497775.3503949},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "Formalising Lie Algebras ..."
Formalising Lie Algebras
Oliver Nash
(Imperial College London, UK)
@InProceedings{CPP22p438,
author = {Oliver Nash},
title = {Formalising Lie Algebras},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {438-437},
doi = {10.1145/3497775.3503672},
year = {2022},
}
Publisher's Version
CPP '22: "Overcoming Restraint: Composing ..."
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Louis Cheung, Liam O'Connor, and Christine Rizkallah
(University of Melbourne, Australia; University of Edinburgh, UK)
@InProceedings{CPP22p70,
author = {Louis Cheung and Liam O'Connor and Christine Rizkallah},
title = {Overcoming Restraint: Composing Verification of Foreign Functions with Cogent},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {70-69},
doi = {10.1145/3497775.3503686},
year = {2022},
}
Publisher's Version
CPP '22: "Applying Formal Verification ..."
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Meta, France; Meta, USA; Cornell University, USA; Meta, UK; University College London, UK)
@InProceedings{CPP22p231,
author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
title = {Applying Formal Verification to Microkernel IPC at Meta},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {231-230},
doi = {10.1145/3497775.3503681},
year = {2022},
}
Publisher's Version
CPP '22: "Specification and Verification ..."
Specification and Verification of a Transient Stack
Alexandre Moine, Arthur Charguéraud, and François Pottier
(Inria, France; University of Strasbourg, France; CNRS, France)
@InProceedings{CPP22p185,
author = {Alexandre Moine and Arthur Charguéraud and François Pottier},
title = {Specification and Verification of a Transient Stack},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {185-184},
doi = {10.1145/3497775.3503677},
year = {2022},
}
Publisher's Version
CPP '22: "A Compositional Proof Framework ..."
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)
@InProceedings{CPP22p162,
author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle},
title = {A Compositional Proof Framework for FRETish Requirements},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {162-161},
doi = {10.1145/3497775.3503685},
year = {2022},
}
Publisher's Version
CPP '22: "On Homotopy of Walks and Spherical ..."
On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides
(University of Bergen, Norway)
@InProceedings{CPP22p599,
author = {Jonathan Prieto-Cubides},
title = {On Homotopy of Walks and Spherical Maps in Homotopy Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {599-598},
doi = {10.1145/3497775.3503671},
year = {2022},
}
Publisher's Version
CPP '22: "Overcoming Restraint: Composing ..."
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Louis Cheung, Liam O'Connor, and Christine Rizkallah
(University of Melbourne, Australia; University of Edinburgh, UK)
@InProceedings{CPP22p70,
author = {Louis Cheung and Liam O'Connor and Christine Rizkallah},
title = {Overcoming Restraint: Composing Verification of Foreign Functions with Cogent},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {70-69},
doi = {10.1145/3497775.3503686},
year = {2022},
}
Publisher's Version
CPP '22: "CertiStr: A Certified String ..."
CertiStr: A Certified String Solver
Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader
(TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
@InProceedings{CPP22p392,
author = {Shuanglong Kan and Anthony Widjaja Lin and Philipp Rümmer and Micha Schrader},
title = {CertiStr: A Certified String Solver},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {392-391},
doi = {10.1145/3497775.3503691},
year = {2022},
}
Publisher's Version
CPP '22: "Certified Abstract Machines ..."
Certified Abstract Machines for Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt
(University of Rennes, France; University of Lorraine, France; Inria, France)
@InProceedings{CPP22p139,
author = {Guillaume Ambal and Sergueï Lenglet and Alan Schmitt},
title = {Certified Abstract Machines for Skeletal Semantics},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {139-138},
doi = {10.1145/3497775.3503676},
year = {2022},
}
Publisher's Version
CPP '22: "CertiStr: A Certified String ..."
CertiStr: A Certified String Solver
Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader
(TU Kaiserslautern, Germany; MPI-SWS, Germany; Uppsala University, Sweden)
@InProceedings{CPP22p392,
author = {Shuanglong Kan and Anthony Widjaja Lin and Philipp Rümmer and Micha Schrader},
title = {CertiStr: A Certified String Solver},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {392-391},
doi = {10.1145/3497775.3503691},
year = {2022},
}
Publisher's Version
CPP '22: "Formal Verification of a Distributed ..."
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)
@InProceedings{CPP22p277,
author = {William Schultz and Ian Dardik and Stavros Tripakis},
title = {Formal Verification of a Distributed Dynamic Reconfiguration Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {277-276},
doi = {10.1145/3497775.3503688},
year = {2022},
}
Publisher's Version
CPP '22: "A Verified Algebraic Representation ..."
A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, Israel)
@InProceedings{CPP22p300,
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
title = {A Verified Algebraic Representation of Cairo Program Execution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {300-299},
doi = {10.1145/3497775.3503675},
year = {2022},
}
Publisher's Version
CPP '22: "Formally Verified Superblock ..."
Formally Verified Superblock Scheduling
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; Verimag, France; ENS Lyon, France)
@InProceedings{CPP22p116,
author = {Cyril Six and Léo Gourdin and Sylvain Boulmé and David Monniaux and Justus Fasse and Nicolas Nardino},
title = {Formally Verified Superblock Scheduling},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {116-115},
doi = {10.1145/3497775.3503679},
year = {2022},
}
Publisher's Version
CPP '22: "Forward Build Systems, Formally ..."
Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Meta, UK)
@InProceedings{CPP22p254,
author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt},
title = {Forward Build Systems, Formally},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {254-253},
doi = {10.1145/3497775.3503687},
year = {2022},
}
Publisher's Version
CPP '22: "A Drag-and-Drop Proof Tactic ..."
A Drag-and-Drop Proof Tactic
Pablo Donato, Pierre-Yves Strub, and Benjamin Werner
(École Polytechnique, France)
@InProceedings{CPP22p369,
author = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner},
title = {A Drag-and-Drop Proof Tactic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3497775.3503692},
year = {2022},
}
Publisher's Version
CPP '22: "A Verified Algebraic Representation ..."
A Verified Algebraic Representation of Cairo Program Execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman
(Carnegie Mellon University, USA; Starkware Industries, Israel)
@InProceedings{CPP22p300,
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
title = {A Verified Algebraic Representation of Cairo Program Execution},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {300-299},
doi = {10.1145/3497775.3503675},
year = {2022},
}
Publisher's Version
CPP '22: "A Compositional Proof Framework ..."
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, and Aaron Dutle
(NASA Langley Research Center, USA; National Institute of Aerospace, USA; NASA Ames Research Center, USA)
@InProceedings{CPP22p162,
author = {Esther Conrad and Laura Titolo and Dimitra Giannakopoulou and Thomas Pressburger and Aaron Dutle},
title = {A Compositional Proof Framework for FRETish Requirements},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {162-161},
doi = {10.1145/3497775.3503685},
year = {2022},
}
Publisher's Version
CPP '22: "Forward Build Systems, Formally ..."
Forward Build Systems, Formally
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Meta, UK)
@InProceedings{CPP22p254,
author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt},
title = {Forward Build Systems, Formally},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {254-253},
doi = {10.1145/3497775.3503687},
year = {2022},
}
Publisher's Version
CPP '22: "Formal Verification of a Distributed ..."
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
William Schultz, Ian Dardik, and Stavros Tripakis
(Northeastern University, USA)
@InProceedings{CPP22p277,
author = {William Schultz and Ian Dardik and Stavros Tripakis},
title = {Formal Verification of a Distributed Dynamic Reconfiguration Protocol},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {277-276},
doi = {10.1145/3497775.3503688},
year = {2022},
}
Publisher's Version
CPP '22: "Reflection, Rewinding, and ..."
Reflection, Rewinding, and Coin-Toss in EasyCrypt
Denis Firsov and Dominique Unruh
(Tallinn University of Technology, Estonia; Guardtime, Estonia; University of Tartu, Estonia)
@InProceedings{CPP22p323,
author = {Denis Firsov and Dominique Unruh},
title = {Reflection, Rewinding, and Coin-Toss in EasyCrypt},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {323-322},
doi = {10.1145/3497775.3503693},
year = {2022},
}
Publisher's Version
CPP '22: "Mechanized Verification of ..."
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Simon Friis Vindum, Dan Frumin, and Lars Birkedal
(Aarhus University, Denmark; University of Groningen, Netherlands)
@InProceedings{CPP22p208,
author = {Simon Friis Vindum and Dan Frumin and Lars Birkedal},
title = {Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {208-207},
doi = {10.1145/3497775.3503689},
year = {2022},
}
Publisher's Version
CPP '22: "A Drag-and-Drop Proof Tactic ..."
A Drag-and-Drop Proof Tactic
Pablo Donato, Pierre-Yves Strub, and Benjamin Werner
(École Polytechnique, France)
@InProceedings{CPP22p369,
author = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner},
title = {A Drag-and-Drop Proof Tactic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {369-368},
doi = {10.1145/3497775.3503692},
year = {2022},
}
Publisher's Version
CPP '22: "Applying Formal Verification ..."
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Meta, France; Meta, USA; Cornell University, USA; Meta, UK; University College London, UK)
@InProceedings{CPP22p231,
author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
title = {Applying Formal Verification to Microkernel IPC at Meta},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {231-230},
doi = {10.1145/3497775.3503681},
year = {2022},
}
Publisher's Version
CPP '22: "Applying Formal Verification ..."
Applying Formal Verification to Microkernel IPC at Meta
Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, and Francesco Zappa Nardelli
(Meta, France; Meta, USA; Cornell University, USA; Meta, UK; University College London, UK)
@InProceedings{CPP22p231,
author = {Quentin Carbonneaux and Noam Zilberstein and Christoph Klee and Peter W. O'Hearn and Francesco Zappa Nardelli},
title = {Applying Formal Verification to Microkernel IPC at Meta},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {231-230},
doi = {10.1145/3497775.3503681},
year = {2022},
}
Publisher's Version