Titlebook: Interactive Theorem Proving; Third International Lennart Beringer,Amy Felty Conference proceedings 2012 Springer-Verlag Berlin Heidelberg

metamorphose

书目名称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读者反馈学科排名

Cleave

Computer-Aided Cryptographic Proofsused to verify emblematic examples of public-key encryption schemes, digital signature schemes, hash function designs, and block cipher modes of operation. The purpose of this paper is to motivate the role of computer-aided proofs in the broader context of provable security and to illustrate the wor

Charlatan

A Differential Operator Approach to Equational Differential Invariantsive to differential equations. Differential invariants are a natural induction principle for proving properties of the remaining differential equations. We study the equational case of differential invariants using a differential operator view. We relate differential invariants to Lie’s seminal work

拍翅

异教徒

凶残

Construction of Real Algebraic Numbers in C,himedean real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a refe

kindred

A Refinement-Based Approach to Computational Algebra in ,ed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank compu

cardiopulmonary

Bridging the Gap: Automatic Verified Abstraction of Chat theorem prover. Accurate translations of such code should be conservative, choosing safe representations over representations convenient to reason about. This paper bridges the gap between conservative representation and convenient reasoning. We present a tool that automatically abstracts low-le

dissent

避开