QWIRE Practice: Formal Verification of Quantum Circuits in Coq
我们描述了在Coq证明助手中嵌入QWIRE量子电路语言。这允许程序员使用高级抽象来编写量子电路，并使用Coq的定理证明功能来证明这些电路的属性。该实现使用高阶抽象语法来表示变量绑定，并为线性导线类型提供类型检查算法，确保量子电路是良构的。我们形式化了一个指称语义，将QWIRE电路解释为密度矩阵上的超算子，并证明了一些简单量子程序的正确性。
2018-03-02 cs.ET cs.LO cs.PL
A Graphical Interface for Category Theory Proofs in Coq
针对范畴论抽象难学、证明助手多为文本形式的问题，研究提出并实现了一款Coq插件，提供范畴论证明的图形化界面，支持可视化与交互，助力学生掌握图表推理。
2025-05-09 cs.LO cs.PL
Proceedings First International Workshop on Hammers for Type Theories
本卷EPTCS包含了2016年7月1日在葡萄牙科英布拉举行的自动推理国际联合会议（IJCAR 2016）的一部分，第一次类型论的锤子研讨会（HaTT 2016）的会议记录。会议记录包括四份定期论文以及Pierre Corbineau（Verimag，法国）和Aleksy Schubert（华沙大学，波兰）应邀发表的两次演讲的摘要。
2016-06-17 cs.AI cs.LG cs.LO
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
本文提出Lean-auto，一种在Lean 4与自动定理证明器之间的翻译算法，首次在Lean 4中实现基于ATP的通用证明自动化，保证健全性并在Mathlib4上优于现有工具。
2025-05-24 cs.LO
Experience Implementing a Performant Category-Theory Library in Coq
我们描述了我们的经验，实现了广泛的范畴论库在Coq。范畴论和计算性能通常不会被相提并论，但我们需要大量的工程努力来教Coq处理大型范畴结构，而不会令人无法接受地减慢证明脚本处理。在本文中，我们分享了我们所学到的关于如何在Coq中表示非常抽象的数学对象和参数的经验教训，以及如何设计未来的证明助手来更好地支持这种推理。一个特殊的编码技巧，我们提请注意允许范畴理论的论点，涉及对偶性内在的柯克的逻辑与定义的平等。我们的可能是迄今为止最大的Coq开发，使用同伦类型理论家开发的相对较新的Coq版本，我们反思哪些新功能特别有用。
2014-04-18 cs.LO math.CT
Functionals in the Clouds: An abstract architecture of serverless Cloud-Native Apps
University of Siedlce（谢德林大学）
本文将云原生应用建模为可动态重配置的有向多重图，并以泛函和高阶类型理论刻画无服务器微服务的组合与运行时重构。
2025-07-22 cs.CL cs.LO
Generating induction principles and subterm relations for inductive types using MetaCoq
我们在MetaCoq中实现了三个关于归纳类型的Coq插件。第一个插件是一个简单的语法转换，通过抽象构造函数类型中的具体索引来生成归纳类型的替代构造函数。第二个插件在MetaCoq中重新实现Coq的$\texttt{Scheme Induction}$命令，并将其扩展到嵌套归纳类型，例如在其定义中使用$\texttt{list}$的玫瑰树等类型，类似于Tassi的Elpi插件。第三个插件实现MetaCoq中Equations包提供的$\texttt{Derive Subterm}$命令。
2020-06-25 cs.LO
MirrorShard: Proof by Computational Reflection with Verified Hints
我们描述了一种在Coq证明助手中构建可组合且可扩展的验证过程的方法。与依赖于运行时生成和检查证明的传统方法不同，我们使用经过验证的正确过程与Coq可靠性证明。虽然他们是内在的Coq的逻辑，我们的证明支持声音扩展用户提示新的领域，使自动推理用户定义的抽象谓词。我们通过开发一个用于模块化包装，构建和组成提示数据库的体系结构来保持稳健性，该体系结构以前仅在其动态类型化，证明生成策略语言的级别上在Coq中实现。我们的证明器还包括对统一变量的丰富处理，使其能够与Coq中其他基于策略的演绎步骤集成。我们已经实现了我们的技术，在反射验证的开源框架，XNUMX碎片。我们证明了它的适用性，通过实例化它的分离逻辑，以理由有关的强制性程序验证。
2013-05-28 cs.LO cs.PL
Towards a Coq-verified Chain of Esterel Semantics
本文利用 Coq 构建并验证 Esterel 的形式语义链，提出去除 Must/Can 势函数对的微步语义，并证明其对 CSS 的精化以及 CBS 与 CSS 的等价性。
2025-01-06 cs.FL cs.LO cs.PL
Certified Impossibility Results for Byzantine-Tolerant Mobile Robots
我们提出了一个框架，建立正式的发展，机器人网络使用COQ证明助手，状态和证明正式的各种属性。在本文中，我们专注于不可能性证明，因为利用COQ高阶微积分来推理算法作为抽象对象是很自然的。我们提出特别是正式证明两个不可能的结果forconvergence的不经意的移动机器人，如果分别超过一半和超过三分之一的机器人表现出拜占庭故障，从原来的定理Bouzid等人。由于我们的形式化，相应的COQ发展是相当紧凑的。据我们所知，这些是机器人网络的第一个认证（在正式证明的意义上）不可能性结果。
2013-06-18 cs.DC cs.LO
Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers
Aston University（阿斯顿大学）；Institute of Mathematics, Physics and Mechanics, Ljubljana（卢布尔雅那数学、物理与力学研究所）；Kyoto University（京都大学）
该研究基于先前工作，提出用于子集超空间认证计算的框架，先抽象定义通用空间子集，后针对波兰空间优化编码，引入连续性原理推导编码等价性，在 Coq 中实现理论并提取认证程序，还给出构造分形的应用。
2026-11-04 cs.LO
Realisability semantics of abstract focussing, formalised
我们提出了一个抽象的焦点，配备了证明条款的微积分：在传统的Zeilberger的工作，逻辑连接词和它们的介绍规则是作为一个参数的系统，它崩溃的同步和异步阶段的焦点作为宏观规则。我们进一步离开作为一个参数的操作，扩展了一个新的假设的背景下，这使我们能够捕捉经典和直观的聚焦微积分。然后，我们定义的可实现性语义（的证明）的系统，蒙奇-Maccagnoni的正交模型的基础上，经典的集中式微积分，但现在在更高的抽象层次上操作上述。在这个层次上，我们证明了一个引理，即如果一个项是A型的，那么在模型中它的外延是在A的（集合论）解释中。这表明了这样一个事实：取集合的正交时所涉及的全称量化在语义中反映了Zeilberger在异步阶段宏观规则中的全称量化。系统及其语义都在Coq中形式化。
2015-11-13 cs.LO
Computable analysis and notions of continuity in Coq
本文在 Coq 中基于 Incone 库形式化证明可计算分析中的多个定理，提供可执行算法并验证其正确性，同时比较不同连续性概念，贡献在于为连续结构上的算法推理提供通用接口。
2021-05-11 cs.LO
Formal Adventures in Convex and Conical Spaces
凸集出现在各种数学理论中，并用于定义凸函数和外壳等概念。作为一个抽象的通常定义的凸集在向量空间中，我们形式化Coq的一个内在公理化的凸集，即凸空间，基于一个操作采取重心的点。凸空间对应于不涉及周围向量空间的特定类型。这简化了函数的定义，我们展示了它的应用，包括定义在分布类型上的信息论函数的凸性。我们还展示了如何凸空间嵌入圆锥空间，这是抽象的实锥，并使用嵌入作为一种有效的设备，以方便计算。
2020-05-27 cs.LO
Initial Semantics for higher-order typed syntax in Coq
初始语义学旨在将与签名相关联的语法表征为某个类别的初始对象。我们提出了一个初步的语义结果类型的高阶语法连同其形式化的Coq证明助手。主要定理在2010年第二作者的博士论文中首次在纸上证明，并在不久后正式验证。对于固定的对象类型集合T上的简单类型绑定签名S，我们将一个称为S的表示范畴的范畴联系起来。我们证明了这个范畴有一个初始对象Sigma（S）。从它的构造中可以清楚地看出，对象Sigma（S）值得与S相关联的名称抽象语法。通过大量使用依赖类型，我们的定理在证明助手Coq中实现并证明了正确性。通过单子的方法产生了一种语法实现，其中术语和变量都是固有类型的，即对象类型反映在元级别类型中。这篇文章被看作是一篇研究文章，而不是关于一个经典数学结果的形式化。我们的定理的性质-涉及冗长，技术证明和复杂的代数结构-使它特别有趣的形式化验证。我们的目标是促进使用计算机定理证明器作为研究工具，并因此，一种新的方式出版的数学成果：一个平行的描述定理及其形式化应允许验证正确转录的定义和声明到证明助手，和简单，但技术证明应该很好地隐藏在一个数字图书馆。我们认为，科克的丰富的类型论，结合其各种功能，如隐式参数，允许一个特别可读的形式化，因此非常适合数学交流。
2011-09-17 cs.LO math.LO
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
证明助手经常调用自动定理证明器来证明子目标。然而，每个证明器都有自己的证明演算，它产生的证明轨迹往往缺乏许多细节来构建完整的证明。因此，这些痕迹很难检查和重用的证明助手。Dedukti是一个证明检查器，其证明可以翻译为各种证明助手：Coq，HOL，Lean，Matita，PVS。我们实现了一个工具，从TSTP文件中提取TPTP子问题，并使用能够生成Dedukti证明的自动证明器（如ZenonModulo或ArchSAT）在Dedukti中重建完整的证明。此工具是通用的：它不假设证明器产生跟踪的证明演算，并且它可以使用不同的证明器来产生Dedukti证明。我们将我们的工具应用于TPTP库的CNF问题上的自动定理证明器产生的痕迹，并且我们能够为其中的大部分重建证明，显着增加了可以为这些问题获得的Dedukti证明的数量。
2019-08-26 cs.LO
A Formal Algebraic Framework for DSL Composition
Two Six Technologies（图六科技公司）
我们讨论了一个正式的框架，使用代数结构建模的元语言，可以写，组成，并提供DSL的抽象之间的互操作性。这个形式化框架的目的是提供元语言的组合属性的验证。在我们的整个文件中，我们讨论了这个正式的框架的建设，以及它的关系，我们的团队的工作DARPA的V-SPELLS程序通过管道，我们已经开发完成我们的验证任务的V-SPELLS。我们的目标是在我们的论文中对这一核查管道进行广泛的概述。流水线可以分为四个主要部分：第一是在Coq中提供元语言的形式化模型;第二是在Coq中给出我们选择的代数结构的规范;第三，我们需要在Coq中实现我们的代数结构的特定实例，以及在Coq中证明这个实现是根据我们在第二步中的规范的代数结构;最后，我们需要在Coq中证明第一步中的元语言的形式模型是第三步中的实现的实例。
2023-02-01 cs.CL cs.LO cs.PL
An Abstract Domain for Heap Commutativity (Extended Version)
本文提出一种面向堆操作程序的抽象域，将具体堆程序的交换性验证转移到抽象数学模型上安全执行，并支持框架化与组合推理，已在 Coq 中完成机械化。
2024-11-25 cs.LO cs.PL
Type classes for efficient exact real arithmetic in Coq
Institute for Computing and Information Sciences Radboud University Nijmegen（拉德堡德大学计算与信息科学研究所）
本文通过类型类扩展了Coq中精确实数算术的实现，包括正弦余弦函数、基于快速有理数的稠密集实现、不可判定结构上的序层次以及运行时终止证明的避免，从而显著提升性能。
2013-02-13 cs.LO cs.NA math.NA
Implementing Open Call-by-Value (Extended Version)
按值调用演算的理论依赖于弱求值和闭项，这是程序设计语言研究中的自然假设。然而，对于模型证明助手，需要强有力的评估和开放的条款。开放式按值调用（Open call-by-value）是带开放项的弱求值的中间设置，在此之上，Grégoire和Leroy设计了Coq的抽象机。本文提出了一种开放式按值调用的抽象机理论。文献中包含的机器要么简单但效率低下，因为它们具有指数开销，要么高效但笨重，因为它们依赖于环境标签和技术优化。我们介绍了一种简单而高效的机器：它不使用标签，并且在双线性开销内实现了开放的按值调用。此外，我们提供了一个新的精细理解不同的优化如何影响开销的复杂性。
2017-02-01 cs.LO
Open Call-by-Value (Extended Version)
按值调用演算的优雅理论依赖于弱求值和封闭项，这是程序设计语言研究中的自然假设。然而，为了对证明助手进行建模，需要强求值和开放项，并且众所周知，在这种情况下，按值调用的操作语义会成为问题。在这里，我们研究中间设置-我们称之为Open Call-by-Value -具有开放项的弱求值，在此之上，Grégoire和Leroy设计了Coq的抽象机。开放式按值调用的各种演算已经存在，每一个都有它的优点和缺点。本文提出了一个详细的比较研究，其中四个操作语义，来自不同的领域，如抽象机的研究，指称语义，线性逻辑证明网，和逻辑演算。我们表明，这些演算都是等价的，从终止的角度来看，证明口号开放调用的价值。
2016-09-19 cs.LO
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
本文描述了离散实闭域在Coq证明助手中的形式化。这个抽象的结构捕捉例如实代数数的理论，一个具有良好算法性质的实数的可判定子集。实代数数和更一般的半代数簇的理论是实分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，根据计算机代数中关于量词消去的标准文献，给出了一个基于伪余项序列的代数证明的形式化.这种形式化涵盖了理论的很大一部分，这是在计算机代数实践中实现的有效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。
2012-02-15 cs.LO
A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
在本文中，我们提出了一个形式化的Kozen的命题模态$μ$ -演算，在演算的归纳结构。我们解决了几个有问题的问题，如使用高阶抽象语法在归纳集合中存在的递归构造器，编码的模态（“证明”）规则和上下文敏感的语法。该编码可用于\Coq系统中，为$μ$ -演算中的无错证明的交互式开发提供了一个实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到其他语言和证明系统具有类似的问题。
1998-09-29 cs.LO
Inductive types in homotopy type theory
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
2012-05-02 cs.LO math.CT math.LO
A weak HOAS approach to the POPLmark Challenge
利用以前的编码和形式化发展的名义演算和类型系统，我们提出了一个弱高阶抽象形式化的类型语言的纯系统F<：在Coq，一个证明助手的基础上演算的归纳结构。我们的编码使我们能够完成算法子类型的传递性属性的证明，这实际上是POPLmark挑战所述的三项任务中的第一项，POPLmark挑战是一组问题，这些问题捕获了形式化程序设计语言元理论中最关键的问题。
2013-03-29 cs.LO cs.PL
Extended Initiality for Typed Abstract Syntax
初始语义学的目标是将与签名相关联的语法解释为某类“模型”的初始对象，为抽象语法产生归纳和递归原则。Zavió证明了一个简单类型语法的初始性结果：给定一个签名S，与S相关联的抽象语法构成了单子中S的模型范畴中的初始对象。然而，她的定理提供的迭代原则只考虑了在一组固定的对象类型上的两种语言之间的翻译。我们推广Zavió的模型概念，使对象类型可以变化，产生一个更大的类别，同时保持其中语法的初始性。因此，我们得到了一个扩展的初始性定理的类型化抽象语法，在不同类型的条款之间的翻译可以指定通过相关的范畴理论的迭代算子作为一个初始态射。我们的定义确保通过初始化指定的翻译是类型安全的，即在明显的意义上与源语言和目标语言中的类型兼容。我们的主要例子是通过命题作为类型的范例：我们指定命题和推理规则的经典和直觉命题逻辑通过各自的类型签名。然后，我们使用范畴论的迭代算子指定一个双重否定翻译从前者到后者。第二个例子是PCF的签名。对于这种特殊情况，我们在证明助手Coq中将定理形式化。然后，我们指定，通过范畴理论的迭代运算符，从PCF的无类型的λ演算的翻译。
2012-04-05 cs.LO cs.PL
An Analysis of Tennenbaum's Theorem in Constructive Type Theory
本文在构造性类型论框架下重新分析并推广Tennenbaum定理，通过Church论题内部化可计算性论证，构造化多个经典证明并给出内在构造性表述，揭示经典视角下不可见的假设与结论差异，并完成Coq机械化。
2024-03-06 cs.LO math.LO
Mechanised Hypersafety Proofs about Structured Data: Extended Version
本文提出 Hoare 风格关系分离逻辑 LGTM，将结构化数据操作规范为参数化超安全性，并在 Coq 中机械化其理论与策略，验证了13个压缩数组和稀疏张量案例。
2024-04-09 cs.LO cs.PL
A Formal Disproof of the Hirsch Conjecture
本文对Santos等人关于多面体（有界凸多面体）直径的Hirsch猜想的一个反例进行了形式化验证。与纸笔证明相比，我们的方法是完全计算：我们实现在Coq和证明正确的算法，明确计算，在证明助手，顶点边缘图的多面体以及它们的直径。这种基于证书的算法的独创性是实现简单性和效率之间的权衡。简单性是获得算法正确性证明的关键。这种证明分为面向证明的数据类型上的抽象算法的正确性和面向计算的数据类型上的低级实现的对应性。已经做出了特别的努力来将算法减少到小的基本操作序列（例如，矩阵乘法，集合和图形上的基本例程），以便使低级实现的正确性的推导更加透明。效率使我们能够扩展到具有挑战性的组合多面体。例如，我们正式检查的两个反例的Matschke，桑托斯和韦伯的赫希猜想，分别为20和23维多面体与36 425和73 224顶点涉及有理系数高达40位数的分子和分母。我们还说明了该方法的性能，通过计算的顶点或直径的著名类的多面体，如（极）循环多面体中涉及的McMullen的上限定理。
2023-01-10 cs.LO math.CO math.OC
Multi-Stage Programs are Generalized Arrows
受类型限制的λ演算提供了一种用于carbohydrate闭范畴的内部语言的语法。本文建立了一个平行的结果：分期注释，受命名水平的限制，提供了一个语法的内部语言的Freyd类别，这是已知的双射对应箭头。这种联系是通过将多级类型系统解释为从多项式范畴到其重索引的索引函子来实现的。这个结果只适用于多阶段语言，这些语言是（1）同构的，（2）允许跨阶段持久化，（3）在类型化派生中对结构规则的使用没有限制。移除这些限制并重复构造会产生广义箭头，其中Arrow是一种特殊情况。提供了从良好类型的多阶段程序到单阶段Garrow术语的翻译。翻译是由归纳法定义的结构证明，多阶段程序是良好类型的，依赖于信息编码的证明中使用的结构规则。元语言设计者现在可以通过提供从分级语法到广义箭头类型表达式的单一翻译来分解元编程的语法机制。对象语言提供程序只需要以无点样式实现通用箭头类型类的函数。对象语言的使用者可以在这些对象语言上以点式的风格编写元程序，在对象语言和元语言中使用相同的绑定、作用域、抽象和应用机制。本文的主要贡献是图2和图3的Garrow定义，图5中的翻译和定义16的范畴理论语义。伴随的Coq证明形式化了类型系统，翻译过程和关键定理。
2010-09-30 cs.LO cs.PL math.CT
