CPP - researchr conference series publications

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 100 from 369

2026

Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical AgdaLiang-TIng Chen 0001, Fredrik Nordvall Forsberg, Tzu-Chun Tsai. CPP 2026: 201-215 [doi]

Building Blocks for Step-Indexed Program LogicsThomas Somers 0001, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers. CPP 2026: 248-263 [doi]

Adhesive Category Theory for Graph Rewriting in RocqSamuel Arsac, Russ Harmer, Damien Pous. CPP 2026: 59-74 [doi]

Towards Composable Proofs of Cache Coherence ProtocolsMartina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat. CPP 2026: 325-338 [doi]

Formalizing Polynomial Laws and the Universal Divided Power AlgebraAntoine Chambert-Loir, María Inés de Frutos-Fernández. CPP 2026: 75-87 [doi]

Certifying the Decidability of the Word Problem in Monoids at LargeReinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith. CPP 2026: 128-142 [doi]

A Recipe for Modular Verification of Generic Tree TraversalsLaila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg 0001. CPP 2026: 339-352 [doi]

Using Ghost Ownership to Verify Union-Find and Persistent Arrays in RustArnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan. CPP 2026: 383-397 [doi]

Higher Order Differential Calculus in MathlibSébastien Gouëzel. CPP 2026: 1-14 [doi]

Precise Reasoning about Container-Internal Pointers with Logical PinningYawen Guan, Clément Pit-Claudel. CPP 2026: 353-367 [doi]

A Lambda-Superposition Tactic for Isabelle/HOLMassin Guerdi. CPP 2026: 117-127 [doi]

Layers of Confluence for ActorsLudovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski. CPP 2026: 309-324 [doi]

Certified Symbolic Finite Transducers: Formalization and Applications to String AnalysisShuanglong Kan, Anthony W. Lin. CPP 2026: 279-293 [doi]

A Rose Tree Is Blooming (Proof Pearl)Joomy Korkut. CPP 2026: 264-278 [doi]

Bar Inductive Predicates for Constructive Algebra in RocqDominique Larchey-Wendling. CPP 2026: 15-28 [doi]

Brack: A Verified Compiler for Scheme via CakeMLPascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen. CPP 2026: 157-170 [doi]

Mechanizing Synthetic Tait Computability in IstariRunming Li, Yue Yao, Robert Harper 0001. CPP 2026: 231-247 [doi]

Mechanized Dominator Tree CertificationJean-Christophe Léchenet. CPP 2026: 143-156 [doi]

Modular Specifications and Implementations of Random Samplers in Higher-Order Separation LogicVirgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre 0001, Lars Birkedal. CPP 2026: 368-382 [doi]

Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental FunctionsTomaz Mascarenhas, Harun Khan 0001, Abdalrhman Mohamed, Andrew Reynolds 0001, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli. CPP 2026: 216-230 [doi]

A Certifying Proof Assistant for Synthetic Mathematics in LeanWojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey. CPP 2026: 88-103 [doi]

Verified VCG and Verified Compiler for DafnyDaniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan. CPP 2026: 171-186 [doi]

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau, editors, ACM, 2026. [doi]

Computing Solutions for Systems of Multivariate Ordinary Differential Equations in RocqHolger Thies. CPP 2026: 29-44 [doi]

Foundational Verification of Running-Time Bounds for Interactive ProgramsAndy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala. CPP 2026: 187-200 [doi]

Enhancing Symbolic Execution with Machine-Checked Safety ProofsDavid Trabish, Shachar Itzhaky. CPP 2026: 294-308 [doi]

Adding Sorts to an Isabelle Formalization of SuperpositionBalázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette. CPP 2026: 104-116 [doi]

Cylindrical Algebraic Decomposition in Coq/RocqQuentin Vermande. CPP 2026: 45-58 [doi]

2025

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]

Formalization of Differential Privacy in Isabelle/HOLTetsuya Sato 0001, Yasuhiko Minamide. CPP 2025: 67-82 [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]

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]

Sign in or sign up to see more results.

runs on WebDSL