3 papers
cs.PL2025
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Qiyuan Xu, Renxi Wang, Peixin Wang +2
Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using na…
cs.LO2025
Generalized Security-Preserving Refinement for Concurrent Systems
Huan Sun, David Sanán, Jingyi Wang +3
Ensuring compliance with Information Flow Security (IFS) is known to be challenging, especially for concurrent systems with large codebases such as multicore operating system (OS)…
cs.PL2025
Generically Automating Separation Logic by Functors, Homomorphisms and Modules
Qiyuan Xu, David Sanan, Zhe Hou +3
Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs.…