| |
Adjedj, Arthur
|
CPP '24: "Martin-Löf à la Coq ..."
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
@InProceedings{CPP24p290,
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
title = {Martin-Löf à la Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {290-289},
doi = {10.1145/3636501.3636951},
year = {2024},
}
 Publisher's Version
 Published Artifact
Artifacts Available
Article: poplws24cppmain-p36-p (type: Full Paper) doi:10.1145/3636501.3636951
|
| |
Ahrens, Benedikt |
CPP '24: "Univalent Double Categories ..."
Univalent Double Categories
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North
(Radboud University Nijmegen, Netherlands; Max Planck Institute for Mathematics, Germany; Delft University of Technology, Netherlands; University of Birmingham, UK; Utrecht University, Netherlands)
@InProceedings{CPP24p307,
author = {Niels van der Weide and Nima Rasekh and Benedikt Ahrens and Paige Randall North},
title = {Univalent Double Categories},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3636501.3636955},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p43-p (type: Full Paper) doi:10.1145/3636501.3636955
CPP '24: "Displayed Monoidal Categories ..."
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert
(Delft University of Technology, Netherlands; University of Birmingham, UK; IRIT - Université de Toulouse - CNRS - Toulouse INP - UT3, France; Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p324,
author = {Benedikt Ahrens and Ralph Matthes and Niels van der Weide and Kobe Wullaert},
title = {Displayed Monoidal Categories for the Semantics of Linear Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {324-323},
doi = {10.1145/3636501.3636956},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p44-p (type: Full Paper) doi:10.1145/3636501.3636956
|
| |
Ang, Zhendong |
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(National University of Singapore, Singapore)
@InProceedings{CPP24p69,
author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {69-68},
doi = {10.1145/3636501.3636944},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p16-p (type: Full Paper) doi:10.1145/3636501.3636944
|
| |
Appel, Andrew W. |
CPP '24: "VCFloat2: Floating-Point Error ..."
VCFloat2: Floating-Point Error Analysis in Coq
Andrew W. Appel and Ariel E. Kellison
(Princeton University, USA; Cornell University, USA)
@InProceedings{CPP24p35,
author = {Andrew W. Appel and Ariel E. Kellison},
title = {VCFloat2: Floating-Point Error Analysis in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {35-34},
doi = {10.1145/3636501.3636953},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p38-p (type: Full Paper) doi:10.1145/3636501.3636953
|
| |
Beringer, Lennart
|
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang
(University of Illinois at Chicago, USA; Princeton University, USA)
@InProceedings{CPP24p86,
author = {Duc-Than Nguyen and Lennart Beringer and William Mansky and Shengyi Wang},
title = {Compositional Verification of Concurrent C Programs with Search Structure Templates},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {86-85},
doi = {10.1145/3636501.3636940},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p2-p (type: Full Paper) doi:10.1145/3636501.3636940
|
| |
Besson, Frédéric |
CPP '24: "PfComp: A Verified Compiler ..."
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon, Frédéric Besson, and Tristan Ninet
(Inria - University of Rennes, France; Thales, France)
@InProceedings{CPP24p120,
author = {Clément Chavanon and Frédéric Besson and Tristan Ninet},
title = {PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {120-119},
doi = {10.1145/3636501.3636954},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p40-p (type: Full Paper) doi:10.1145/3636501.3636954
|
| |
Casals Buñuel, Joaquim
|
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
Chavanon, Clément |
CPP '24: "PfComp: A Verified Compiler ..."
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon, Frédéric Besson, and Tristan Ninet
(Inria - University of Rennes, France; Thales, France)
@InProceedings{CPP24p120,
author = {Clément Chavanon and Frédéric Besson and Tristan Ninet},
title = {PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {120-119},
doi = {10.1145/3636501.3636954},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p40-p (type: Full Paper) doi:10.1145/3636501.3636954
|
| |
Conejero Rodríguez, Juan |
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
De Almeida Borges, Ana
|
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
De Frutos-Fernández, María Inés |
CPP '24: "A Formalization of Complete ..."
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de Frutos-Fernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
(Autonomous University of Madrid, Spain; Université Jean Monnet Saint-Étienne, France)
@InProceedings{CPP24p239,
author = {María Inés de Frutos-Fernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio},
title = {A Formalization of Complete Discrete Valuation Rings and Local Fields},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {239-238},
doi = {10.1145/3636501.3636942},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p13-p (type: Full Paper) doi:10.1145/3636501.3636942
|
| |
Ebner, Gabriel
|
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)
@InProceedings{CPP24p154,
author = {Ekaterina Zhuchko and Margus Veanes and Gabriel Ebner},
title = {Lean Formalization of Extended Regular Expression Matching with Lookarounds},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154-153},
doi = {10.1145/3636501.3636959},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p61-p (type: Full Paper) doi:10.1145/3636501.3636959
|
| |
Edmonds, Chelsea |
CPP '24: "Formal Probabilistic Methods ..."
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Chelsea Edmonds and Lawrence C. Paulson
(University of Sheffield, UK; University of Cambridge, UK)
@InProceedings{CPP24p171,
author = {Chelsea Edmonds and Lawrence C. Paulson},
title = {Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {171-170},
doi = {10.1145/3636501.3636946},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p21-p (type: Full Paper) doi:10.1145/3636501.3636946
|
| |
Eremondi, Joseph |
CPP '24: "Strictly Monotone Brouwer ..."
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Joseph Eremondi
(University of Edinburgh, UK)
@InProceedings{CPP24p256,
author = {Joseph Eremondi},
title = {Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {256-255},
doi = {10.1145/3636501.3636948},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p26-p (type: Full Paper) doi:10.1145/3636501.3636948
|
| |
Gadgil, Siddhartha
|
CPP '24: "Formalizing Giles Gardam’s ..."
Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
Siddhartha Gadgil and Anand Rao Tadipatri
(Indian Institute of Science, India; Indian Institute of Science Education and Research, India)
@InProceedings{CPP24p222,
author = {Siddhartha Gadgil and Anand Rao Tadipatri},
title = {Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {222-221},
doi = {10.1145/3636501.3636947},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p23-p (type: Full Paper) doi:10.1145/3636501.3636947
|
| |
González Bedmar, Mireia |
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
Hansen, Lasse Letager
|
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Haselwarter, Philipp G. |
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Hermo Reyes, Eduardo |
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
Hirokawa, Nao |
CPP '24: "Certification of Confluence- ..."
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann
(JAIST, Japan; University of Innsbruck, Austria)
@InProceedings{CPP24p188,
author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188-187},
doi = {10.1145/3636501.3636949},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p32-p (type: Full Paper) doi:10.1145/3636501.3636949
|
| |
Hriţcu, Cătălin |
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Hvass, Benjamin Salling |
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Joosten, Joost J.
|
CPP '24: "UTC Time, Formally Verified ..."
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, and Joost J. Joosten
(University of Barcelona, Spain; Formal Vindications, Spain)
@InProceedings{CPP24p18,
author = {Ana de Almeida Borges and Mireia González Bedmar and Juan Conejero Rodríguez and Eduardo Hermo Reyes and Joaquim Casals Buñuel and Joost J. Joosten},
title = {UTC Time, Formally Verified},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {18-17},
doi = {10.1145/3636501.3636958},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p47-p (type: Full Paper) doi:10.1145/3636501.3636958
|
| |
Kellison, Ariel E.
|
CPP '24: "VCFloat2: Floating-Point Error ..."
VCFloat2: Floating-Point Error Analysis in Coq
Andrew W. Appel and Ariel E. Kellison
(Princeton University, USA; Cornell University, USA)
@InProceedings{CPP24p35,
author = {Andrew W. Appel and Ariel E. Kellison},
title = {VCFloat2: Floating-Point Error Analysis in Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {35-34},
doi = {10.1145/3636501.3636953},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p38-p (type: Full Paper) doi:10.1145/3636501.3636953
|
| |
Kim, Dohan |
CPP '24: "Certification of Confluence- ..."
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann
(JAIST, Japan; University of Innsbruck, Austria)
@InProceedings{CPP24p188,
author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188-187},
doi = {10.1145/3636501.3636949},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p32-p (type: Full Paper) doi:10.1145/3636501.3636949
|
| |
Kirst, Dominik |
CPP '24: "A Mechanised and Constructive ..."
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Ian Shillito and Dominik Kirst
(Australian National University, Australia; Ben-Gurion University of the Negev, Israel)
@InProceedings{CPP24p273,
author = {Ian Shillito and Dominik Kirst},
title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {273-272},
doi = {10.1145/3636501.3636957},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p45-p (type: Full Paper) doi:10.1145/3636501.3636957
|
| |
Krebbers, Robbert |
CPP '24: "Unification for Subformula ..."
Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p103,
author = {Ike Mulder and Robbert Krebbers},
title = {Unification for Subformula Linking under Quantifiers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {103-102},
doi = {10.1145/3636501.3636950},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p34-p (type: Full Paper) doi:10.1145/3636501.3636950
|
| |
Kudasov, Nikolai |
CPP '24: "Formalizing the ∞-Categorical ..."
Formalizing the ∞-Categorical Yoneda Lemma
Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger
(Innopolis University, Russia; Johns Hopkins University, USA)
@InProceedings{CPP24p341,
author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger},
title = {Formalizing the ∞-Categorical Yoneda Lemma},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {341-340},
doi = {10.1145/3636501.3636945},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p18-p (type: Full Paper) doi:10.1145/3636501.3636945
|
| |
Lennon-Bertrand, Meven
|
CPP '24: "Martin-Löf à la Coq ..."
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
@InProceedings{CPP24p290,
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
title = {Martin-Löf à la Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {290-289},
doi = {10.1145/3636501.3636951},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p36-p (type: Full Paper) doi:10.1145/3636501.3636951
|
| |
Maillard, Kenji
|
CPP '24: "Martin-Löf à la Coq ..."
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
@InProceedings{CPP24p290,
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
title = {Martin-Löf à la Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {290-289},
doi = {10.1145/3636501.3636951},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p36-p (type: Full Paper) doi:10.1145/3636501.3636951
|
| |
Mansky, William |
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang
(University of Illinois at Chicago, USA; Princeton University, USA)
@InProceedings{CPP24p86,
author = {Duc-Than Nguyen and Lennart Beringer and William Mansky and Shengyi Wang},
title = {Compositional Verification of Concurrent C Programs with Search Structure Templates},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {86-85},
doi = {10.1145/3636501.3636940},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p2-p (type: Full Paper) doi:10.1145/3636501.3636940
|
| |
Mathur, Umang |
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(National University of Singapore, Singapore)
@InProceedings{CPP24p69,
author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {69-68},
doi = {10.1145/3636501.3636944},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p16-p (type: Full Paper) doi:10.1145/3636501.3636944
|
| |
Matthes, Ralph |
CPP '24: "Displayed Monoidal Categories ..."
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert
(Delft University of Technology, Netherlands; University of Birmingham, UK; IRIT - Université de Toulouse - CNRS - Toulouse INP - UT3, France; Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p324,
author = {Benedikt Ahrens and Ralph Matthes and Niels van der Weide and Kobe Wullaert},
title = {Displayed Monoidal Categories for the Semantics of Linear Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {324-323},
doi = {10.1145/3636501.3636956},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p44-p (type: Full Paper) doi:10.1145/3636501.3636956
|
| |
Monniaux, David |
CPP '24: "Memory Simulations, Security ..."
Memory Simulations, Security and Optimization in a Verified Compiler
David Monniaux
(University of Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France)
@InProceedings{CPP24p137,
author = {David Monniaux},
title = {Memory Simulations, Security and Optimization in a Verified Compiler},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {137-136},
doi = {10.1145/3636501.3636952},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p37-p (type: Full Paper) doi:10.1145/3636501.3636952
|
| |
Mulder, Ike |
CPP '24: "Unification for Subformula ..."
Unification for Subformula Linking under Quantifiers
Ike Mulder and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p103,
author = {Ike Mulder and Robbert Krebbers},
title = {Unification for Subformula Linking under Quantifiers},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {103-102},
doi = {10.1145/3636501.3636950},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p34-p (type: Full Paper) doi:10.1145/3636501.3636950
|
| |
Muñoz, César |
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz
(NASA, USA; AMA, USA)
@InProceedings{CPP24p205,
author = {Lauren White and Laura Titolo and J. Tanner Slagel and César Muñoz},
title = {A Temporal Differential Dynamic Logic Formal Embedding},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {205-204},
doi = {10.1145/3636501.3636943},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p14-p (type: Full Paper) doi:10.1145/3636501.3636943
|
| |
Nguyen, Duc-Than
|
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang
(University of Illinois at Chicago, USA; Princeton University, USA)
@InProceedings{CPP24p86,
author = {Duc-Than Nguyen and Lennart Beringer and William Mansky and Shengyi Wang},
title = {Compositional Verification of Concurrent C Programs with Search Structure Templates},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {86-85},
doi = {10.1145/3636501.3636940},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p2-p (type: Full Paper) doi:10.1145/3636501.3636940
|
| |
Ninet, Tristan |
CPP '24: "PfComp: A Verified Compiler ..."
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Clément Chavanon, Frédéric Besson, and Tristan Ninet
(Inria - University of Rennes, France; Thales, France)
@InProceedings{CPP24p120,
author = {Clément Chavanon and Frédéric Besson and Tristan Ninet},
title = {PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {120-119},
doi = {10.1145/3636501.3636954},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p40-p (type: Full Paper) doi:10.1145/3636501.3636954
|
| |
North, Paige Randall |
CPP '24: "Univalent Double Categories ..."
Univalent Double Categories
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North
(Radboud University Nijmegen, Netherlands; Max Planck Institute for Mathematics, Germany; Delft University of Technology, Netherlands; University of Birmingham, UK; Utrecht University, Netherlands)
@InProceedings{CPP24p307,
author = {Niels van der Weide and Nima Rasekh and Benedikt Ahrens and Paige Randall North},
title = {Univalent Double Categories},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3636501.3636955},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p43-p (type: Full Paper) doi:10.1145/3636501.3636955
|
| |
Nuccio Mortarino Majno di Capriglio, Filippo Alberto Edoardo |
CPP '24: "A Formalization of Complete ..."
A Formalization of Complete Discrete Valuation Rings and Local Fields
María Inés de Frutos-Fernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
(Autonomous University of Madrid, Spain; Université Jean Monnet Saint-Étienne, France)
@InProceedings{CPP24p239,
author = {María Inés de Frutos-Fernández and Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio},
title = {A Formalization of Complete Discrete Valuation Rings and Local Fields},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {239-238},
doi = {10.1145/3636501.3636942},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p13-p (type: Full Paper) doi:10.1145/3636501.3636942
|
| |
Paulson, Lawrence C.
|
CPP '24: "Formal Probabilistic Methods ..."
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
Chelsea Edmonds and Lawrence C. Paulson
(University of Sheffield, UK; University of Cambridge, UK)
@InProceedings{CPP24p171,
author = {Chelsea Edmonds and Lawrence C. Paulson},
title = {Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {171-170},
doi = {10.1145/3636501.3636946},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p21-p (type: Full Paper) doi:10.1145/3636501.3636946
|
| |
Pédrot, Pierre-Marie |
CPP '24: "Martin-Löf à la Coq ..."
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
@InProceedings{CPP24p290,
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
title = {Martin-Löf à la Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {290-289},
doi = {10.1145/3636501.3636951},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p36-p (type: Full Paper) doi:10.1145/3636501.3636951
|
| |
Pîrlea, George |
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(National University of Singapore, Singapore)
@InProceedings{CPP24p69,
author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {69-68},
doi = {10.1145/3636501.3636944},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p16-p (type: Full Paper) doi:10.1145/3636501.3636944
|
| |
Pujet, Loïc |
CPP '24: "Martin-Löf à la Coq ..."
Martin-Löf à la Coq
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet
(ENS Paris Saclay - Université Paris-Saclay, France; University of Cambridge, UK; Inria, France; Stockholm University, Sweden)
@InProceedings{CPP24p290,
author = {Arthur Adjedj and Meven Lennon-Bertrand and Kenji Maillard and Pierre-Marie Pédrot and Loïc Pujet},
title = {Martin-Löf à la Coq},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {290-289},
doi = {10.1145/3636501.3636951},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p36-p (type: Full Paper) doi:10.1145/3636501.3636951
|
| |
Raad, Azalea
|
CPP '24: "Under-Approximation for Scalable ..."
Under-Approximation for Scalable Bug Detection (Keynote)
Azalea Raad
(Imperial College London, UK)
@InProceedings{CPP24p1,
author = {Azalea Raad},
title = {Under-Approximation for Scalable Bug Detection (Keynote)},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {1-0},
doi = {10.1145/3636501.3637683},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-key1-p (type: Invited Talk Abstract) doi:10.1145/3636501.3637683
|
| |
Rasekh, Nima |
CPP '24: "Univalent Double Categories ..."
Univalent Double Categories
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North
(Radboud University Nijmegen, Netherlands; Max Planck Institute for Mathematics, Germany; Delft University of Technology, Netherlands; University of Birmingham, UK; Utrecht University, Netherlands)
@InProceedings{CPP24p307,
author = {Niels van der Weide and Nima Rasekh and Benedikt Ahrens and Paige Randall North},
title = {Univalent Double Categories},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3636501.3636955},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p43-p (type: Full Paper) doi:10.1145/3636501.3636955
|
| |
Riehl, Emily |
CPP '24: "Formalizing the ∞-Categorical ..."
Formalizing the ∞-Categorical Yoneda Lemma
Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger
(Innopolis University, Russia; Johns Hopkins University, USA)
@InProceedings{CPP24p341,
author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger},
title = {Formalizing the ∞-Categorical Yoneda Lemma},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {341-340},
doi = {10.1145/3636501.3636945},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p18-p (type: Full Paper) doi:10.1145/3636501.3636945
|
| |
Sergey, Ilya
|
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(National University of Singapore, Singapore)
@InProceedings{CPP24p69,
author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {69-68},
doi = {10.1145/3636501.3636944},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p16-p (type: Full Paper) doi:10.1145/3636501.3636944
|
| |
Shillito, Ian |
CPP '24: "A Mechanised and Constructive ..."
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic
Ian Shillito and Dominik Kirst
(Australian National University, Australia; Ben-Gurion University of the Negev, Israel)
@InProceedings{CPP24p273,
author = {Ian Shillito and Dominik Kirst},
title = {A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {273-272},
doi = {10.1145/3636501.3636957},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p45-p (type: Full Paper) doi:10.1145/3636501.3636957
|
| |
Shintani, Kiraku |
CPP '24: "Certification of Confluence- ..."
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann
(JAIST, Japan; University of Innsbruck, Austria)
@InProceedings{CPP24p188,
author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188-187},
doi = {10.1145/3636501.3636949},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p32-p (type: Full Paper) doi:10.1145/3636501.3636949
|
| |
Slagel, J. Tanner |
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz
(NASA, USA; AMA, USA)
@InProceedings{CPP24p205,
author = {Lauren White and Laura Titolo and J. Tanner Slagel and César Muñoz},
title = {A Temporal Differential Dynamic Logic Formal Embedding},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {205-204},
doi = {10.1145/3636501.3636943},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p14-p (type: Full Paper) doi:10.1145/3636501.3636943
|
| |
Spitters, Bas |
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Tadipatri, Anand Rao
|
CPP '24: "Formalizing Giles Gardam’s ..."
Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
Siddhartha Gadgil and Anand Rao Tadipatri
(Indian Institute of Science, India; Indian Institute of Science Education and Research, India)
@InProceedings{CPP24p222,
author = {Siddhartha Gadgil and Anand Rao Tadipatri},
title = {Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {222-221},
doi = {10.1145/3636501.3636947},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p23-p (type: Full Paper) doi:10.1145/3636501.3636947
|
| |
Thiemann, René |
CPP '24: "Certification of Confluence- ..."
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann
(JAIST, Japan; University of Innsbruck, Austria)
@InProceedings{CPP24p188,
author = {Nao Hirokawa and Dohan Kim and Kiraku Shintani and René Thiemann},
title = {Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {188-187},
doi = {10.1145/3636501.3636949},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p32-p (type: Full Paper) doi:10.1145/3636501.3636949
|
| |
Titolo, Laura |
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz
(NASA, USA; AMA, USA)
@InProceedings{CPP24p205,
author = {Lauren White and Laura Titolo and J. Tanner Slagel and César Muñoz},
title = {A Temporal Differential Dynamic Logic Formal Embedding},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {205-204},
doi = {10.1145/3636501.3636943},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p14-p (type: Full Paper) doi:10.1145/3636501.3636943
|
| |
Van der Weide, Niels
|
CPP '24: "Univalent Double Categories ..."
Univalent Double Categories
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North
(Radboud University Nijmegen, Netherlands; Max Planck Institute for Mathematics, Germany; Delft University of Technology, Netherlands; University of Birmingham, UK; Utrecht University, Netherlands)
@InProceedings{CPP24p307,
author = {Niels van der Weide and Nima Rasekh and Benedikt Ahrens and Paige Randall North},
title = {Univalent Double Categories},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {307-306},
doi = {10.1145/3636501.3636955},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p43-p (type: Full Paper) doi:10.1145/3636501.3636955
CPP '24: "Displayed Monoidal Categories ..."
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert
(Delft University of Technology, Netherlands; University of Birmingham, UK; IRIT - Université de Toulouse - CNRS - Toulouse INP - UT3, France; Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p324,
author = {Benedikt Ahrens and Ralph Matthes and Niels van der Weide and Kobe Wullaert},
title = {Displayed Monoidal Categories for the Semantics of Linear Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {324-323},
doi = {10.1145/3636501.3636956},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p44-p (type: Full Paper) doi:10.1145/3636501.3636956
|
| |
Veanes, Margus |
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)
@InProceedings{CPP24p154,
author = {Ekaterina Zhuchko and Margus Veanes and Gabriel Ebner},
title = {Lean Formalization of Extended Regular Expression Matching with Lookarounds},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154-153},
doi = {10.1145/3636501.3636959},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p61-p (type: Full Paper) doi:10.1145/3636501.3636959
|
| |
Wang, Shengyi
|
CPP '24: "Compositional Verification ..."
Compositional Verification of Concurrent C Programs with Search Structure Templates
Duc-Than Nguyen, Lennart Beringer, William Mansky, and Shengyi Wang
(University of Illinois at Chicago, USA; Princeton University, USA)
@InProceedings{CPP24p86,
author = {Duc-Than Nguyen and Lennart Beringer and William Mansky and Shengyi Wang},
title = {Compositional Verification of Concurrent C Programs with Search Structure Templates},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {86-85},
doi = {10.1145/3636501.3636940},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p2-p (type: Full Paper) doi:10.1145/3636501.3636940
|
| |
Weinberger, Jonathan |
CPP '24: "Formalizing the ∞-Categorical ..."
Formalizing the ∞-Categorical Yoneda Lemma
Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger
(Innopolis University, Russia; Johns Hopkins University, USA)
@InProceedings{CPP24p341,
author = {Nikolai Kudasov and Emily Riehl and Jonathan Weinberger},
title = {Formalizing the ∞-Categorical Yoneda Lemma},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {341-340},
doi = {10.1145/3636501.3636945},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p18-p (type: Full Paper) doi:10.1145/3636501.3636945
|
| |
White, Lauren |
CPP '24: "A Temporal Differential Dynamic ..."
A Temporal Differential Dynamic Logic Formal Embedding
Lauren White, Laura Titolo, J. Tanner Slagel, and César Muñoz
(NASA, USA; AMA, USA)
@InProceedings{CPP24p205,
author = {Lauren White and Laura Titolo and J. Tanner Slagel and César Muñoz},
title = {A Temporal Differential Dynamic Logic Formal Embedding},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {205-204},
doi = {10.1145/3636501.3636943},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p14-p (type: Full Paper) doi:10.1145/3636501.3636943
|
| |
Winterhalter, Théo |
CPP '24: "The Last Yard: Foundational ..."
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters
(Aarhus University, Denmark; Inria, France; MPI-SP, Germany)
@InProceedings{CPP24p52,
author = {Philipp G. Haselwarter and Benjamin Salling Hvass and Lasse Letager Hansen and Théo Winterhalter and Cătălin Hriţcu and Bas Spitters},
title = {The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {52-51},
doi = {10.1145/3636501.3636961},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p4-p (type: Full Paper) doi:10.1145/3636501.3636961
|
| |
Wullaert, Kobe |
CPP '24: "Displayed Monoidal Categories ..."
Displayed Monoidal Categories for the Semantics of Linear Logic
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert
(Delft University of Technology, Netherlands; University of Birmingham, UK; IRIT - Université de Toulouse - CNRS - Toulouse INP - UT3, France; Radboud University Nijmegen, Netherlands)
@InProceedings{CPP24p324,
author = {Benedikt Ahrens and Ralph Matthes and Niels van der Weide and Kobe Wullaert},
title = {Displayed Monoidal Categories for the Semantics of Linear Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {324-323},
doi = {10.1145/3636501.3636956},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p44-p (type: Full Paper) doi:10.1145/3636501.3636956
|
| |
Zhao, Qiyuan
|
CPP '24: "Rooting for Efficiency: Mechanised ..."
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey
(National University of Singapore, Singapore)
@InProceedings{CPP24p69,
author = {Qiyuan Zhao and George Pîrlea and Zhendong Ang and Umang Mathur and Ilya Sergey},
title = {Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {69-68},
doi = {10.1145/3636501.3636944},
year = {2024},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws24cppmain-p16-p (type: Full Paper) doi:10.1145/3636501.3636944
|
| |
Zhuchko, Ekaterina |
CPP '24: "Lean Formalization of Extended ..."
Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)
@InProceedings{CPP24p154,
author = {Ekaterina Zhuchko and Margus Veanes and Gabriel Ebner},
title = {Lean Formalization of Extended Regular Expression Matching with Lookarounds},
booktitle = {Proc.\ CPP},
publisher = {ACM},
pages = {154-153},
doi = {10.1145/3636501.3636959},
year = {2024},
}
Publisher's Version
Article: poplws24cppmain-p61-p (type: Full Paper) doi:10.1145/3636501.3636959
|