Formal verification in Coq of program properties involving the global state effect
一个命令式语言的语法没有明确提到的状态，而它的指称语义必须提到它。在本文中，我们提出了一个框架，在Coq的性质的程序操纵全局状态效果的验证。这些性质用一个证明系统来表达，这个证明系统与语法接近，就像在有效系统中一样，在这个意义上，状态并不显式地出现在操纵它的表达式类型中，而是通过添加到项和方程中的装饰来出现。在这个系统中，程序的证明因此呈现两个方面：性质可以被验证{ \em直到效果}或者效果可以被考虑。因此，我们的Coq库的设计反映了这两个方面：我们的框架围绕着两个归纳和依赖类型的构建，一个用于效果的术语，另一个用于装饰的操作。
2013-10-14 cs.LO cs.PL
Cubical Syntax for Reflection-Free Extensional Equality
我们贡献XTT，观察类型论的立体重建，扩展马丁-洛夫的内涵类型论与依赖的平等类型，享有功能扩展性和判断版本的唯一性的身份类型原则（UIP）：任何两个元素相同的平等类型是判断平等的。此外，我们推测，类型关系可以决定在一个实用的方式。在本文中，我们建立了一个代数规范性定理，使用一个新的立方扩展（独立提出的Awodey）的逻辑家庭或范畴胶合参数的启发Coquand和Shulman：每一个封闭的布尔类型的元素是可导等于要么“真”或“假”。
2019-06-06 cs.LO math.LO
DBGen User Manual
DBGen是Coq开发人员的工具。它将带有绑定注释的术语结构的定义作为输入，并在De Bruijn设置中生成用于提升和替换的定义和属性，直到替换引理。它还提供了一个命名语法和一个到De Bruijn语法的翻译函数。
2012-12-02 cs.LO
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
我们描述了在Coq证明助手中嵌入QWIRE量子电路语言。这允许程序员使用高级抽象来编写量子电路，并使用Coq的定理证明功能来证明这些电路的属性。该实现使用高阶抽象语法来表示变量绑定，并为线性导线类型提供类型检查算法，确保量子电路是良构的。我们形式化了一个指称语义，将QWIRE电路解释为密度矩阵上的超算子，并证明了一些简单量子程序的正确性。
2018-03-02 cs.ET cs.LO cs.PL
Characteristics of de Bruijn's early proof checker Automath
本文聚焦de Bruijn早期证明检查器Automath的句法背景与不常见方面，提出一个封装最常见版本的通用Automath系统，并以现代句法框架呈现，该系统基于CC的扩展λD。
2022-06-15 cs.LO math.LO
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
一个新的，全面的方法来解决居住问题的简单类型的λ演算，处理决策和计数问题。这种方法的工作原理是利用一个表示的搜索空间所产生的一个给定的居住问题，这是在一个证明搜索，作者最近开发的微积分。这种表示可以被看作是通过类元项扩展证明的Curry-Howard表示，保持在λ演算和类型系统的方法内。我们的方法揭示了归纳描述的决策问题，由证明搜索表达式的语法驱动，最终产品是简单的，递归的决策程序和计数功能。
2017-03-11 cs.LO math.LO
Mechanizing Matching Logic In Coq
匹配逻辑是使用模式和模式匹配来指定和推理数学结构的形式体系。它越来越流行，已被用来定义许多逻辑系统，如具有递归定义的分离逻辑和线性时态逻辑。此外，它还作为K语义框架的逻辑基础，该框架用于为许多现实世界的语言构建实用的验证器。尽管匹配逻辑是一个容纳大量理论的基本形式系统，但它缺乏通用的、机器检查的形式化。因此，我们使用Coq证明助手来形式化匹配逻辑。具体来说，我们创建了一个新的表示匹配逻辑，使用本地无名编码，我们正式的语法，语义和证明系统，这种表示在Coq证明助手。最重要的是，我们证明了形式化证明系统的可靠性，并提供了一种在Coq中进行交互式匹配逻辑推理的方法。我们相信这项工作提供了一个以前未探索的途径推理匹配逻辑，其模型和证明系统。
2022-09-21 cs.LO
Initial Semantics for Reduction Rules
本文通过范畴论中的初始对象性质，为带有归约规则的简单类型语言（如PCF）提供了代数语义刻画，并利用该性质构造了从PCF到无类型lambda演算的语义忠实翻译。
2019-03-20 cs.LO math.LO
Abstract clones for abstract syntax
本文提出用带额外代数结构的 abstract clones 公理化简单类型理论的二阶变量绑定算子，构造自由代数并导出归纳原理，从而支持独立于语法的可靠性与规范化证明。
2021-05-03 cs.LO cs.PL
On the Expressive Power of Schemes
本文提出贴近自然演绎证明语法、且不为假设命名的 scheme-calculus，并证明部分带类型版本虽具非确定性，仍与相应带类型 λ-calculus 表达能力相同。
2023-04-24 cs.LO
MirrorShard: Proof by Computational Reflection with Verified Hints
我们描述了一种在Coq证明助手中构建可组合且可扩展的验证过程的方法。与依赖于运行时生成和检查证明的传统方法不同，我们使用经过验证的正确过程与Coq可靠性证明。虽然他们是内在的Coq的逻辑，我们的证明支持声音扩展用户提示新的领域，使自动推理用户定义的抽象谓词。我们通过开发一个用于模块化包装，构建和组成提示数据库的体系结构来保持稳健性，该体系结构以前仅在其动态类型化，证明生成策略语言的级别上在Coq中实现。我们的证明器还包括对统一变量的丰富处理，使其能够与Coq中其他基于策略的演绎步骤集成。我们已经实现了我们的技术，在反射验证的开源框架，XNUMX碎片。我们证明了它的适用性，通过实例化它的分离逻辑，以理由有关的强制性程序验证。
2013-05-28 cs.LO cs.PL
Typed compositional quantum computation with lenses
Nagoya University（名古屋大学）
本文提出一种基于类型理论的框架，用于描述和证明量子计算的性质，特别是以量子电路形式呈现的计算。通过引入离散的透镜概念，将电路结构的组合学与门操作的计算内容分离，并递归定义量子电路并证明其正确性。
2026-05-11 cs.LO cs.PL
Towards an induction principle for nested data types
针对嵌套数据类型难以推导归纳原理的问题，本文引入依赖类型折叠，并以Bush为例展示推导过程，同时探讨其与传统高阶折叠的关系。
2023-06-16 cs.LO cs.PL
The Delta-calculus: syntax and types
我们提出了Delta演算，一个显式类型的Delta-calculus强对，投影和显式类型的Delta-calculus。演算可以用不同的交集类型论T参数化，例如Coppo-Dezani、Coppo-Dezani-Salle '、Coppo-Dezani-Venneri和Barendregt-Coppo-Dezani理论，产生具有相关交集类型系统的Delta-演算族。我们证明了它的主要性质，如Church-Rosser，类型唯一性，主题约简，强规范化，类型检查和类型重构的可判定性。本文通过一个将显式Delta项转换为纯Delta项的本质函数，说明了Curry型交集型赋值系统与Church型交集型赋值系统之间的关系.最后，我们将一个带类型子的Delta项翻译成一个不带类型子的Delta项，证明了这种翻译是连贯的，因为它的本质是恒等式。一般的Delta演算可以被参数化，以考虑其他的交集类型论，如Barendregt等人的书中的理论。
2019-02-25 cs.LO
Syntax and Typing for Cedille Core
本文档指定了Cedille工具中实现的类型论的核心版本。Cedille是一种用于依赖类型编程和计算机检查证明的语言。Cedille可以将源程序细化到Cedille核心，可以通过一个小检查器以简单的方式检查（Cedille包含的参考实现不到1000行Haskell）。其他工具也可以将CedilleCore作为一个富有表现力的后端类型论。该文档描述了Cedille Core的语法和类型规则。
2018-11-04 cs.LO cs.PL
Logic of Combinatory Logic
我们开发了一个经典的命题逻辑推理组合逻辑。我们定义了它的语法、公理系统和语义。以经典命题逻辑为基础，以类型化组合项为基本命题，给出了其语法和公理系统，并给出了其语义，该语义基于扩展了与原始组合子相对应的特殊元素的应用结构。无类型组合逻辑的方程理论和所提出的公理系统都被证明是正确和完整的。给出的语义。此外，我们证明了组合逻辑是可靠的和完备的w.r.t.给出的语义。
2022-12-13 cs.LO math.LO
Full Abstraction for a Recursively Typed Lambda Calculus with Parallel Conditional
我们定义了一个递归类型的λ演算的语法和约简关系，并给出了一个并行的条件函数。减少显示为融合性。我们将递归类型解释为受限形式的信息系统，我们称之为素系统。一个指称语义定义与此解释。定义了项的语法范式逼近，证明了逼近定理：项的语义等于其逼近的语义的极限。证明使用包含谓词（逻辑关系）。对于布尔值的观察，语义是足够的。在平行格功能的存在下，它也是完全抽象的。
2008-06-11 cs.LO
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
在约简证明搜索中，证明自然地被解广义化，包括由局部正确的、自底向上的推理规则应用生成的所有可能的无限结构。我们提出了一个扩展的库里-霍华德范式的代表性，从证明到解决方案：代表解决方案可能是无限项的一个专用的微积分。这种新的，全面的方法证明搜索的例子与直觉蕴涵逻辑的演算LJT。提出了一种有限表示法，它包括用一个形式最大不动点扩展的类项，以及一个可以看作是共归纳证明逻辑的类型系统。在有穷系统中，定点变量享有宽松的绑定形式，允许通过类型系统检测循环。在搜索过程中，形式和用于表示备选项。此外，正式总和中使用的共归纳语法来定义“decontraction”（自下而上的收缩）-一个操作的理论，我们在本文中启动。作为一种语义，我们分配一个共归纳项到每个有限项。主要结果是存在一个等价的有限表示的任何完整的解决方案空间表示共归纳。这一结果是证明我们的共归纳证明逻辑在共归纳语义上是健全和完备的主要因素。这些结果是证明搜索的原始方法的基础，其中搜索建立了完整解空间的有限表示，并且后验分析通常包括应用语法指导的过程或函数。本文说明了这一点证明搜索和居住问题的简单类型的Alzada演算，审查结果详细其他地方，并包括新的结果，获得广泛的推广所谓的单原子定理。
2021-07-29 cs.LO math.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
The Dependently Typed Higher-Order Form for the TPTP World
本文提出TPTP语言的依赖类型高阶形式DTF，作为对THF的最小侵入性扩展，并提供超100个问题集及现有工具支持以展示其价值。
2025-07-03 cs.LO
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
FU Berlin（柏林自由大学）；University Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）；University Bamberg（班贝格大学）
本文引入了HOL的依存类型扩展DHOL，保留了HOL的风格与概念框架，并构建从DHOL到HOL的翻译作为HOL定理证明器的前置预处理器，从而实现DHOL的定理证明。
2023-05-24 cs.AI cs.FL cs.LO
On a Dependently Typed Encoding of Matching Logic
本文提出匹配μ-逻辑的首个依值类型定义，通过类型索引编码排序上下文确保良排序性，使不良排序语法不可表示且良排序元素语义保证在关联排序域内。
2025-09-16 cs.LO
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
我们研究了一类简单类型的λ演算的名义代数Henkin式模型，其中变量映射到表示中的名称，而λ演算抽象映射到（非功能性的）名称抽象操作。由此产生的表示更小，更好的行为，在我们精确的方式，比基于函数值的模型。使用这些新的模型，我们然后开发了一个概括的λ-长期语法丰富他们的存在元变量，从而产生一个理论的不完整的功能。这种不完备性与函数抽象和应用给出的不完备性的通常概念是正交的，并且对应于洞和不完备对象。
2011-11-01 cs.LO cs.PL
Learning to Prove Theorems via Interacting with Proof Assistants
Princeton University（普林斯顿大学）
人类通过大量的高级推理和特定问题的见解来证明定理。证明助手提供了一种类似于人类数学推理的形式主义，将高阶逻辑中的定理和证明表示为高级策略。然而，人类专家必须通过将策略输入到证明助手中来手动构造证明。在本文中，我们研究的问题，使用机器学习自动化的互动与证明助手。我们构建了CoqGym，这是一个大规模的数据集和学习环境，包含来自Coq证明助手开发的123个项目的71K人类书面证明。我们开发了ASTactic，这是一种基于深度学习的模型，可以以抽象语法树（AST）的形式生成策略作为程序。实验表明，在CoqGym上训练的ASTactic可以生成有效的策略，并可用于证明以前无法通过自动方法证明的新定理。代码可在https://github.com/princeton-vl/CoqGym上获得。
2019-05-21 cs.AI cs.LG cs.LO
Touring the MetaCoq Project (Invited Paper)
证明助手在研究和工业中得到越来越广泛的使用，以提供关于理论、设计、系统和实现的经认证的和可独立检查的保证。然而，证明助手实现本身很少被验证，尽管它们在任何此类认证工作中占据了受信任代码库的主要份额。在这一领域，基于高阶逻辑的证明助手享有更强的保证，因为自认证实现已经有几年了。这种差异的一个原因是依赖类型论的内在复杂性，以及它们与归纳类型、论域多态性和复杂排序系统的扩展，以及理论与高效程序设计语言的实际实现之间的差距。MetaCoq是一个合作项目，旨在解决这些困难，为Coq证明助手底层的完整演算提供第一个经过完全认证的类型检查器的真实实现。为了实现这一点，我们改进了有时模糊的，如果不是不正确的，系统的规范和实现。我们展示了这个社区的理论工具，如双向类型检查，Tait-Martin-Löf/Takahashi的汇合证明技术和monadic和依赖类型编程，可以帮助构建以下工件：Coq的语法和类型论的规范，（Co）-归纳构造的多态累积演算（PCUIC）;用于操纵原始语法和与Coq系统交互的monad;对PCUIC的元理论的验证，其主要结果是归约、类型保持和类型原则的融合，PCUIC的一个真实、正确和完整的类型检查器，从PCUIC到无类型的类型演算的一个可靠的类型和证明擦除过程，即，辅酶Q提取机理的核心。
2021-07-16 cs.LO cs.PL
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
1flonatel GmbH \& Co. KG, Aachen, Germany
本文构建了一个源自超一万个 Coq 源文件的综合数据集，用于训练 LLMs 生成 Coq 代码，实验表明微调模型可为一个引理生成 141 个有效证明，推动了自动定理证明的发展。
2024-04-02 cs.AI cs.LO
Syntax Monads for the Working Formal Metatheorist
针对原始一阶语法表示缺乏范畴论支撑导致基础引理难复用的问题，本文提出Coq框架Tealeaves的核心抽象装饰可遍历单子的弦图解释，证明其表示定理并得到有穷树状数据类型递归组合子。
2023-12-14 cs.LO cs.PL
Bicategorical type theory: semantics and syntax
本文为双范畴类型论建立语义（理解双范畴）与语法（判断与推理规则），证明规则可靠性，并在Coq中形式化验证语义。
2023-10-12 cs.LO math.CT
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
我们描述了一种方法来验证实现的转换功能的程序，利用高阶表示的语法。在这种方法中，使用遗传Harrop公式的逻辑指定变换。一方面，这些规范直接作为实现，是Lambda Prolog语言中的程序。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。我们认为，这种方法是特别有效的实现转换，分析绑定结构。我们通过在Lambda Prolog中描述对这种结构敏感的类型化闭包转换和代码提升等转换的简洁编码，并通过展示如何使用Abella证明其正确性来做到这一点。
2016-01-23 cs.LO cs.PL
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
本文从范畴和代数的角度研究了类型化λ演算的赋值正规化问题。本文的第一部分通过Kripke逻辑关系分析了Jung和Tiuryn的lambda可定义性结果，并展示了它如何适用于统一可定义性和规范化，产生一个扩展的规范化结果。在第二部分的文件的分析进一步细化考虑内涵Kripke关系（在阿丁胶合的形式），并显示提供一个功能的规范化条款，铸造规范化的范畴胶合的背景下进行评估。技术发展包括类型化λ演算的语法和语义的代数处理，其允许在简单类型化元理论内给出规范化函数的定义。合成依赖类型的函数式程序设计语言中的求值规范化程序。
2022-08-18 cs.LO math.CT
Nexus Authorization Logic (NAL): Logical Results
Nexus授权逻辑（NAL）[Schneider et al. 2011]是一种用于分布式系统中授权推理的逻辑。NAL的修订版本在这里，包括修订后的语法，修改后的证明理论，使用本地化的假设，和一个新的Kripke语义。证明理论被证明是健全的语义方面，证明是形式化的Coq。
2012-11-16 cs.CR cs.LO
Bidirectional Elaborators à la Carte
University of Cambridge（剑桥大学）
研究证明助手中表层语法隐含问题，引入依赖类型单子领域特定语言，通过浅嵌入表示双向类型表层语言，实现正确转换，提取具体精细化算法，提升语法处理可靠性与可预测性。
2026-10-16 cs.LO cs.PL
Modules over relative monads for syntax and semantics
我们给出了一类变量绑定语言的语法和语义的代数刻画。我们引入了一个2-签名的概念：这样的签名不仅指定了语言的术语，而且还指定了这些术语的归约规则。对于任何2-签名$S$，我们关联$S$的“模型”类别。这个范畴有一个初始对象，它整合了由$S$自由生成的项，并配备了根据$S$中给出的不等式的约简。我们将这个初始对象称为由$S$生成的语言。2-签名的模型是从相对单子和这些单子上的模块构建的。通过使用单子，模型-特别是初始模型-配备了一个替换操作，该操作在适当的意义上与归约兼容。初始性定理在证明助手Coq中被形式化，产生一种机器，当被馈送2-签名时，该机器为相关的程序设计语言提供约简关系和经认证的替换。
2013-11-19 cs.LO cs.PL
Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
Budapest University of Technology and Economics（布达佩斯技术与经济大学）
该研究提出带希尔伯特ε算子的直觉主义内涵一阶逻辑的类型化证明项演算，证明其关于特定超教义模型的可靠性与完备性，相关成果在Rocq中形式化。
2026-10-14 cs.LO math.CT math.LO
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
2023-05-25 cs.LO
Sequent Calculus and Equational Programming
基于类型论的证明助手和程序设计语言通常有两种风格：一种是基于类型论的标准自然演绎表示，并涉及消除器，而另一种是提供等式风格的语法。我们在这里表明，方程的方法对应于使用一个集中的介绍类型论表示为微积分。一个类型化的函数语言，基于一个代数演算，我们涉及到的语法和内部语言的Agda。特别是，我们讨论了使用的模式和情况下分裂，以及规则实现归纳推理和相关产品和总和。
2015-07-29 cs.LO
Modal Dependent Type Theory and Dependent Right Adjoints
近年来，我们已经看到了几个新的模型，依赖类型论扩展了某种形式的模态必要性算子，包括名义类型论，守卫和时钟类型论，空间和凝聚类型论。在本文中，我们研究模态依赖类型论：依赖类型论与运营商满足（依赖版本）的K公理的模态逻辑。我们研究语义和语法。对于语义，我们引入了具有依赖右伴随（Cwandom）的家族的类别，并表明上面的例子可以这样呈现。事实上，我们表明，任何有限的极限范畴的附加endofunctors引起的Cwerk通过当地的宇宙建设。对于语法，我们引入了一个依赖类型的扩展的Fitch风格的模态的Bunda演算，表明它可以在任何Cwetches解释，并建立一个长期的模型。我们扩展的语法和语义与宇宙。
2019-07-25 cs.LO
Homotopy Type Theory in Isabelle
本文介绍了Isabelle/HoTT，同伦类型论的第一个发展Isabelle证明助手。在Paulson早期工作的基础上，我使用Isabelle现有的逻辑框架基础设施来实现基本的自动化，例如类型检查和术语细化，这通常是在依赖类型系统的源代码级别上处理的。我还集成了命题作为类型的范式与声明性的Isar证明语言，提供了一种替代的Coq和Agda的证明条款的基于策略的证明。基础设施开发，然后用于形式化的同伦类型论书的基础结果。
2021-04-19 cs.LO
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
本文利用预层模型和余单子 $\ lat$ 刻画 Cocon 的上下文类型语义，并借助带族范畴将其扩展到依赖类型。
2022-06-08 cs.LO cs.PL
A weak HOAS approach to the POPLmark Challenge
利用以前的编码和形式化发展的名义演算和类型系统，我们提出了一个弱高阶抽象形式化的类型语言的纯系统F<：在Coq，一个证明助手的基础上演算的归纳结构。我们的编码使我们能够完成算法子类型的传递性属性的证明，这实际上是POPLmark挑战所述的三项任务中的第一项，POPLmark挑战是一组问题，这些问题捕获了形式化程序设计语言元理论中最关键的问题。
2013-03-29 cs.LO cs.PL
Algebraic models of simple type theories: a polynomial approach
我们开发简单的类型论的代数模型，奠定了一个框架，扩展通用代数，将代数排序和变量绑定。简单类型论的例子包括单位类型和简单类型的$λ$ -演算、计算$λ$ -演算和谓词逻辑。简单类型论是在预层范畴中给出的模型，其结构由对应于自然演绎规则的多项式内函子的代数指定。我们构建的初始模型抽象地描述了简单类型论的语法。考虑到替换结构，我们进一步提供了结构化carbohydrate多范畴的声音和完整的语义。这一发展概括了Lambek的对应关系之间的简单类型$λ$演算和笛卡尔闭范畴，任意简单的类型论。
2020-06-30 cs.LO math.CT
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Freie Universität Berlin（柏林自由大学）；Vienna University of Technology（维也纳技术大学）
哥德尔的本体论证明已经分析了第一次与前所未有的详细程度和形式的帮助下，高阶定理证明。以下是已经完成的（并按此顺序）：一个详细的自然演绎证明。TPTP THF语法中公理、定义和定理的形式化。使用Nitpick自动验证公理和定义的一致性。自动证明定理与证明LEO-II和Satallax。使用Coq证明助手的逐步形式化。使用Isabelle证明助手的形式化，其中定理（和一些额外的引理）已使用Sledgehammer和Metis自动化。
2017-09-03 cs.AI cs.LO math.LO
A Natural Deduction style proof system for propositional $μ$-calculus and its formalization in inductive type theories
在本文中，我们提出了一个形式化的Kozen的命题模态$μ$ -演算，在演算的归纳结构。我们解决了几个有问题的问题，如使用高阶抽象语法在归纳集合中存在的递归构造器，编码的模态（“证明”）规则和上下文敏感的语法。该编码可用于\Coq系统中，为$μ$ -演算中的无错证明的交互式开发提供了一个实验性的计算机辅助证明环境。我们采用的技术可以很容易地移植到其他语言和证明系统具有类似的问题。
1998-09-29 cs.LO
A Case Study on Logical Relations using Contextual Types
逻辑关系证明在建立诸如规范化或上下文等价等丰富的性质方面起着关键作用。机械化也很有挑战性。在本文中，我们描述了算法的完整性证明的简单类型的Algida-条款的Crary，我们的原因在逻辑上等价的条款在证明环境白鲸。有三个关键方面，我们依赖于：1）我们编码与他们的操作语义和使用高阶抽象语法的算法等式一起，2）我们直接使用递归类型和高阶函数编码相应的逻辑等价的良好类型的与条件3）我们利用Beluga的支持上下文和等式理论的同时替代。这导致了一个直接和紧凑的机械化，展示了Beluga在形式化逻辑关系证明方面的实力。
2015-07-29 cs.LO cs.PL
A Type Checker for a Logical Framework with Union and Intersection Types
我们提出的语法，语义和类型规则的公牛，一个原型定理证明的基础上的三角洲框架，即一个完全类型化的Alkida演算装饰与工会和交叉类型，如作者在以前的论文中所描述的。Bull还实现了Barbanera-Dezani-de'Liguoro的类型论Xi的子类型算法。Bull有一个命令行界面，用户可以在其中声明公理，术语，并执行计算和一些基本的终端风格的功能，如错误漂亮打印，子表达式突出显示和文件加载。此外，它可以对证明进行类型检查或规范化，这些项可能是不完整的，因此类型检查算法使用统一来尝试构建缺失的子项。Bull使用Berardi的纯类型系统的语法来提高内核的紧凑性和模块性。抽象语法和具体语法基本上是一致的，并且与Coq的具体语法相似。Bull对术语使用高阶统一算法，而类型检查和部分类型推断是通过双向细化算法完成的，类似于Matita和Beluga中发现的算法。精化可以分为两个部分：本质精化和类型精化。绑定器使用常用的de Bruijn索引实现。我们已经定义了一个具体的语言语法，允许用户编写Delta-terms。我们已经定义了约简规则和评价器。我们从头开始实现了一个细化器，它可以进行部分类型检查和类型重构。我们已经实验了公牛经典的例子的交集和工会的文学，如形式化的Pfenning与他的细化类型在LF。我们希望，这种研究静脉可能是有用的实验，在证明理论的设置，形式的多态性替代吉拉德的参数…
2020-02-25 cs.LO cs.PL
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
ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
School of Information Science, Beijing Language and Culture University（北京语言文化大学信息科学学院）
提出ZX-演算，通过迹索引类型、预层非单调语义和构造性AGM信念修正，保守扩展Martin-Löf依赖类型论，并给出Coq机械化证明。
2026-06-02 cs.CL cs.LO
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
基于具有更高类型量化的直觉或线性逻辑的逻辑框架已成功地用于对程序设计语言和推理系统领域中的许多重要判断给出高级、模块化和形式化的规范。给定这样的规范，考虑证明框架中指定系统的属性是很自然的：例如，给定函数式程序设计语言的求值规范，证明该语言是确定性的或求值保留类型。开发这种推理框架的一个挑战是高阶抽象语法（HOAS），一种优雅的和声明性的对象级抽象和替换处理，很难在涉及归纳的证明中处理。在本文中，我们提出了一个元逻辑，可用于推理使用HOAS编码的判断，这个元逻辑是一个简单的直觉主义逻辑，承认高阶量化简单类型的非线性项（HOAS的关键成分），以及归纳和定义的概念的扩展。我们通过考虑直觉和线性逻辑的编码，探讨了HOAS编码的形式元理论分析的困难，并正式推导出这些逻辑的重要子集的割的容许性。然后，我们提出了一种方法，以避免高阶抽象语法的好处和分析所产生的编码的能力之间的明显的权衡。我们通过涉及简单函数式和命令式程序设计语言PCF和PCF：=的示例来说明这种方法。我们正式推导出这样的属性，作为唯一性的类型，主题减少，确定性的评价，和等价的过渡语义和自然语义表示的评价。
2001-01-15 cs.LO cs.PL
Two tricks to trivialize higher-indexed families
本文提出利用 Fording 和小宇宙索引两种技巧，将依赖类型论中具有高阶归纳索引的复杂索引族编码为无索引归纳类型与单一大型类型族，从而将其平凡化。
2023-10-30 cs.LO
A Formal Proof of the Strong Normalization Theorem for System T in Agda
我们提出了一个框架的正式元理论的lambda演算在一阶语法，有两种名称，一个代表自由和绑定变量，和其他常量，并通过使用斯托顿的多重替换。在这个框架之上，我们形式化了Girard对简单类型λ演算和系统T的强规范化定理的证明。对于后者，我们也提出了一个简化的原始证明。整个开发过程都使用Agda系统进行了机器检查。
2023-03-23 cs.LO
The Functional Machine Calculus II: Semantics
作者最近引入的函数机器演算（FMC）是拉姆达演算的推广，它可以忠实地编码高阶可变存储、I/O和概率/非确定性输入的影响。值得注意的是，它仍然是融合的，并且可以在这些效果存在的情况下简单地类型化。在本文中，我们探讨的指称语义的FMC。我们有三个主要的贡献：首先，我们认为，它的语法-在这两个效果，并实现使用相同的句法结构-是语义自然，密切对应的结构斯科特风格的域理论语义。第二，我们表明，简单的类型赋予强规范化扩展甘迪的证明，包括一个小的简化的技术。最后，我们表明，类型FMC（不考虑具体的编码效果），模适当的方程理论，是一个完整的语言笛卡尔闭范畴。
2023-02-05 cs.LO cs.PL
Natural Deduction as Higher-Order Resolution
一个交互式定理证明程序Isabelle正在开发中。在LCF中，每个推理规则由一个用于向前证明的函数和另一个用于向后证明的函数（一种策略）表示。在Isabelle中，每个推理规则由Horn子句表示。解析给出了向前和向后的证明，支持一大类逻辑。伊莎贝尔被用来证明马丁-洛夫的构造性类型论中的定理。量词构成了几个困难：替代，约束变量，Skolemization。Isabelle的逻辑语法表示是类型化的微积分，需要更高阶的统一。它可能具有逻辑编程的潜力。沿着推理规则的深度优先子目标构成高阶Prolog。
2000-10-31 cs.LO
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
高阶并发语言的更精确的正确性证明是困难的：它们涉及到在并发的高级源语言和使用低级共享内存原语的实现之间建立一个保持终止的精化。然而，现有的逻辑证明并发加细要么忽略属性，如终止，或只处理一阶状态。在本文中，我们解决这些限制，扩展虹膜，最近的高阶并发分离逻辑，支持终止保留的细化推理。为了证明这些扩展的功能，我们证明了一个高阶，会话类型的语言的有效实现的正确性。据我们所知，这是第一个能够为这种语言提供编译器正确性证明的程序逻辑。我们的扩展和我们的编译器正确性证明的合理性已经在Coq中机械化。
2017-01-20 cs.LO cs.PL
Dependent Pearl: Normalization by realizability
对于我们这些通常生活在语法世界中的人来说，语义证明技术，如还原性，可实现性或逻辑关系，似乎有点神奇，尽管-或者可能是由于-它们似乎不合理的有效性。它们为什么有效？在证明中的哪一点是“真正的工作”完成了？希望建立一个编程的直觉，这些证明，我们实现了一个规范化的参数，简单类型的Alzida演算与总和：而不是一个证明，它被描述为一个程序中的依赖类型的元语言。我们着手研究的语义技术是Krivine的经典可实现性，它相当于一个证明相关的介绍还原参数-一元逻辑关系。可归约性为每种类型分配一个谓词，可实现性分配一组实现器，它们是用第一类上下文概念扩展可归约项的抽象机器。规范化是充分性定理或“基本引理”的直接结果，它指出任何类型良好的项都可以转换为其类型的实现器。我们表明，充分性定理，作为一个依赖的程序编写时，对应于一个评估过程。特别地，弱规范化证明精确地计算从输入项到范式的一系列约简。有趣的是，我们在定义归约谓词时所做的选择--每个连接词的真和假见证--决定了证明的求值顺序，每个数据类型构造函数以懒惰或严格的方式运行。虽然本演示文稿中的大多数想法都是专家之间的民间传说，但我们的依赖型函数程序为更广泛的受众提供了一个可访问的演示文稿。特别是，我们的工作提供了一个温和的介绍抽象的机器演算最近被用作一个有效的研究工具。
2020-07-27 cs.LO cs.PL
