|
Alexandru, Cass
|
CPP '25: "Intrinsically Correct Sorting ..."
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide
(RPTU Kaiserslautern-Landau, Germany; University of Bologna, Italy; Radboud University Nijmegen, Netherlands)
Article Search
|
|
Almeida, José Bacelar |
CPP '25: "Leakage-Free Probabilistic ..."
Leakage-Free Probabilistic Jasmin Programs
Denis Firsov, Tiago Oliveira, José Bacelar Almeida, and Dominique Unruh
(Tallinn University of Technology, Estonia; SandboxAQ, n.n.; HASLab, n.n.; INESC TEC, Portugal; University of Minho, Portugal; University of Tartu, Estonia)
Article Search
|
|
Almeida, Ricardo |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Baanen, Anne
|
CPP '25: "Certifying Rings of Integers ..."
Certifying Rings of Integers in Number Fields
Anne Baanen, Alain Chavarri Villarello, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands; Lean FRO, Netherlands)
Article Search
|
|
Birkedal, Lars |
CPP '25: "The Nextgen Modality: A Modality ..."
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Simon Friis Vindum, Aïna Linn Georges, and Lars Birkedal
(Aarhus University, Denmark; MPI-SWS, Germany)
Article Search
|
|
Boulmé, Sylvain |
CPP '25: "Formally Verified Hardening ..."
Formally Verified Hardening of C Programs against Hardware Fault Injection
Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet
(Ecole Nationale de l’Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; CNRS, France)
Article Search
|
|
Campbell, Brian
|
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Chappe, Nicolas |
CPP '25: "Monadic Interpreters for Concurrent ..."
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski
(Inria - LIP, France; CNRS, France; Inria, France)
Article Search
|
|
Chattopadhyay, Agnishom |
CPP '25: "Verified and Efficient Matching ..."
Verified and Efficient Matching of Regular Expressions with Lookaround
Agnishom Chattopadhyay, Angela W. Li, and Konstantinos Mamouras
(Rice University, USA)
Article Search
|
|
Chavarri Villarello, Alain |
CPP '25: "Certifying Rings of Integers ..."
Certifying Rings of Integers in Number Fields
Anne Baanen, Alain Chavarri Villarello, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands; Lean FRO, Netherlands)
Article Search
|
|
Cheney, James |
CPP '25: "Nominal Matching Logic with ..."
Nominal Matching Logic with Fixpoints
Mircea Sebe, Maribel Fernández, and James Cheney
(University of Illinois at Urbana-Champaign, USA; King’s College London, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Cheung, Louis |
CPP '25: "Formalized Burrows-Wheeler ..."
Formalized Burrows-Wheeler Transform
Louis Cheung, Alistair Moffat, and Christine Rizkallah
(University of Melbourne, Australia)
Article Search
|
|
Choudhury, Vikraman |
CPP '25: "Intrinsically Correct Sorting ..."
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide
(RPTU Kaiserslautern-Landau, Germany; University of Bologna, Italy; Radboud University Nijmegen, Netherlands)
Article Search
|
|
Dahmen, Sander R.
|
CPP '25: "Certifying Rings of Integers ..."
Certifying Rings of Integers in Number Fields
Anne Baanen, Alain Chavarri Villarello, and Sander R. Dahmen
(Vrije Universiteit Amsterdam, Netherlands; Lean FRO, Netherlands)
Article Search
|
|
Fernández, Maribel
|
CPP '25: "Nominal Matching Logic with ..."
Nominal Matching Logic with Fixpoints
Mircea Sebe, Maribel Fernández, and James Cheney
(University of Illinois at Urbana-Champaign, USA; King’s College London, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Filardo, Nathaniel |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Firsov, Denis |
CPP '25: "Leakage-Free Probabilistic ..."
Leakage-Free Probabilistic Jasmin Programs
Denis Firsov, Tiago Oliveira, José Bacelar Almeida, and Dominique Unruh
(Tallinn University of Technology, Estonia; SandboxAQ, n.n.; HASLab, n.n.; INESC TEC, Portugal; University of Minho, Portugal; University of Tartu, Estonia)
Article Search
|
|
From, Asta Halkjær |
CPP '25: "An Isabelle/HOL Framework ..."
An Isabelle/HOL Framework for Synthetic Completeness Proofs
Asta Halkjær From
(University of Copenhagen, Denmark)
Article Search
|
|
Georges, Aïna Linn
|
CPP '25: "The Nextgen Modality: A Modality ..."
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Simon Friis Vindum, Aïna Linn Georges, and Lars Birkedal
(Aarhus University, Denmark; MPI-SWS, Germany)
Article Search
|
|
Heidler, Katharina
|
CPP '25: "Formalizing the One-Way to ..."
Formalizing the One-Way to Hiding Theorem
Katharina Heidler and Dominique Unruh
(TU Munich, Germany; RWTH Aachen University, Germany)
Article Search
|
|
Henrio, Ludovic |
CPP '25: "Monadic Interpreters for Concurrent ..."
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski
(Inria - LIP, France; CNRS, France; Inria, France)
Article Search
|
|
Hivert, Florent |
CPP '25: "Machine Checked Proofs and ..."
Machine Checked Proofs and Programs in Algebraic Combinatorics
Florent Hivert
(University Paris-Saclay - LISN - LMF - CNRS - Inria, France)
Article Search
|
|
Jensen, Martin
|
CPP '25: "CertiCoq-Wasm: A Verified ..."
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, and Bas Spitters
(Aarhus University, Denmark)
Article Search
|
|
Kim, Dohan
|
CPP '25: "An Isabelle Formalization ..."
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Conditional Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
(University of Innsbruck, Austria; JAIST, Japan; NAIST, Japan)
Article Search
|
|
Kirk, Christina |
CPP '25: "Formalizing Simultaneous Critical ..."
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk and Aart Middeldorp
(University of Innsbruck, Austria)
Article Search
|
|
Li, Angela W.
|
CPP '25: "Verified and Efficient Matching ..."
Verified and Efficient Matching of Regular Expressions with Lookaround
Agnishom Chattopadhyay, Angela W. Li, and Konstantinos Mamouras
(Rice University, USA)
Article Search
|
|
Limperg, Jannis |
CPP '25: "Tactic Script Optimisation ..."
Tactic Script Optimisation for Aesop
Jannis Limperg
(LMU Munich, Germany)
Article Search
|
|
Mamouras, Konstantinos
|
CPP '25: "Verified and Efficient Matching ..."
Verified and Efficient Matching of Regular Expressions with Lookaround
Agnishom Chattopadhyay, Angela W. Li, and Konstantinos Mamouras
(Rice University, USA)
Article Search
|
|
Meier, Wolfgang |
CPP '25: "CertiCoq-Wasm: A Verified ..."
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, and Bas Spitters
(Aarhus University, Denmark)
Article Search
|
|
Memarian, Kayvan |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Middeldorp, Aart |
CPP '25: "Formalizing Simultaneous Critical ..."
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk and Aart Middeldorp
(University of Innsbruck, Austria)
Article Search
|
|
Minamide, Yasuhiko |
CPP '25: "Further Tackling Post Correspondence ..."
Further Tackling Post Correspondence Problem and Proof Generation
Akihiro Omori and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
CPP '25: "Formalization of Differential ..."
Formalization of Differential Privacy in Isabelle/HOL
Tetsuya Sato and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
|
|
Moffat, Alistair |
CPP '25: "Formalized Burrows-Wheeler ..."
Formalized Burrows-Wheeler Transform
Louis Cheung, Alistair Moffat, and Christine Rizkallah
(University of Melbourne, Australia)
Article Search
|
|
Momigliano, Alberto |
CPP '25: "Split Decisions: Explicit ..."
Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon, Chuta Sano, Alberto Momigliano, and Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)
Article Search
|
|
Monniaux, David |
CPP '25: "Formally Verified Hardening ..."
Formally Verified Hardening of C Programs against Hardware Fault Injection
Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet
(Ecole Nationale de l’Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; CNRS, France)
Article Search
|
|
Oliveira, Tiago
|
CPP '25: "Leakage-Free Probabilistic ..."
Leakage-Free Probabilistic Jasmin Programs
Denis Firsov, Tiago Oliveira, José Bacelar Almeida, and Dominique Unruh
(Tallinn University of Technology, Estonia; SandboxAQ, n.n.; HASLab, n.n.; INESC TEC, Portugal; University of Minho, Portugal; University of Tartu, Estonia)
Article Search
|
|
Omori, Akihiro |
CPP '25: "Further Tackling Post Correspondence ..."
Further Tackling Post Correspondence Problem and Proof Generation
Akihiro Omori and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
|
|
Pesin, Basile
|
CPP '25: "Formally Verified Hardening ..."
Formally Verified Hardening of C Programs against Hardware Fault Injection
Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet
(Ecole Nationale de l’Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; CNRS, France)
Article Search
|
|
Pichon-Pharabod, Jean |
CPP '25: "CertiCoq-Wasm: A Verified ..."
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, and Bas Spitters
(Aarhus University, Denmark)
Article Search
|
|
Pientka, Brigitte |
CPP '25: "Split Decisions: Explicit ..."
Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon, Chuta Sano, Alberto Momigliano, and Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)
Article Search
|
|
Potet, Marie-Laure |
CPP '25: "Formally Verified Hardening ..."
Formally Verified Hardening of C Programs against Hardware Fault Injection
Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet
(Ecole Nationale de l’Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; CNRS, France)
Article Search
|
|
Rizkallah, Christine
|
CPP '25: "Formalized Burrows-Wheeler ..."
Formalized Burrows-Wheeler Transform
Louis Cheung, Alistair Moffat, and Christine Rizkallah
(University of Melbourne, Australia)
Article Search
|
|
Rot, Jurriaan |
CPP '25: "Intrinsically Correct Sorting ..."
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide
(RPTU Kaiserslautern-Landau, Germany; University of Bologna, Italy; Radboud University Nijmegen, Netherlands)
Article Search
|
|
Saito, Teppei
|
CPP '25: "An Isabelle Formalization ..."
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Conditional Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
(University of Innsbruck, Austria; JAIST, Japan; NAIST, Japan)
Article Search
|
|
Sano, Chuta |
CPP '25: "Split Decisions: Explicit ..."
Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon, Chuta Sano, Alberto Momigliano, and Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)
Article Search
|
|
Sato, Tetsuya |
CPP '25: "Formalization of Differential ..."
Formalization of Differential Privacy in Isabelle/HOL
Tetsuya Sato and Yasuhiko Minamide
(Institute of Science Tokyo, Japan)
Article Search
|
|
Sebe, Mircea |
CPP '25: "Nominal Matching Logic with ..."
Nominal Matching Logic with Fixpoints
Mircea Sebe, Maribel Fernández, and James Cheney
(University of Illinois at Urbana-Champaign, USA; King’s College London, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Sewell, Peter |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Spitters, Bas |
CPP '25: "CertiCoq-Wasm: A Verified ..."
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, and Bas Spitters
(Aarhus University, Denmark)
Article Search
|
|
Stark, Ian |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|
|
Thiemann, René
|
CPP '25: "An Isabelle Formalization ..."
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Conditional Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
(University of Innsbruck, Austria; JAIST, Japan; NAIST, Japan)
Article Search
|
|
Unruh, Dominique
|
CPP '25: "Formalizing the One-Way to ..."
Formalizing the One-Way to Hiding Theorem
Katharina Heidler and Dominique Unruh
(TU Munich, Germany; RWTH Aachen University, Germany)
Article Search
CPP '25: "Leakage-Free Probabilistic ..."
Leakage-Free Probabilistic Jasmin Programs
Denis Firsov, Tiago Oliveira, José Bacelar Almeida, and Dominique Unruh
(Tallinn University of Technology, Estonia; SandboxAQ, n.n.; HASLab, n.n.; INESC TEC, Portugal; University of Minho, Portugal; University of Tartu, Estonia)
Article Search
|
|
Van der Weide, Niels
|
CPP '25: "Intrinsically Correct Sorting ..."
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, and Niels van der Weide
(RPTU Kaiserslautern-Landau, Germany; University of Bologna, Italy; Radboud University Nijmegen, Netherlands)
Article Search
|
|
Vindum, Simon Friis |
CPP '25: "The Nextgen Modality: A Modality ..."
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
Simon Friis Vindum, Aïna Linn Georges, and Lars Birkedal
(Aarhus University, Denmark; MPI-SWS, Germany)
Article Search
|
|
Yamada, Akihisa
|
CPP '25: "An Isabelle Formalization ..."
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Conditional Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
(University of Innsbruck, Austria; JAIST, Japan; NAIST, Japan)
Article Search
|
|
Zackon, Daniel
|
CPP '25: "Split Decisions: Explicit ..."
Split Decisions: Explicit Contexts for Substructural Languages
Daniel Zackon, Chuta Sano, Alberto Momigliano, and Brigitte Pientka
(McGill University, Canada; University of Milan, Italy)
Article Search
|
|
Zakowski, Yannick |
CPP '25: "Monadic Interpreters for Concurrent ..."
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski
(Inria - LIP, France; CNRS, France; Inria, France)
Article Search
|
|
Zaliva, Vadim |
CPP '25: "A CHERI C Memory Model for ..."
A CHERI C Memory Model for Verified Temporal Safety
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell
(University of Cambridge, United Kingdom; University of Edinburgh, United Kingdom)
Article Search
|