Research Articleposted 2025-07-30 08:48:06
Automated reasoning boosted by a probabilistic automaton classifier: An application to the Andrews-Curtis conjecture
Michael Fairbank, Alexei Lisitsa, Alexei Vernitski
Under Revision
at
Research Articleposted 2024-08-27 08:43:25
A connection method for a defeasible extension of ALCH
Renan Fernandes, Fred Freitas, Ivan Varzinczak, Pedro P. M. Farias
Under Review
at
Research Articleposted 2024-07-24 19:39:19
A Mechanically Verified Garbage Collector for OCaml
Sheera Shamsu, Dipesh Kaphle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, Sivaramakrishnan KC
Published
at
Research Articleposted 2024-06-13 18:02:41
Reimplementing Mizar in Rust
Mario Carneiro
Under Revision
at
Research Articleposted 2024-05-27 10:44:38
Windmills of the Minds: A Hopping Algorithm for Fermat's Two Squares Theorem
Hing Lun Chan
Published
at
Research Articleposted 2024-05-09 09:35:44
Timed Automata Verification and Synthesis via Finite Automata Learning
Ocan Sankur
Published
at
Research Articleposted 2023-05-15 04:17:33
Verifying Programs with Logic and Extended Proof Rules: Deep Embed v.s. Shallow Embed
Zhongye Wang, Qinxiang Cao, Yichen Tao
Published
at
Research Articleposted 2023-05-12 06:19:40
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Published
at
Research Articleposted 2023-03-28 15:51:14
Refinement of Parallel Algorithms down to LLVM applied to practically efficient parallel sorting
Peter Lammich
Published
at
Research Articleposted 2023-03-03 12:32:27
Rensets and Renaming-Based Recursion for Syntax with Bindings: Extended Version
Andrei Popescu
Published
at