CPP - researchr conference series publications

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 100 from 341

2025

Formalization of Differential Privacy in Isabelle/HOLTetsuya Sato 0001, Yasuhiko Minamide. CPP 2025: 67-82 [doi]

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term RewritingDohan Kim 0001, Teppei Saito, René Thiemann, Akihisa Yamada 0001. CPP 2025: 272-282 [doi]

Intrinsically Correct Sorting in Cubical AgdaCass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide. CPP 2025: 34-49 [doi]

Leakage-Free Probabilistic Jasmin ProgramsJosé Bacelar Almeida, Denis Firsov, Tiago Oliveira 0004, Dominique Unruh. CPP 2025: 3-16 [doi]

Certifying Rings of Integers in Number FieldsAnne Baanen, Alain Chavarri Villarello, Sander R. Dahmen. CPP 2025: 50-66 [doi]

Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IRNicolas Chappe, Ludovic Henrio, Yannick Zakowski. CPP 2025: 283-298 [doi]

Verified and Efficient Matching of Regular Expressions with LookaroundAgnishom Chattopadhyay, Wu Angela Li, Konstantinos Mamouras. CPP 2025: 198-213 [doi]

Formalized Burrows-Wheeler TransformLouis Cheung, Alistair Moffat, Christine Rizkallah. CPP 2025: 187-197 [doi]

An Isabelle/HOL Framework for Synthetic Completeness ProofsAsta Halkjær From. CPP 2025: 171-186 [doi]

Formalizing the One-Way to Hiding TheoremKatharina Heidler, Dominique Unruh. CPP 2025: 243-256 [doi]

Machine Checked Proofs and Programs in Algebraic CombinatoricsFlorent Hivert. CPP 2025: 214-230 [doi]

CRIS: The Power of Imagination in Specification and Verification (Invited Talk)Chung-Kil Hur. CPP 2025: 2 [doi]

Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite SystemsChristina Kirk, Aart Middeldorp. CPP 2025: 156-170 [doi]

Tactic Script Optimisation for AesopJannis Limperg. CPP 2025: 98-111 [doi]

CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoqWolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters. CPP 2025: 127-139 [doi]

Further Tackling Post Correspondence Problem and Proof GenerationAkihiro Omori, Yasuhiko Minamide. CPP 2025: 231-242 [doi]

Formally Verified Hardening of C Programs against Hardware Fault InjectionBasile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet. CPP 2025: 140-155 [doi]

Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)Emily Riehl. CPP 2025: 1 [doi]

Nominal Matching Logic with FixpointsMircea Sebe, Maribel Fernández, James Cheney. CPP 2025: 17-33 [doi]

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025Kathrin Stark, Amin Timany, Sandrine Blazy, Nicolas Tabareau, editors, ACM, 2025. [doi]

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicSimon Friis Vindum, Aïna Linn Georges, Lars Birkedal. CPP 2025: 83-97 [doi]

Split Decisions: Explicit Contexts for Substructural LanguagesDaniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka. CPP 2025: 257-271 [doi]

A CHERI C Memory Model for Verified Temporal SafetyVadim Zaliva, Kayvan Memarian, Brian Campbell 0001, Ricardo Almeida 0003, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell. CPP 2025: 112-126 [doi]

2024

Martin-Löf à la CoqArthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet. CPP 2024: 230-245 [doi]

Displayed Monoidal Categories for the Semantics of Linear LogicBenedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert. CPP 2024: 260-273 [doi]

VCFloat2: Floating-Point Error Analysis in CoqAndrew W. Appel, Ariel Kellison. CPP 2024: 14-29 [doi]

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision DiagramsClément Chavanon, Frédéric Besson, Tristan Ninet. CPP 2024: 89-102 [doi]

UTC Time, Formally VerifiedAna de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten. CPP 2024: 2-13 [doi]

A Formalization of Complete Discrete Valuation Rings and Local FieldsMaría Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio. CPP 2024: 190-204 [doi]

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local LemmaChelsea Edmonds, Lawrence C. Paulson. CPP 2024: 132-146 [doi]

Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple ArgumentsJoseph Eremondi. CPP 2024: 205-217 [doi]

Formalizing Giles Gardam's Disproof of Kaplansky's Unit ConjectureSiddhartha Gadgil, Anand Rao Tadipatri. CPP 2024: 177-189 [doi]

