Titlebook: Interactive Theorem Proving; 4th International Co Sandrine Blazy,Christine Paulin-Mohring,David Pich Conference proceedings 2013 Springer-V

Engaging

orthopedist

Conscientious

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

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

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

爆炸

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

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.

放气

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

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.