使厌恶
发表于 2025-3-26 23:57:42
A Formal Library for Elliptic Curves in the Coq Proof Assistantathematical theory. In this paper we present a formalization of elliptic curves theory, in the SSReflect extension of the Coq proof assistant. Our central contribution is a library containing many of the objects and core properties related to elliptic curve theory. We demonstrate the applicability o
PATRI
发表于 2025-3-27 01:26:57
Truly Modular (Co)datatypes for Isabelle/HOL-behaved type constructors, including mixed recursion–corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle’s Coinductive library to use the new commands, elimin
AXIOM
发表于 2025-3-27 09:12:10
Cardinals in Isabelle/HOLordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation that identifies ordinals with wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss two applications of this general theory in
思乡病
发表于 2025-3-27 12:42:13
http://reply.papertrans.cn/48/4706/470574/470574_34.png
巧办法
发表于 2025-3-27 14:37:06
http://reply.papertrans.cn/48/4706/470574/470574_35.png
incision
发表于 2025-3-27 19:32:26
A Computer-Algebra-Based Formal Proof of the Irrationality of ,(3)tant. This result was first proved by Apéry in 1978, and the proof we have formalized follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations p
流出
发表于 2025-3-27 22:58:51
From Operational Models to Information Theory; Side Channels in pGCL with Isabelle modelled in pGCL. Our principal theoretical contribution is to link the process-oriented view, where attacker and system execute particular model programs, and the information-theoretic view, where the attacker solves an optimal-decoding problem, viewing the system as a noisy channel. Our practical
harrow
发表于 2025-3-28 03:18:40
http://reply.papertrans.cn/48/4706/470574/470574_38.png
Injunction
发表于 2025-3-28 07:39:37
Formalized, Effective Domain Theory in Coq., . and that supports all the usual constructions on domains. In particular, I develop constructive models of both the unpointed profinite and the pointed profinite domains. Standard constructions (e.g., products, sums, the function space, and powerdomains) are all developed. In addition, I build t
过份
发表于 2025-3-28 10:53:18
http://reply.papertrans.cn/48/4706/470574/470574_40.png