The Last Yard: Foundational End-to-End Verification of High-Speed CryptographyPhilipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters. CPP 2024: 30-44 [doi]

Certification of Confluence- and Commutation-Proofs via Parallel Critical PairsNao Hirokawa, Dohan Kim 0001, Kiraku Shintani, René Thiemann. CPP 2024: 147-161 [doi]

Formalizing the ∞-Categorical Yoneda LemmaNikolai Kudasov, Emily Riehl, Jonathan Weinberger. CPP 2024: 274-290 [doi]

Memory Simulations, Security and Optimization in a Verified CompilerDavid Monniaux. CPP 2024: 103-117 [doi]

Unification for Subformula Linking under QuantifiersIke Mulder, Robbert Krebbers. CPP 2024: 75-88 [doi]

Compositional Verification of Concurrent C Programs with Search Structure TemplatesDuc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang. CPP 2024: 60-74 [doi]

Under-Approximation for Scalable Bug Detection (Keynote)Azalea Raad. CPP 2024: 1 [doi]

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic LogicIan Shillito, Dominik Kirst. CPP 2024: 218-229 [doi]

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy, editors, ACM, 2024. [doi]

Univalent Double CategoriesNiels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North. CPP 2024: 246-259 [doi]

A Temporal Differential Dynamic Logic Formal EmbeddingLauren White, Laura Titolo, J. Tanner Slagel, César A. Muñoz. CPP 2024: 162-176 [doi]

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation LogicQiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur 0001, Ilya Sergey. CPP 2024: 45-59 [doi]

Lean Formalization of Extended Regular Expression Matching with LookaroundsEkaterina Zhuchko, Margus Veanes, Gabriel Ebner. CPP 2024: 118-131 [doi]

2023

Terms for Efficient Proof Checking and ParsingMichael Färber 0002. CPP 2023: 135-147 [doi]

A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)Yannick Forster 0002, Felix Jahn, Gert Smolka. CPP 2023: 159-166 [doi]

Semantics of Probabilistic Programs using s-Finite Kernels in CoqReynald Affeldt, Cyril Cohen, Ayumu Saito. CPP 2023: 3-16 [doi]

A Formal Disproof of Hirsch ConjectureXavier Allamigeon, Quentin Canu, Pierre-Yves Strub. CPP 2023: 17-29 [doi]

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value StoresArvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy. CPP 2023: 30-46 [doi]

A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOLAngeliki Koutsoukou Argyraki, Mantas Baksys, Chelsea Edmonds. CPP 2023: 225-238 [doi]

Formalized Class Group Computations and Integral Points on Mordell Elliptic CurvesAnne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen. CPP 2023: 47-62 [doi]

CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote)Sandrine Blazy. CPP 2023: 1 [doi]

Compositional Pre-processing for Automated Reasoning in Dependent Type TheoryValentin Blot, Denis Cousineau 0003, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial. CPP 2023: 63-77 [doi]

Encoding Dependently-Typed Constructions into Simple Type TheoryAnthony Bordg, Adrián Doña Mateo. CPP 2023: 78-89 [doi]

A Formalized Reduction of Keller's ConjectureJoshua Clune. CPP 2023: 90-101 [doi]

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection ConstructivelyMatthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi. CPP 2023: 102-120 [doi]

Formalizing and Computing Propositional QuantifiersHugo Férée, Sam van Gool. CPP 2023: 148-158 [doi]

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-ElpiBenjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi. CPP 2023: 167-181 [doi]

Mechanised Semantics for Gated Static Single AssignmentYann Herklotz, Delphine Demange, Sandrine Blazy. CPP 2023: 182-196 [doi]

Improved Assistance for Interactive Proof (Keynote)Cezary Kaliszyk. CPP 2023: 2 [doi]

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite SystemsChristina Kohl, Aart Middeldorp. CPP 2023: 197-210 [doi]

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLKatherine Kosaian, Yong Kiam Tan, André Platzer. CPP 2023: 211-224 [doi]

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic, editors, ACM, 2023. [doi]

Computing Cohomology Rings in Cubical AgdaThomas Lamiaux, Axel Ljungström, Anders Mörtberg. CPP 2023: 239-252 [doi]

Aesop: White-Box Best-First Proof Search for LeanJannis Limperg, Asta Halkjær From. CPP 2023: 253-266 [doi]

