Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.8K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#coq

3 posts3 participants0 posts today
Public
もく

discourse.rocq-prover.org/t/co

This is the saddest Discourse post I've ever read😢
#Coq -> #Rocq

Rocq Prover · Coq Community Survey 2022 Results: Part IV and ITP paper announcementCoq Community Survey 2022 Results: Part IV and ITP paper announcement TL;DR: This post completes a series of three previous posts (part I, part II, part III) with plots of answers to questions not yet analyzed in previous posts, and with the announcement of an article at ITP about the survey and the associated dataset. The Coq Community Survey 2022 was organized by an ad hoc working group and conducted during February 2022. It contained 109 questions (in English and Chinese) and received 466 an...
Public
José A. Alonso

Efficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. arxiv.org/abs/2504.07732

arXiv logo
arXiv.orgEfficient Formal Verification of Quantum Error Correcting ProgramsQuantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.
Public
José A. Alonso

Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. arxiv.org/abs/2503.17159

arXiv logo
arXiv.orgBi-intuitionistic logics through the abstract algebraic logic lensSince the discovery of critical mistakes in Rauszer's work on bi-intuitionistic logics, solid foundations for these have progressively been rebuilt. However, the algebraic treatment of these logics has not yet been tended to. We fill this gap by algebraically analysing the bi-intuitionistic logics wBIL and sBIL. Given that these logics are only distinguished as consequence relations, and not as sets of theorems (hence the conflation in Rauszer's work), the algebraic tools we use are tailored to the treatment of such relations. We mainly inspect these logics through the lens of abstract algebraic logic, but we also provide an alternative algebraic analysis of wBIL and sBIL as logic preserving degrees of truth and truth, respectively. Our results pertaining to wBIL and sBIL are formalised in the interactive theorem prover Rocq.
Public
José A. Alonso

Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). arxiv.org/abs/2407.06222

arXiv logo
arXiv.orgFormalization of the Filter Extension Principle (FEP) in CoqThe Filter Extension Principle (FEP) asserts that every filter can be extended to an ultrafilter, which plays a crucial role in the quest for non-principal ultrafilters. Non-principal ultrafilters find widespread applications in logic, set theory, topology, model theory, and especially non-standard extensions of algebraic structures. Since non-principal ultrafilters are challenging to construct directly, the Filter Extension Principle, stemming from the Axiom of Choice, holds significant value in obtaining them. This paper presents the formal verification of the Filter Extension Principle, implemented using the Coq proof assistant and grounded in axiomatic set theory. It offers formal descriptions for the concepts related to filter base, filter, ultrafilter and more. All relevant theorems, propositions, and the Filter Extension Principle itself are rigorously and formally verified. This work sets the stage for the formalization of non-standard analysis and a specific real number theory.
SearchLive feeds
About