数学中的类型推断

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed a…

优化最优约简：初等仿射逻辑的类型推断算法

Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic

本文提出了一种基于线性约束的初等仿射逻辑中的非线性项的类型推断算法。我们证明了算法的正确性和完备性。

建设性世界的经典数学

Classical Mathematics for a Constructive World

基于依赖类型论的交互式定理证明器具有支持构造性推理和经典推理的灵活性。构造性推理由依赖类型论原生地支持，而经典推理通常通过添加额外的非构造性公理来支持。然而，还有另一种观点认为，构造性逻辑是经典逻辑的延伸。本文将说明如何经典的推理可以支持在一个实用的方式内依赖类型论没有额外的公理。我们将看到几个经典结果如何应用于构造性数学的例子。最后，我们将看到如何通过使用弱值单子来表示经典函数空间，将这种观点从逻辑扩展到数学。

保护递归数据类型的类型推断

Type Inference for Guarded Recursive Data Types

我们考虑保护递归数据类型（GRDT）的类型推断--代数数据类型的最新概括。我们减少类型推断GRDTs统一下的混合前缀。因此，我们得到有效的类型推断。推断是不完整的，因为允许出现在类型系统中的类型约束集只是由类型推断生成的那些类型约束的子集。因此，只有当程序被充分地类型注释时，推理才会成功。我们提出了完善的程序，逐步推断类型，并协助用户识别哪些类型的信息丢失。此外，我们还引入了一些过程来测试一个类型是否不是主体类型，并在存在主体类型时查找主体类型。

构造性高sheaf模型及其在合成数学中的应用

Constructive higher sheaf models with applications to synthetic mathematics

本文提出了一种构造性高sheaf模型，用于合成数学中的类型理论扩展，包括univalence和高诱导类型，并构建了这些形式系统的构造性模型。

学习辅助的百万引理定理证明

Learning-assisted Theorem Proving with Millions of Lemmas

大型形式数学库由数百万个原子推理步骤组成，这些步骤产生相应数量的已证明语句（引理）。类似于非正式的数学实践，只有一小部分这样的陈述被正式的数学家命名并在后来的证明中重复使用。在这项工作中，我们建议和实施标准定义的估计有用的HOL光引理证明进一步的定理。我们使用这些标准来挖掘HOL Light和Flyspeck库中引理的大型推理图，将数百万个最佳引理添加到可以在以后的证明中重用的语句池中。我们表明，结合基于学习的相关性过滤，这种方法显着加强自动定理证明的新的大正式的数学库，如Flyspeck。

原子多态中的可类型化性与类型推断

Typability and Type Inference in Atomic Polymorphism

本文研究系统Fat的Curry风格变体，证明可类型化性可判定，并提出能处理非冗余约束的类型推断算法。

Implicit Polarized F: local type inference for impredicativity

System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction. Unfortunately, type applications need to be implicit for a language to be human-usable, and the problem of inferring all type applications in System F is undecidable. As a result, language designers have historically avoided impredicative type inference. We reformulate System F in terms of call-by-push-value, and study type inference for it. Surprisingly, this new pers…

用于检查注释的改进推理

Improved Inference for Checking Annotations

我们认为类型推断在Hindley/Milner系统扩展的类型注释和约束，特别侧重于Haskell风格的类型类。我们观察到，标准的推理算法是不完整的嵌套类型注释的存在。为了改善这种情况，我们引入了一个新的推理方案检查类型注释。我们的推理方案也是不完整的一般，但改善了现有的实现，如发现在格拉斯哥哈斯克尔密码（GHC）。对于某些情况（例如Haskell 98），我们的推理方案是完整的。我们的方法已经完全实现为Chameleon系统（Haskell的实验版本）的一部分。

Data Type Inference for Logic Programming

In this paper we present a new static data type inference algorithm for logic programming. Without the need of declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases, correspond to the data types processed by their intended meaning. The algorithm is also able to infer types given data type definitions similar to data definitions in Haskell and, in this case, the inferred types are more informative in general. We present the type inference algorithm, prove some properties and finally, we evaluate our approach on example programs th…

基于HOL Light的引理挖掘

Lemma Mining over HOL Light

大型形式数学库由数百万个原子推理步骤组成，这些步骤产生相应数量的已证明语句（引理）。类似于非正式的数学实践，只有一小部分这样的陈述被正式的数学家命名并在后来的证明中重复使用。在这项工作中，我们建议和实施标准定义的估计有用的HOL光引理证明进一步的定理。我们使用这些标准来挖掘核心HOL Light库中所有引理的大型推理图，将数千个最佳引理添加到命名语句池中，这些语句可以在以后的证明中重用。新引理的有用性，然后通过比较的性能自动证明的核心HOL光定理，没有这样的补充引理。

双态递归的类型推断

Type Inference for Bimorphic Recursion

本文提出了双态递归，这是一种受限制的多态递归，使得函数定义体中的每个递归调用具有相同的类型。双态递归允许我们为递归定义的函数分配两种不同的类型：一种是递归调用，另一种是定义之外的调用。本文中的双态递归是可以嵌套的。本文证明了双态递归具有主类型和可判定的类型推断。因此，双态递归给我们提供了灵活的递归类型和可判定的类型推断。本文还表明，它的类型成为不可判定的，因为嵌套的递归时，从双态递归删除的实例化属性。