Formalising Sharkovsky's Theorem (Proof Pearl)Bhavik Mehta. CPP 2023: 267-274 [doi]

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DERHaobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy. CPP 2023: 275-289 [doi]

Formalising Decentralised Exchanges in CoqEske Hoy Nielsen, Danil Annenkov, Bas Spitters. CPP 2023: 290-302 [doi]

P4Cub: A Little Language for Big RoutersRudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster. CPP 2023: 303-319 [doi]

Formalising the h-Principle and Sphere EversionFloris van Doorn, Patrick Massot, Oliver Nash. CPP 2023: 121-134 [doi]

Verifying Term Graph Optimizations using Isabelle/HOLBrae J. Webb, Ian J. Hayes, Mark Utting. CPP 2023: 320-333 [doi]

A Formalization of Doob's Martingale Convergence Theorems in mathlibKexing Ying, Rémy Degenne. CPP 2023: 334-347 [doi]

2022

CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022Andrei Popescu 0001, Steve Zdancewic, editors, ACM, 2022. [doi]

Implementing a category-theoretic framework for typed abstract syntaxBenedikt Ahrens, Ralph Matthes, Anders Mörtberg. CPP 2022: 307-323 [doi]

Certified abstract machines for skeletal semanticsGuillaume Ambal, Sergueï Lenglet, Alan Schmitt. CPP 2022: 55-67 [doi]

The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk)June Andronick. CPP 2022: 1 [doi]

Coq's vibrant ecosystem for verification engineering (invited talk)Andrew W. Appel. CPP 2022: 2-11 [doi]

A verified algebraic representation of cairo program executionJeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman. CPP 2022: 153-165 [doi]

Windmills of the minds: an algorithm for fermat's two squares theoremHing-Lun Chan. CPP 2022: 251-264 [doi]

Overcoming restraint: composing verification of foreign functions with cogentLouis Cheung, Liam O'Connor, Christine Rizkallah. CPP 2022: 13-26 [doi]

A compositional proof framework for FRETish requirementsEsther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle. CPP 2022: 68-81 [doi]

A drag-and-drop proof tacticPablo Donato, Pierre-Yves Strub, Benjamin Werner. CPP 2022: 197-209 [doi]

Verbatim++: verified, optimized, and semantically rich lexing with derivativesDerek Egolf, Sam Lasser, Kathleen Fisher. CPP 2022: 27-39 [doi]

Reflection, rewinding, and coin-toss in EasyCryptDenis Firsov, Dominique Unruh. CPP 2022: 166-179 [doi]

Semantic cut elimination for the logic of bunched implications, formalized in CoqDan Frumin. CPP 2022: 291-306 [doi]

Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewritingMichael Färber. CPP 2022: 225-238 [doi]

(Deep) induction rules for GADTsPatricia Johann, Enrico Ghiorzi. CPP 2022: 324-337 [doi]

CertiStr: a certified string solverShuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader. CPP 2022: 210-224 [doi]

A machine-checked direct proof of the Steiner-lehmus theoremAriel Kellison. CPP 2022: 265-273 [doi]

Undecidability, incompleteness, and completeness of second-order logic in CoqMark Koch, Dominik Kirst. CPP 2022: 274-290 [doi]

An extension of the framework types-to-sets for Isabelle/HOLMihails Milehins. CPP 2022: 180-196 [doi]

Specification and verification of a transient stackAlexandre Moine, Arthur Charguéraud, François Pottier. CPP 2022: 82-99 [doi]

Structural embeddings revisited (invited talk)César Muñoz. CPP 2022: 12 [doi]

Formalising lie algebrasOliver Nash. CPP 2022: 239-250 [doi]

On homotopy of walks and spherical maps in homotopy type theoryJonathan Prieto-Cubides. CPP 2022: 338-351 [doi]

Formal verification of a distributed dynamic reconfiguration protocolWilliam Schultz, Ian Dardik, Stavros Tripakis. CPP 2022: 143-152 [doi]

Formally verified superblock schedulingCyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino. CPP 2022: 40-54 [doi]

Forward build systems, formallySarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. CPP 2022: 130-142 [doi]

Mechanized verification of a fine-grained concurrent queue from meta's folly librarySimon Friis Vindum, Dan Frumin, Lars Birkedal. CPP 2022: 100-115 [doi]

Sign in or sign up to see more results.

runs on WebDSL