Engaging
发表于 2025-3-26 23:57:52
http://reply.papertrans.cn/48/4706/470573/470573_31.png
orthopedist
发表于 2025-3-27 03:06:08
http://reply.papertrans.cn/48/4706/470573/470573_32.png
Conscientious
发表于 2025-3-27 06:47:28
Formalizing Bounded Increases of the Babylonian algorithm to compute square roots. These algorithms were required to write executable functions which can certify untrusted termination proofs from termination tools that make use of bounded increase. And indeed, the resulting certifier was already useful: it detected an implementation error that remained undetected since 2007.
alcohol-abuse
发表于 2025-3-27 12:18:35
Scalable LCF-Style Proof Translationours on commodity hardware. We also provide mappings for most basic types present in the developments including lists, integers and real numbers. This papers outlines some design considerations and presents a few of our extensive measurements, which reveal interesting insights in the low-level structure of larger proof developments.
vitreous-humor
发表于 2025-3-27 17:05:52
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computationputational model, there exists a witness from which the same reduction may be simulated . by the monad. We encode several examples using simulable monads and demonstrate the advantages of the technique over previous approaches.
Gustatory
发表于 2025-3-27 19:48:34
http://reply.papertrans.cn/48/4706/470573/470573_36.png
爆炸
发表于 2025-3-28 01:11:22
Conference proceedings 2013n July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics
Dissonance
发表于 2025-3-28 06:01:16
Automating Theorem Proving with SMTof examples that illustrate how theorems are expressed and proved. Since the SMT solver takes care of many formal trivialities automatically, users can focus more of their time on the creative ingredients of proofs.
放气
发表于 2025-3-28 06:58:26
Certifying Voting Protocolss its result. Our work within the DemTech research project (.) aims to maintain or even increase the level of the trust by applying modern theorem proving technology to the domain of voting protocols and schemas.
LAP
发表于 2025-3-28 11:33:18
Kleene Algebra with Tests and Coq Tools for while Programsositional Hoare logic..We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.