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

債務(wù)人

書目名稱Interactive Theorem Proving影響因子(影響力)




書目名稱Interactive Theorem Proving影響因子(影響力)學(xué)科排名




書目名稱Interactive Theorem Proving網(wǎng)絡(luò)公開度




書目名稱Interactive Theorem Proving網(wǎng)絡(luò)公開度學(xué)科排名




書目名稱Interactive Theorem Proving被引頻次




書目名稱Interactive Theorem Proving被引頻次學(xué)科排名




書目名稱Interactive Theorem Proving年度引用




書目名稱Interactive Theorem Proving年度引用學(xué)科排名




書目名稱Interactive Theorem Proving讀者反饋




書目名稱Interactive Theorem Proving讀者反饋學(xué)科排名

故意釣到白楊

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.