Titlebook: Interactive Theorem Proving; Second International Marko Eekelen,Herman Geuvers,Freek Wiedijk Conference proceedings 2011 Springer-Verlag Gm

债务人

书目名称Interactive Theorem Proving影响因子(影响力)




书目名称Interactive Theorem Proving影响因子(影响力)学科排名




书目名称Interactive Theorem Proving网络公开度




书目名称Interactive Theorem Proving网络公开度学科排名




书目名称Interactive Theorem Proving被引频次




书目名称Interactive Theorem Proving被引频次学科排名




书目名称Interactive Theorem Proving年度引用




书目名称Interactive Theorem Proving年度引用学科排名




书目名称Interactive Theorem Proving读者反馈




书目名称Interactive Theorem Proving读者反馈学科排名

故意钓到白杨

Verified Synthesis of Knowledge-Based Programs in Finite Synchronous EnvironmentsKBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle’s locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle’s code generator.

cogitate

https://doi.org/10.1007/978-3-642-22863-6ACL2; Coq; HOL; Isabelle; formal methods; program semantics; proof assistants

MAG

978-3-642-22862-9Springer-Verlag GmbH Berlin Heidelberg 2011

NAUT

Interactive Theorem Proving978-3-642-22863-6Series ISSN 0302-9743 Series E-ISSN 1611-3349

Vldl379

Advances in the Formalization of the Odd Order TheoremWe present some of the proof techniques and library designs we used to formalize a large part of the proof of the Odd Order theorem.

cancer

蕨类

Lecture Notes in Computer Sciencehttp://image.papertrans.cn/i/image/470571.jpg

dowagers-hump

Abduct

Formalization of Entropy Measures in HOLe some of its properties using the HOL theorem prover. This infrastructure is then used to formalize information theoretic fundamentals like Shannon entropy and relative entropy. We discuss potential applications of the proposed formalization for the analysis of data compression and security protocols.