Titlebook: Interactive Theorem Proving; 6th International Co Christian Urban,Xingyuan Zhang Conference proceedings 2015 Springer International Publish

顾客

978-3-319-22101-4Springer International Publishing Switzerland 2015

aesthetician

乱砍

浮雕

https://doi.org/10.1007/978-3-319-22102-1Coq; Isabelle/HOL; automated planning; bracket polynomial; embedded systems; error-correcting codes; forma

臭名昭著

Christian Urban,Xingyuan ZhangIncludes supplementary material:

推延

Cleave

,Mechanisation of AKS Algorithm: Part 1 – The Main Theorem,s from finite fields. This paper describes the first step towards the goal of a full mechanisation of this result: a mechanisation of the AKS Main Theorem, which justifies the correctness (but not the complexity) of the AKS algorithm.

entitle

啜泣

逃避现实

HOCore in Coq,. We highlight a number of important technical issues that we have uncovered in the original publication. We believe that these issues are not unique to the paper under consideration and require particular care to be avoided.