Canyam
AI summaries for academic research
Home
Preprint
Subscribe
Favorites
Tools
Analysis
Summary
Not logged in
Back
Journal Details
P
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
Papers
27
Citations
Related Insights
0
subscribe
Journal Papers
27
Related Insights
0
Journal Papers
27
Publication Date
Publication Date
IF
Citations
Mechanizing Synthetic Tait Computability in Istari
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Li, Runming; Yao, Yue; Harper, Robert
Share
Save
Towards Composable Proofs of Cache Coherence Protocols
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Camaioni, Martina; Herklotz, Yann; Yu, Tz-Ching; Bourgeat, Thomas
Share
Save
Foundational Verification of Running-Time Bounds for Interactive Programs
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Tockman, Andy; Singh, Pratap; Erbsen, Andres; Gruetter, Samuel; Chlipala, Adam
Share
Save
Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Thies, Holger
Share
Save
Certifying the Decidability of the Word Problem in Monoids at Large
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Cirpons, Reinis; Hivert, Florent; Mahboubi, Assia; Melquiond, Guillaume; Mitchell, James D.; Smith, Finn
Share
Save
Precise Reasoning about Container-Internal Pointers with Logical Pinning
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Guan, Yawen; Pit-Claudel, Clement
Share
Save
A Rose Tree Is Blooming (Proof Pearl)
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Korkut, Joomy
Share
Save
Higher Order Differential Calculus in Mathlib
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Gouezel, Sebastien
Share
Save
Cylindrical Algebraic Decomposition in Coq/Rocq
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Vermande, Quentin
Share
Save
Formalizing Polynomial Laws and the Universal Divided Power Algebra
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Chambert-Loir, Antoine; de Frutos-Fernandez, Maria Ines
Share
Save
BRACK: A Verified Compiler for Scheme via CakeML
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Lasnier, Pascal Y.; Yallop, Jeremy; Myreen, Magnus O.
Share
Save
Building Blocks for Step-Indexed Program Logics
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Somers, Thomas; Hinrichsen, Jonas Kastberg; Gaeher, Lennard; Krebbers, Robbert
Share
Save
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Mascarenhas, Tomaz; Khan, Harun; Mohamed, Abdalrhman; Reynolds, Andrew; Barbosa, Haniel; Barrett, Clark; Tinelli, Cesare
Share
Save
Adhesive Category Theory for Graph Rewriting in Rocq
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Arsac, Samuel; Harmer, Russ; Pous, Damien
Share
Save
Bar Inductive Predicates for Constructive Algebra in Rocq
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Larchey-Wendling, Dominique
Share
Save
Mechanized Dominator Tree Certification
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Lechenet, Jean-Christophe
Share
Save
A Certifying Proof Assistant for Synthetic Mathematics in Lean
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Nawrocki, Wojciech; Hua, Joseph; Carneiro, Mario; Xu, Yiming; Woolfson, Spencer; Rong, Shuge; Hazratpour, Sina; Awodey, Steve
Share
Save
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Marionneau, Virgil; Bourda, Felix Sassus; Aguirre, Alejandro; Birkedal, Lars
Share
Save
Adding Sorts to an Isabelle Formalization of Superposition
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Toth, Balazs; Desharnais-Schafer, Martin; Blanchette, Jasmin
Share
Save
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
PROCEEDINGS OF THE 15TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2026
IF
0
2026-01-01
0
PRE
AI
Trabish, David; Itzhaky, Shachar
Share
Save
.png){kind=icon}
.png){kind=icon}
Not logged in.png){kind=icon}
Not logged in.png){kind=icon}
.png){kind=icon}
.png){kind=icon}
.png){kind=icon}