18:56

[CPP'23] Terms for Efficient Proof Checking and Parsing

ACM SIGPLAN

20:48

[CPP'23] Compositional pre-processing for automated reasoning in dependent type theory

ACM SIGPLAN

20:18

[CPP'23] Practical and sound equality tests, automatically

ACM SIGPLAN

27:24

[CPP'23] Compiling higher-order specifications to SMT solvers: how to deal with rejection ...

ACM SIGPLAN

22:24

[CPP'23] FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores

ACM SIGPLAN

17:59

[CPP'23] Formalising Decentralised Exchanges in Coq

ACM SIGPLAN

23:53

[CPP'23] Semantics of Probabilistic Programs using S-Finite Kernels in Coq

ACM SIGPLAN

28:02

[CPP'23] Formalising Sharkovsky's Theorem (Proof Pearl)

ACM SIGPLAN

23:54

[CPP'23] A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

ACM SIGPLAN

18:08

[CPP'23] P4Cub: A Little Language for Big Routers

ACM SIGPLAN

24:36

[CPP'23] ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER

ACM SIGPLAN

20:47

[CPP'23] Verifying term graph optimizations using Isabelle/HOL

ACM SIGPLAN

49:37

[CPP'23] CompCert: a journey through the landscape of mechanized semantics for verified co...

ACM SIGPLAN

22:19

[CPP'23] Mechanised Semantics for Gated Static Single Assignment

ACM SIGPLAN

23:57

[CPP'23] Formalising the h-principle and sphere eversion

ACM SIGPLAN

22:06

[CPP'23] A Formalized Reduction of Keller's Conjecture

ACM SIGPLAN

18:41

[CPP'23] Computing Cohomology Rings in Cubical Agda

ACM SIGPLAN

25:20

[CPP'23] CPP Business Meeting

ACM SIGPLAN

22:51

[CPP'23] A Formalization of the Development Closedness Criterion for Left-Linear Term Rewr...

ACM SIGPLAN

22:27

[CPP'23] Formalizing and computing propositional quantifiers

ACM SIGPLAN

21:33

[CPP'23] Encoding Dependently-Typed Constructions into Simple Type Theory

ACM SIGPLAN

19:15

[CPP'23] A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive...

ACM SIGPLAN

22:19

[CPP'23] Aesop: White-Box Best-First Proof Search for Lean

ACM SIGPLAN

21:44

[CPP'23] A formalization of Doob's martingale convergence theorems in mathlib

ACM SIGPLAN

20:29

[CPP'23] A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL

ACM SIGPLAN

19:01

[CPP'23] A Formal Disproof of Hirsch Conjecture

ACM SIGPLAN

22:29

[CPP'23] Formalized Class Group Computations and Integral Points on Mordell Elliptic Curve...

ACM SIGPLAN