default search action

combined dblp search
author search
venue search
publication search

ask others

12th CPP 2023: Boston, MA, USA

> Home > Conferences and Workshops > CPP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/2023
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2023
Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Blazy23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Blazy23
Sandrine Blazy:
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). 1
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Kaliszyk23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Kaliszyk23
Cezary Kaliszyk:
Improved Assistance for Interactive Proof (Keynote). 2
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AffeldtCS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AffeldtCS23
Reynald Affeldt, Cyril Cohen, Ayumu Saito:
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. 3-16
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AllamigeonCS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AllamigeonCS23
Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of Hirsch Conjecture. 17-29
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ArasuRRSFHPR23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ArasuRRSFHPR23
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy:
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. 30-46
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BaanenBCD23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BaanenBCD23
Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen:
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. 47-62
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Blot0CPKMV23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Blot0CPKMV23
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial:
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. 63-77
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BordgM23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BordgM23
Anthony Bordg, Adrián Doña Mateo:
Encoding Dependently-Typed Constructions into Simple Type Theory. 78-89
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Clune23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Clune23
Joshua Clune:
A Formalized Reduction of Keller's Conjecture. 90-101
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DaggittAKKA23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DaggittAKKA23
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi:
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. 102-120
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoornMN23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoornMN23
Floris van Doorn, Patrick Massot, Oliver Nash:
Formalising the h-Principle and Sphere Eversion. 121-134
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Farber23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Farber23
Michael Färber:
Terms for Efficient Proof Checking and Parsing. 135-147
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FereeG23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FereeG23
Hugo Férée, Sam van Gool:
Formalizing and Computing Propositional Quantifiers. 148-158
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0002JS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0002JS23
Yannick Forster, Felix Jahn, Gert Smolka:
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). 159-166
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GregoireLT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GregoireLT23
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi:
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. 167-181
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HerklotzDB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HerklotzDB23
Yann Herklotz, Delphine Demange, Sandrine Blazy:
Mechanised Semantics for Gated Static Single Assignment. 182-196
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KohlM23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KohlM23
Christina Kohl, Aart Middeldorp:
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. 197-210
- view
  - electronic edition via DOI (open access)
  - references & citations
  authority control:
- export record
  dblp key:
  - conf/cpp/KosaianTP23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KosaianTP23
Katherine Kosaian, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. 211-224
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Koutsoukou-Argyraki23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Koutsoukou-Argyraki23
Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds:
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. 225-238
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LamiauxLM23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LamiauxLM23
Thomas Lamiaux, Axel Ljungström, Anders Mörtberg:
Computing Cohomology Rings in Cubical Agda. 239-252
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LimpergF23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LimpergF23
Jannis Limperg, Asta Halkjær From:
Aesop: White-Box Best-First Proof Search for Lean. 253-266
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Mehta23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Mehta23
Bhavik Mehta:
Formalising Sharkovsky's Theorem (Proof Pearl). 267-274
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NiDFRS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NiDFRS23
Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy:
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. 275-289
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NielsenAS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NielsenAS23
Eske Hoy Nielsen, Danil Annenkov, Bas Spitters:
Formalising Decentralised Exchanges in Coq. 290-302
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/PetersonCCISDAF23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/PetersonCCISDAF23
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster:
P4Cub: A Little Language for Big Routers. 303-319
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/WebbHU23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/WebbHU23
Brae J. Webb, Ian J. Hayes, Mark Utting:
Verifying Term Graph Optimizations using Isabelle/HOL. 320-333
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/YingD23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/YingD23
Kexing Ying, Rémy Degenne:
A Formalization of Doob's Martingale Convergence Theorems in mathlib. 334-347

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.