CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt, Cyril Cohen, and Ayumu Saito
(AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan)
@InProceedings{CPP23p45,
author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {45-44},
doi = {10.1145/3573105.3575691},
year = {2023},
}
Publisher's Version
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub
(Inria, France; École Polytechnique, France; Meta, France)
@InProceedings{CPP23p67,
author = {Xavier Allamigeon and Quentin Canu and Pierre-Yves Strub},
title = {A Formal Disproof of Hirsch Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {67-66},
doi = {10.1145/3573105.3575678},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP23p507,
author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters},
title = {Formalising Decentralised Exchanges in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {507-506},
doi = {10.1145/3573105.3575685},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "Compiling Higher-Order Specifications ..."
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
@InProceedings{CPP23p199,
author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi},
title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3573105.3575674},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "Compiling Higher-Order Specifications ..."
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
@InProceedings{CPP23p199,
author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi},
title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3573105.3575674},
year = {2023},
}
Publisher's Version
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP23p111,
author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen},
title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {111-110},
doi = {10.1145/3573105.3575682},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
(University of Cambridge, UK)
@InProceedings{CPP23p397,
author = {Angeliki Koutsoukou-Argyraki and Mantas Bakšys and Chelsea Edmonds},
title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3573105.3575680},
year = {2023},
}
Publisher's Version
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP23p111,
author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen},
title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {111-110},
doi = {10.1145/3573105.3575682},
year = {2023},
}
Publisher's Version
CPP '23: "CompCert: A Journey through ..."
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)
Sandrine Blazy
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP23p1,
author = {Sandrine Blazy},
title = {CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3573105.3579107},
year = {2023},
}
Publisher's Version
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz, Delphine Demange, and Sandrine Blazy
(Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP23p331,
author = {Yann Herklotz and Delphine Demange and Sandrine Blazy},
title = {Mechanised Semantics for Gated Static Single Assignment},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {331-330},
doi = {10.1145/3573105.3575681},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "Encoding Dependently-Typed ..."
Encoding Dependently-Typed Constructions into Simple Type Theory
Anthony Bordg and Adrián Doña Mateo
(University of Cambridge, UK; University of Edinburgh, UK)
@InProceedings{CPP23p155,
author = {Anthony Bordg and Adrián Doña Mateo},
title = {Encoding Dependently-Typed Constructions into Simple Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {155-154},
doi = {10.1145/3573105.3575679},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub
(Inria, France; École Polytechnique, France; Meta, France)
@InProceedings{CPP23p67,
author = {Xavier Allamigeon and Quentin Canu and Pierre-Yves Strub},
title = {A Formal Disproof of Hirsch Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {67-66},
doi = {10.1145/3573105.3575678},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "A Formalized Reduction of ..."
A Formalized Reduction of Keller’s Conjecture
Joshua Clune
(Carnegie Mellon University, USA)
@InProceedings{CPP23p177,
author = {Joshua Clune},
title = {A Formalized Reduction of Keller’s Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {177-176},
doi = {10.1145/3573105.3575669},
year = {2023},
}
Publisher's Version
CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt, Cyril Cohen, and Ayumu Saito
(AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan)
@InProceedings{CPP23p45,
author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {45-44},
doi = {10.1145/3573105.3575691},
year = {2023},
}
Publisher's Version
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP23p111,
author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen},
title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {111-110},
doi = {10.1145/3573105.3575682},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "Compiling Higher-Order Specifications ..."
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
@InProceedings{CPP23p199,
author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi},
title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3573105.3575674},
year = {2023},
}
Publisher's Version
CPP '23: "Formalized Class Group Computations ..."
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands)
@InProceedings{CPP23p111,
author = {Anne Baanen and Alex J. Best and Nirvana Coppola and Sander R. Dahmen},
title = {Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {111-110},
doi = {10.1145/3573105.3575682},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalization of Doob’s ..."
A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying and Rémy Degenne
(University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198-CRIStAL, France)
@InProceedings{CPP23p573,
author = {Kexing Ying and Rémy Degenne},
title = {A Formalization of Doob’s Martingale Convergence Theorems in mathlib},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {573-572},
doi = {10.1145/3573105.3575675},
year = {2023},
}
Publisher's Version
CPP '23: "ASN1*: Provably Correct, Non-malleable ..."
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
@InProceedings{CPP23p485,
author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy},
title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {485-484},
doi = {10.1145/3573105.3575684},
year = {2023},
}
Publisher's Version
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz, Delphine Demange, and Sandrine Blazy
(Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP23p331,
author = {Yann Herklotz and Delphine Demange and Sandrine Blazy},
title = {Mechanised Semantics for Gated Static Single Assignment},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {331-330},
doi = {10.1145/3573105.3575681},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "Encoding Dependently-Typed ..."
Encoding Dependently-Typed Constructions into Simple Type Theory
Anthony Bordg and Adrián Doña Mateo
(University of Cambridge, UK; University of Edinburgh, UK)
@InProceedings{CPP23p155,
author = {Anthony Bordg and Adrián Doña Mateo},
title = {Encoding Dependently-Typed Constructions into Simple Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {155-154},
doi = {10.1145/3573105.3575679},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
(University of Cambridge, UK)
@InProceedings{CPP23p397,
author = {Angeliki Koutsoukou-Argyraki and Mantas Bakšys and Chelsea Edmonds},
title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3573105.3575680},
year = {2023},
}
Publisher's Version
CPP '23: "Terms for Efficient Proof ..."
Terms for Efficient Proof Checking and Parsing
Michael Färber
(University of Innsbruck, Austria)
@InProceedings{CPP23p243,
author = {Michael Färber},
title = {Terms for Efficient Proof Checking and Parsing},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {243-242},
doi = {10.1145/3573105.3575686},
year = {2023},
}
Publisher's Version
CPP '23: "Formalizing and Computing ..."
Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool
(Université Paris Cité, France)
@InProceedings{CPP23p265,
author = {Hugo Férée and Sam van Gool},
title = {Formalizing and Computing Propositional Quantifiers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {265-264},
doi = {10.1145/3573105.3575668},
year = {2023},
}
Publisher's Version
CPP '23: "A Computational Cantor-Bernstein ..."
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster, Felix Jahn, and Gert Smolka
(Inria, France; Saarland University, Germany)
@InProceedings{CPP23p287,
author = {Yannick Forster and Felix Jahn and Gert Smolka},
title = {A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {287-286},
doi = {10.1145/3573105.3575690},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "ASN1*: Provably Correct, Non-malleable ..."
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
@InProceedings{CPP23p485,
author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy},
title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {485-484},
doi = {10.1145/3573105.3575684},
year = {2023},
}
Publisher's Version
CPP '23: "Aesop: White-Box Best-First ..."
Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg and Asta Halkjær From
(Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark)
@InProceedings{CPP23p441,
author = {Jannis Limperg and Asta Halkjær From},
title = {Aesop: White-Box Best-First Proof Search for Lean},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {441-440},
doi = {10.1145/3573105.3575671},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi
Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi
(Université Côte d’Azur, France; Inria, France)
@InProceedings{CPP23p309,
author = {Benjamin Grégoire and Jean-Christophe Léchenet and Enrico Tassi},
title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3573105.3575683},
year = {2023},
}
Publisher's Version
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb, Ian J. Hayes, and Mark Utting
(University of Queensland, Australia)
@InProceedings{CPP23p551,
author = {Brae J. Webb and Ian J. Hayes and Mark Utting},
title = {Verifying Term Graph Optimizations using Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {551-550},
doi = {10.1145/3573105.3575673},
year = {2023},
}
Publisher's Version
CPP '23: "Mechanised Semantics for Gated ..."
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz, Delphine Demange, and Sandrine Blazy
(Imperial College London, UK; University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
@InProceedings{CPP23p331,
author = {Yann Herklotz and Delphine Demange and Sandrine Blazy},
title = {Mechanised Semantics for Gated Static Single Assignment},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {331-330},
doi = {10.1145/3573105.3575681},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "A Computational Cantor-Bernstein ..."
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster, Felix Jahn, and Gert Smolka
(Inria, France; Saarland University, Germany)
@InProceedings{CPP23p287,
author = {Yannick Forster and Felix Jahn and Gert Smolka},
title = {A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {287-286},
doi = {10.1145/3573105.3575690},
year = {2023},
}
Publisher's Version
CPP '23: "Improved Assistance for Interactive ..."
Improved Assistance for Interactive Proof (Keynote)
Cezary Kaliszyk
(University of Innsbruck, Austria)
@InProceedings{CPP23p23,
author = {Cezary Kaliszyk},
title = {Improved Assistance for Interactive Proof (Keynote)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {23-22},
doi = {10.1145/3573105.3579108},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalization of the Development ..."
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl and Aart Middeldorp
(University of Innsbruck, Austria)
@InProceedings{CPP23p353,
author = {Christina Kohl and Aart Middeldorp},
title = {A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {353-352},
doi = {10.1145/3573105.3575667},
year = {2023},
}
Publisher's Version
CPP '23: "Compiling Higher-Order Specifications ..."
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
@InProceedings{CPP23p199,
author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi},
title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3573105.3575674},
year = {2023},
}
Publisher's Version
CPP '23: "Compiling Higher-Order Specifications ..."
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, and Luca Arnaboldi
(Heriot-Watt University, UK; University of Strathclyde, UK; University of Edinburgh, UK)
@InProceedings{CPP23p199,
author = {Matthew L. Daggitt and Robert Atkey and Wen Kokke and Ekaterina Komendantskaya and Luca Arnaboldi},
title = {Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {199-198},
doi = {10.1145/3573105.3575674},
year = {2023},
}
Publisher's Version
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, and André Platzer
(Carnegie Mellon University, USA; KIT, Germany)
@InProceedings{CPP23p375,
author = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {375-374},
doi = {10.1145/3573105.3575672},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalisation of the Balog–Szemerédi–Gowers ..."
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds
(University of Cambridge, UK)
@InProceedings{CPP23p397,
author = {Angeliki Koutsoukou-Argyraki and Mantas Bakšys and Chelsea Edmonds},
title = {A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {397-396},
doi = {10.1145/3573105.3575680},
year = {2023},
}
Publisher's Version
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg
(University of Paris-Saclay, France; ENS Paris-Saclay, France; Stockholm University, Sweden)
@InProceedings{CPP23p419,
author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg},
title = {Computing Cohomology Rings in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {419-418},
doi = {10.1145/3573105.3575677},
year = {2023},
}
Publisher's Version
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi
Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi
(Université Côte d’Azur, France; Inria, France)
@InProceedings{CPP23p309,
author = {Benjamin Grégoire and Jean-Christophe Léchenet and Enrico Tassi},
title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3573105.3575683},
year = {2023},
}
Publisher's Version
CPP '23: "Aesop: White-Box Best-First ..."
Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg and Asta Halkjær From
(Vrije Universiteit Amsterdam, Netherlands; DTU, Denmark)
@InProceedings{CPP23p441,
author = {Jannis Limperg and Asta Halkjær From},
title = {Aesop: White-Box Best-First Proof Search for Lean},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {441-440},
doi = {10.1145/3573105.3575671},
year = {2023},
}
Publisher's Version
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg
(University of Paris-Saclay, France; ENS Paris-Saclay, France; Stockholm University, Sweden)
@InProceedings{CPP23p419,
author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg},
title = {Computing Cohomology Rings in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {419-418},
doi = {10.1145/3573105.3575677},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising the h-Principle ..."
Formalising the h-Principle and Sphere Eversion
Floris van Doorn, Patrick Massot, and Oliver Nash
(University of Paris-Saclay, France; CNRS, France; Imperial College London, UK)
@InProceedings{CPP23p221,
author = {Floris van Doorn and Patrick Massot and Oliver Nash},
title = {Formalising the h-Principle and Sphere Eversion},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {221-220},
doi = {10.1145/3573105.3575688},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "Formalising Sharkovsky’s ..."
Formalising Sharkovsky’s Theorem (Proof Pearl)
Bhavik Mehta
(University of Cambridge, UK)
@InProceedings{CPP23p463,
author = {Bhavik Mehta},
title = {Formalising Sharkovsky’s Theorem (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {463-462},
doi = {10.1145/3573105.3575689},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalization of the Development ..."
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl and Aart Middeldorp
(University of Innsbruck, Austria)
@InProceedings{CPP23p353,
author = {Christina Kohl and Aart Middeldorp},
title = {A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {353-352},
doi = {10.1145/3573105.3575667},
year = {2023},
}
Publisher's Version
CPP '23: "Computing Cohomology Rings ..."
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux, Axel Ljungström, and Anders Mörtberg
(University of Paris-Saclay, France; ENS Paris-Saclay, France; Stockholm University, Sweden)
@InProceedings{CPP23p419,
author = {Thomas Lamiaux and Axel Ljungström and Anders Mörtberg},
title = {Computing Cohomology Rings in Cubical Agda},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {419-418},
doi = {10.1145/3573105.3575677},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising the h-Principle ..."
Formalising the h-Principle and Sphere Eversion
Floris van Doorn, Patrick Massot, and Oliver Nash
(University of Paris-Saclay, France; CNRS, France; Imperial College London, UK)
@InProceedings{CPP23p221,
author = {Floris van Doorn and Patrick Massot and Oliver Nash},
title = {Formalising the h-Principle and Sphere Eversion},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {221-220},
doi = {10.1145/3573105.3575688},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "ASN1*: Provably Correct, Non-malleable ..."
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
@InProceedings{CPP23p485,
author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy},
title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {485-484},
doi = {10.1145/3573105.3575684},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP23p507,
author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters},
title = {Formalising Decentralised Exchanges in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {507-506},
doi = {10.1145/3573105.3575685},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, and André Platzer
(Carnegie Mellon University, USA; KIT, Germany)
@InProceedings{CPP23p375,
author = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {375-374},
doi = {10.1145/3573105.3575672},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "ASN1*: Provably Correct, Non-malleable ..."
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
@InProceedings{CPP23p485,
author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy},
title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {485-484},
doi = {10.1145/3573105.3575684},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "Semantics of Probabilistic ..."
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Reynald Affeldt, Cyril Cohen, and Ayumu Saito
(AIST, Japan; Inria, France; Tokyo Institute of Technology, Japan)
@InProceedings{CPP23p45,
author = {Reynald Affeldt and Cyril Cohen and Ayumu Saito},
title = {Semantics of Probabilistic Programs using s-Finite Kernels in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {45-44},
doi = {10.1145/3573105.3575691},
year = {2023},
}
Publisher's Version
CPP '23: "P4Cub: A Little Language for ..."
P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster
(Cornell University, USA; Microsoft, USA)
@InProceedings{CPP23p529,
author = {Rudy Peterson and Eric Hayden Campbell and John Chen and Natalie Isak and Calvin Shyu and Ryan Doenges and Parisa Ataei and Nate Foster},
title = {P4Cub: A Little Language for Big Routers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {529-528},
doi = {10.1145/3573105.3575670},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "A Computational Cantor-Bernstein ..."
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Yannick Forster, Felix Jahn, and Gert Smolka
(Inria, France; Saarland University, Germany)
@InProceedings{CPP23p287,
author = {Yannick Forster and Felix Jahn and Gert Smolka},
title = {A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {287-286},
doi = {10.1145/3573105.3575690},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising Decentralised ..."
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters
(Aarhus University, Denmark)
@InProceedings{CPP23p507,
author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters},
title = {Formalising Decentralised Exchanges in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {507-506},
doi = {10.1145/3573105.3575685},
year = {2023},
}
Publisher's Version
CPP '23: "A Formal Disproof of Hirsch ..."
A Formal Disproof of Hirsch Conjecture
Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub
(Inria, France; École Polytechnique, France; Meta, France)
@InProceedings{CPP23p67,
author = {Xavier Allamigeon and Quentin Canu and Pierre-Yves Strub},
title = {A Formal Disproof of Hirsch Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {67-66},
doi = {10.1145/3573105.3575678},
year = {2023},
}
Publisher's Version
CPP '23: "ASN1*: Provably Correct, Non-malleable ..."
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, and Nikhil Swamy
(Cornell University, USA; Microsoft Research, UK; Microsoft Research, USA)
@InProceedings{CPP23p485,
author = {Haobin Ni and Antoine Delignat-Lavaud and Cédric Fournet and Tahina Ramananandro and Nikhil Swamy},
title = {ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {485-484},
doi = {10.1145/3573105.3575684},
year = {2023},
}
Publisher's Version
CPP '23: "FastVer2: A Provably Correct ..."
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, and Ravi Ramamurthy
(Microsoft Research, USA; Microsoft Research, India; Inria, France; University of Maryland, USA; Carnegie Mellon University, USA)
@InProceedings{CPP23p89,
author = {Arvind Arasu and Tahina Ramananandro and Aseem Rastogi and Nikhil Swamy and Aymeric Fromherz and Kesha Hietala and Bryan Parno and Ravi Ramamurthy},
title = {FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {89-88},
doi = {10.1145/3573105.3575687},
year = {2023},
}
Publisher's Version
CPP '23: "A First Complete Algorithm ..."
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, and André Platzer
(Carnegie Mellon University, USA; KIT, Germany)
@InProceedings{CPP23p375,
author = {Katherine Kosaian and Yong Kiam Tan and André Platzer},
title = {A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {375-374},
doi = {10.1145/3573105.3575672},
year = {2023},
}
Publisher's Version
CPP '23: "Practical and Sound Equality ..."
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi
Benjamin Grégoire, Jean-Christophe Léchenet, and Enrico Tassi
(Université Côte d’Azur, France; Inria, France)
@InProceedings{CPP23p309,
author = {Benjamin Grégoire and Jean-Christophe Léchenet and Enrico Tassi},
title = {Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {309-308},
doi = {10.1145/3573105.3575683},
year = {2023},
}
Publisher's Version
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb, Ian J. Hayes, and Mark Utting
(University of Queensland, Australia)
@InProceedings{CPP23p551,
author = {Brae J. Webb and Ian J. Hayes and Mark Utting},
title = {Verifying Term Graph Optimizations using Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {551-550},
doi = {10.1145/3573105.3575673},
year = {2023},
}
Publisher's Version
CPP '23: "Formalising the h-Principle ..."
Formalising the h-Principle and Sphere Eversion
Floris van Doorn, Patrick Massot, and Oliver Nash
(University of Paris-Saclay, France; CNRS, France; Imperial College London, UK)
@InProceedings{CPP23p221,
author = {Floris van Doorn and Patrick Massot and Oliver Nash},
title = {Formalising the h-Principle and Sphere Eversion},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {221-220},
doi = {10.1145/3573105.3575688},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
CPP '23: "Formalizing and Computing ..."
Formalizing and Computing Propositional Quantifiers
Hugo Férée and Sam van Gool
(Université Paris Cité, France)
@InProceedings{CPP23p265,
author = {Hugo Férée and Sam van Gool},
title = {Formalizing and Computing Propositional Quantifiers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {265-264},
doi = {10.1145/3573105.3575668},
year = {2023},
}
Publisher's Version
CPP '23: "Compositional Pre-processing ..."
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
(LMF, France; Inria, France; University of Paris-Saclay, France; Mitsubishi, France; Nantes Université, France; École Centrale Nantes, France; CNRS, France; LS2N, France; UMR 6004, France)
@InProceedings{CPP23p133,
author = {Valentin Blot and Denis Cousineau and Enzo Crance and Louise Dubois de Prisque and Chantal Keller and Assia Mahboubi and Pierre Vial},
title = {Compositional Pre-processing for Automated Reasoning in Dependent Type Theory},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {133-132},
doi = {10.1145/3573105.3575676},
year = {2023},
}
Publisher's Version
CPP '23: "Verifying Term Graph Optimizations ..."
Verifying Term Graph Optimizations using Isabelle/HOL
Brae J. Webb, Ian J. Hayes, and Mark Utting
(University of Queensland, Australia)
@InProceedings{CPP23p551,
author = {Brae J. Webb and Ian J. Hayes and Mark Utting},
title = {Verifying Term Graph Optimizations using Isabelle/HOL},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {551-550},
doi = {10.1145/3573105.3575673},
year = {2023},
}
Publisher's Version
CPP '23: "A Formalization of Doob’s ..."
A Formalization of Doob’s Martingale Convergence Theorems in mathlib
Kexing Ying and Rémy Degenne
(University of Cambridge, UK; University of Lille, France; Inria, France; CNRS, France; Centrale Lille, France; UMR 9198-CRIStAL, France)
@InProceedings{CPP23p573,
author = {Kexing Ying and Rémy Degenne},
title = {A Formalization of Doob’s Martingale Convergence Theorems in mathlib},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {573-572},
doi = {10.1145/3573105.3575675},
year = {2023},
}
Publisher's Version