| |
Affeldt, Reynald
|
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
Article: poplws23cppmain-p61-p doi:10.1145/3573105.3575691
|
| |
Allamigeon, Xavier |
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
Article: poplws23cppmain-p29-p doi:10.1145/3573105.3575678
|
| |
Annenkov, Danil |
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
Article: poplws23cppmain-p40-p doi:10.1145/3573105.3575685
|
| |
Arasu, Arvind |
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Arnaboldi, Luca |
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
Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674
|
| |
Ataei, Parisa |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Atkey, Robert |
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
Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674
|
| |
Baanen, Anne
|
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
Article: poplws23cppmain-p36-p doi:10.1145/3573105.3575682
|
| |
Bakšys, Mantas |
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
Article: poplws23cppmain-p31-p doi:10.1145/3573105.3575680
|
| |
Best, Alex J. |
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
Article: poplws23cppmain-p36-p doi:10.1145/3573105.3575682
|
| |
Blazy, Sandrine |
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
Article: poplws23cppmain-key1-p doi:10.1145/3573105.3579107
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
Article: poplws23cppmain-p32-p doi:10.1145/3573105.3575681
|
| |
Blot, Valentin |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Bordg, Anthony |
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
Article: poplws23cppmain-p30-p doi:10.1145/3573105.3575679
|
| |
Campbell, Eric Hayden
|
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Canu, Quentin |
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
Article: poplws23cppmain-p29-p doi:10.1145/3573105.3575678
|
| |
Chen, John |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Clune, Joshua |
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
Article: poplws23cppmain-p10-p doi:10.1145/3573105.3575669
|
| |
Cohen, Cyril |
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
Article: poplws23cppmain-p61-p doi:10.1145/3573105.3575691
|
| |
Coppola, Nirvana |
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
Article: poplws23cppmain-p36-p doi:10.1145/3573105.3575682
|
| |
Cousineau, Denis |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Crance, Enzo |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Daggitt, Matthew L.
|
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
Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674
|
| |
Dahmen, Sander R. |
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
Article: poplws23cppmain-p36-p doi:10.1145/3573105.3575682
|
| |
Degenne, Rémy |
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
Article: poplws23cppmain-p22-p doi:10.1145/3573105.3575675
|
| |
Delignat-Lavaud, Antoine |
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
Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684
|
| |
Demange, Delphine |
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
Article: poplws23cppmain-p32-p doi:10.1145/3573105.3575681
|
| |
De Prisque, Louise Dubois |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Doenges, Ryan |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Doña Mateo, Adrián |
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
Article: poplws23cppmain-p30-p doi:10.1145/3573105.3575679
|
| |
Edmonds, Chelsea
|
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
Article: poplws23cppmain-p31-p doi:10.1145/3573105.3575680
|
| |
Färber, Michael
|
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
Article: poplws23cppmain-p44-p doi:10.1145/3573105.3575686
|
| |
Férée, Hugo |
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
Article: poplws23cppmain-p2-p doi:10.1145/3573105.3575668
|
| |
Forster, Yannick |
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
Article: poplws23cppmain-p58-p doi:10.1145/3573105.3575690
|
| |
Foster, Nate |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Fournet, Cédric |
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
Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684
|
| |
From, Asta Halkjær |
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
Article: poplws23cppmain-p18-p doi:10.1145/3573105.3575671
|
| |
Fromherz, Aymeric |
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Grégoire, Benjamin
|
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
Article: poplws23cppmain-p37-p doi:10.1145/3573105.3575683
|
| |
Hayes, Ian J.
|
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
Article: poplws23cppmain-p20-p doi:10.1145/3573105.3575673
|
| |
Herklotz, Yann |
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
Article: poplws23cppmain-p32-p doi:10.1145/3573105.3575681
|
| |
Hietala, Kesha |
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Isak, Natalie
|
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Jahn, Felix
|
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
Article: poplws23cppmain-p58-p doi:10.1145/3573105.3575690
|
| |
Kaliszyk, Cezary
|
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
Article: poplws23cppmain-key2-p doi:10.1145/3573105.3579108
|
| |
Keller, Chantal |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Kohl, Christina |
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
Article: poplws23cppmain-p1-p doi:10.1145/3573105.3575667
|
| |
Kokke, Wen |
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
Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674
|
| |
Komendantskaya, Ekaterina |
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
Article: poplws23cppmain-p21-p doi:10.1145/3573105.3575674
|
| |
Kosaian, Katherine |
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
Article: poplws23cppmain-p19-p doi:10.1145/3573105.3575672
|
| |
Koutsoukou-Argyraki, Angeliki |
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
Article: poplws23cppmain-p31-p doi:10.1145/3573105.3575680
|
| |
Lamiaux, Thomas
|
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
Article: poplws23cppmain-p27-p doi:10.1145/3573105.3575677
|
| |
Léchenet, Jean-Christophe |
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
Article: poplws23cppmain-p37-p doi:10.1145/3573105.3575683
|
| |
Limperg, Jannis |
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
Article: poplws23cppmain-p18-p doi:10.1145/3573105.3575671
|
| |
Ljungström, Axel |
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
Article: poplws23cppmain-p27-p doi:10.1145/3573105.3575677
|
| |
Mahboubi, Assia
|
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Massot, Patrick |
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
Article: poplws23cppmain-p53-p doi:10.1145/3573105.3575688
|
| |
Mehta, Bhavik |
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
Article: poplws23cppmain-p57-p doi:10.1145/3573105.3575689
|
| |
Middeldorp, Aart |
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
Article: poplws23cppmain-p1-p doi:10.1145/3573105.3575667
|
| |
Mörtberg, Anders |
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
Article: poplws23cppmain-p27-p doi:10.1145/3573105.3575677
|
| |
Nash, Oliver
|
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
Article: poplws23cppmain-p53-p doi:10.1145/3573105.3575688
|
| |
Ni, Haobin |
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
Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684
|
| |
Nielsen, Eske Hoy |
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
Article: poplws23cppmain-p40-p doi:10.1145/3573105.3575685
|
| |
Parno, Bryan
|
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Peterson, Rudy |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Platzer, André |
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
Article: poplws23cppmain-p19-p doi:10.1145/3573105.3575672
|
| |
Ramamurthy, Ravi
|
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Ramananandro, Tahina |
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
Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Rastogi, Aseem |
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Saito, Ayumu
|
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
Article: poplws23cppmain-p61-p doi:10.1145/3573105.3575691
|
| |
Shyu, Calvin |
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
Article: poplws23cppmain-p13-p doi:10.1145/3573105.3575670
|
| |
Smolka, Gert |
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
Article: poplws23cppmain-p58-p doi:10.1145/3573105.3575690
|
| |
Spitters, Bas |
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
Article: poplws23cppmain-p40-p doi:10.1145/3573105.3575685
|
| |
Strub, Pierre-Yves |
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
Article: poplws23cppmain-p29-p doi:10.1145/3573105.3575678
|
| |
Swamy, Nikhil |
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
Article: poplws23cppmain-p38-p doi:10.1145/3573105.3575684
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
Article: poplws23cppmain-p49-p doi:10.1145/3573105.3575687
|
| |
Tan, Yong Kiam
|
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
Article: poplws23cppmain-p19-p doi:10.1145/3573105.3575672
|
| |
Tassi, Enrico |
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
Article: poplws23cppmain-p37-p doi:10.1145/3573105.3575683
|
| |
Utting, Mark
|
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
Article: poplws23cppmain-p20-p doi:10.1145/3573105.3575673
|
| |
Van Doorn, Floris
|
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
Article: poplws23cppmain-p53-p doi:10.1145/3573105.3575688
|
| |
Van Gool, Sam |
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
Article: poplws23cppmain-p2-p doi:10.1145/3573105.3575668
|
| |
Vial, Pierre |
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
Article: poplws23cppmain-p24-p doi:10.1145/3573105.3575676
|
| |
Webb, Brae J.
|
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
Article: poplws23cppmain-p20-p doi:10.1145/3573105.3575673
|
| |
Ying, Kexing
|
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
Article: poplws23cppmain-p22-p doi:10.1145/3573105.3575675
|