LEERY
发表于 2025-3-30 11:29:40
http://reply.papertrans.cn/48/4706/470577/470577_51.png
follicular-unit
发表于 2025-3-30 12:37:10
http://reply.papertrans.cn/48/4706/470577/470577_52.png
Lasting
发表于 2025-3-30 17:40:08
How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation,ecent breakthroughs are bringing MPC into practice, solving fundamental challenges for secure distributed computation. Just as with classic protocols for encryption and key exchange, precise guarantees are needed for MPC designs and implementations; any flaw will give attackers a chance to break pri
栏杆
发表于 2025-3-30 21:49:05
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability, in ad hoc pointwise translations, e.g. between HOL Light and Isabelle in the Flyspeck project or uses of more or less complete certificates. We propose in this paper a methodology to combine proofs coming from different theorem provers. This methodology relies on the Dedukti logical framework as a
INCH
发表于 2025-3-31 04:03:00
,A Formal Proof in , of LaSalle’s Invariance Principle,he asymptotic stability of the solutions to a nonlinear system of differential equations and several extensions of this principle have been designed to fit different particular kinds of system. In this paper we present a formalization, in the . proof assistant, of a slightly improved version of the
BLUSH
发表于 2025-3-31 07:10:56
http://reply.papertrans.cn/48/4706/470577/470577_56.png
condone
发表于 2025-3-31 11:11:09
Certifying Standard and Stratified Datalog Inference Engines in SSReflect,nd of its extension with stratified negation. The library contains a formalization of the model theoretical and fixpoint semantics of the languages, implemented through bottom-up and, respectively, through stratified evaluation procedures. We provide corresponding soundness, termination, completenes
钳子
发表于 2025-3-31 15:04:22
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq,e and as a model of computation. We show key results including (1) semantic properties of procedures are undecidable, (2) the class of total procedures is not recognisable, (3) a class is decidable if it is recognisable, corecognisable, and logically decidable, and (4) a class is recognisable if and
死猫他烧焦
发表于 2025-3-31 19:32:02
,Bellerophon: Tactical Theorem Proving for Hybrid Systems, motion. Verification is undecidable for hybrid systems and challenging for many models and properties of practical interest. Thus, human interaction and insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing them to focus on those insights
fender
发表于 2025-4-1 00:07:31
,A Formalized General Theory of Syntax with Bindings,malization efforts. Terms are defined for an arbitrary number of constructors of varying numbers of inputs, quotiented to alpha-equivalence and sorted according to a binding signature. The theory includes a rich collection of properties of the standard operators on terms, such as substitution and fr