esculent
发表于 2025-3-23 10:25:40
http://reply.papertrans.cn/48/4706/470577/470577_11.png
Diatribe
发表于 2025-3-23 15:30:11
http://reply.papertrans.cn/48/4706/470577/470577_12.png
Wordlist
发表于 2025-3-23 19:51:38
Formalization of the Lindemann-Weierstrass Theorem,ve forms of the fundamental theorem of symmetric polynomials. This formalization uses mainly the Mathcomp library for the part relying on algebra, and the Coquelicot library and the Coq standard library of real numbers for the calculus part.
cruise
发表于 2025-3-24 02:09:48
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics,s available..The whole proof of . is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.
Sciatica
发表于 2025-3-24 03:52:49
Formal Verification of a Floating-Point Expansion Renormalization Algorithm, operation. It is a critical step needed to ensure that the resulted expansion has the same property as the input one, and is more “compressed”. The formal proof uncovered several gaps in the pen-and-paper proof and gives the algorithm a very high level of guarantee.
轻打
发表于 2025-3-24 06:31:15
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability,, we rely on the structuring features offered by FoCaLiZe, in particular parameterized modules and inheritance to build a formal library of transfer theorems called MathTransfer. We finally illustrate this methodology on the Sieve of Eratosthenes, which we prove correct using HOL and Coq in combination.
condone
发表于 2025-3-24 13:00:38
Conference proceedings 2017, in September 2017...The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization
cognizant
发表于 2025-3-24 17:47:38
http://reply.papertrans.cn/48/4706/470577/470577_18.png
RAG
发表于 2025-3-24 22:33:57
Automating Formalization by Statistical and Semantic Parsing of Mathematics,We show that our learning method allows efficient use of large amount of contextual information, which in turn significantly boosts the precision of the statistical parsing and also makes it more efficient. This leads to a large improvement of our first results in parsing theorems from the Flyspeck corpus.
lacrimal-gland
发表于 2025-3-25 02:19:55
http://reply.papertrans.cn/48/4706/470577/470577_20.png