Implementing Dependent Types in pi-forall
本讲义介绍最小依赖类型语言 pi-forall 的设计及其类型检查器实现，源自2023年俄勒冈编程语言暑期学校课程。
2023-07-11 cs.PL
Canonicity and normalisation for Dependent Type Theory
我们显示规范性和规范化的依赖类型论的累积序列的宇宙和布尔类型。这个论点遵循了还原论的通常概念，可以追溯到哥德尔的辩证法解释和泰特的工作。我们的方法的一个关键特征是使用证明相关的概念还原。
2018-10-22 cs.PL
Structural Contracts -- Contracts for Type Construction & Dependent Types to Ensure Consistency of Extra-Functional Reasoning
针对使用基于契约的设计规范和细化的功能外属性，本研究摘要建议使用类型约束和依赖类型，以确保正确和一致的自上而下的合同分解相对于一个可指定的类型构造函数。为此，我们总结了组成问题，并给出了我们的方法的简短草案，称为结构合同。
2019-06-26 cs.PL
Dependent Type Systems as Macros
我们提出了Turnstile+，一个高层次的，基于宏的MetaDSL构建依赖类型的语言。有了它，程序员可以快速地原型化和重新设计新的依赖类型的功能和扩展。或者，它们可以创建全新的DSL，其依赖类型“power”是针对特定域定制的。我们的框架对面向语言编程的支持也使其适合于实验交互组件的系统，例如，一个证明助手及其伴随DSL。本文解释了Turnstile+的实现细节，以及如何使用它来创建各种依赖类型的语言，从一个轻量级的索引类型，到一个全频谱的证明助手，完成了一个战术系统和扩展的功能，如大小类型和SMT交互。
2021-07-02 cs.PL
A Dependently Typed Library for Static Information-Flow Control in Idris
在应用程序中安全地集成第三方代码，同时保护信息的机密性是一个长期存在的问题。纯函数式程序设计语言（如Haskell）使得通过像Russo的MAC这样的库来实施轻量级信息流控制成为可能。这项工作提出DepSec，MAC启发，依赖类型库的静态信息流控制在Idris。我们展示了如何添加依赖类型增加了最先进的静态信息流控制库的表现力，以及DepSec如何在一个关键的例子中匹配一个特殊用途的依赖信息流类型系统。最后，我们展示了使用依赖类型指定静态强制解密策略的新颖而强大的方法。
2019-02-18 cs.PL
Label-Dependent Session Types
会话类型已经作为通信协议的类型规则出现。具有会话类型的现有演算配备了许多不同的原语，这些原语将通信与传输值的引入或消除相结合。我们提出了一个轻量级的操作语义的基本会话类型演算。它从数据的引入和消除完全简化了通信，因此具有单个通信减少的功能，它充当了接收器和接收器之间的会合。我们通过引入标签依赖的会话类型来实现这种解耦，这是一个具有子类型的最低限度的值依赖的会话类型系统。该系统是足够强大的模拟现有的功能会话类型的系统。与这样的系统相比，标签依赖的会话类型对代码的限制更少。我们进一步介绍原始递归自然数的类型级别，从而允许描述协议的行为取决于在消息中交换的数字。介绍了一种算法类型检查系统，并证明了它与声明式类型检查系统是等价的。新的演算展示了依赖类型和线性类型的新型轻量级集成，其用途超出了会话类型系统。
2019-11-11 cs.PL
A Dependently Typed Multi-Stage Calculus
我们研究了一个多阶段的程序设计语言的依赖类型的扩展LA MetaOCaml，它支持准报价和跨阶段的持久性操作的代码片段作为第一类值和评估结构执行的程序动态生成的代码操作。依赖类型有望在多阶段编程中对动态生成的代码的行为实施强不变性--超越简单的类型安全性。然而，扩展并不是微不足道的，因为这样的类型系统必须考虑类型的阶段-粗略地说，周围引用的数量-考虑。为了严格地研究这样的扩展的性质，我们开发了$λ^{MD}$，这是Hanada和Igarashi的依赖类型的类型演算$λ^{\triangleright\%} $的扩展，并证明了它的性质，包括保存，汇合，强规范化的充分减少，和进步的分阶段减少。出于代码生成器生成的代码，其类型取决于一个值从外部的报价，我们认为跨阶段的持久性依赖类型的多阶段编程和某些类型的等价物，不直接从减少规则的意义。
2021-08-17 cs.PL
A Role for Dependent Types in Haskell (Extended version)
现代的Haskell支持零成本转换器，这是一种机制，共享相同运行时表示的类型可以在它们之间自由转换。为了确保这种转换是安全和可取的，此功能依赖于一种角色机制来禁止无效的转换。在这项工作中，我们将展示如何整合角色与依赖类型系统，并证明，使用Coq证明助手，所产生的系统是健全的。我们将这项工作设计为向Glasgow Haskell编译器添加依赖类型的基础，但我们也希望它对其他依赖类型语言的设计者有用，他们可能希望采用Haskell的安全编译器特性。
2019-05-31 cs.PL
Generic Zero-Cost Reuse for Dependent Types
众所周知，依赖类型语言在代码重用方面存在问题。传统的非索引代数数据库（例如列表）与大量的索引变量（例如向量）一起出现。函数经常被重写为基本相同数据类型的非索引和索引版本，这是代码重复的来源。我们在Curry风格的依赖类型论中工作，其中相同的未类型化术语可以被分类为数据类型的非索引版本和索引版本。对于依赖类型的重用问题，已经提出了许多解决方案，但是我们在解决方案中利用Curry风格的类型论，不仅重用数据和程序，而且以零成本（没有运行时损失）这样做。我们的工作是一个练习依赖类型的泛型编程，并内化的过程中的零成本重用的身份功能的咖喱风格的理论。
2018-07-09 cs.PL
Proof Mining with Dependent Types
有几种方法可以对大型正式证明语料库进行数据挖掘。其中一些方法是基于统计机器学习的，还有一些是基于理论探索的。然而，大多数是为无类型或简单类型的定理证明器开发的。本文提出了一种将统计数据采掘和理论探索相结合的方法，用于Coq语言中的依赖类型证明的分析和自动化。
2017-05-19 cs.PL
Linear Dependent Types for Domain Specific Program Analysis (Extended Abstract)
在本教程中，我将介绍如何组合线性和依赖类型可以用来描述高阶程序的不同属性。线性类型已被证明对表达函数的属性特别有用;依赖类型对描述程序在控制流方面的行为很有用。这两个想法很好地结合在一起，当一个人有兴趣分析的功能取决于程序的控制流的属性。我将通过复杂性分析和敏感性分析的例子来说明这些想法。我将通过讨论这种方法的一般性来结束本教程。
2013-06-28 cs.PL
Dependent Types for JavaScript
我们提出依赖JavaScript（DJS），一个静态类型的方言的命令式，面向对象，动态语言。DJS支持特别具有挑战性的功能，例如运行时类型测试，高阶函数，可扩展对象，原型继承，以及通过嵌套细化类型，堆的强更新和堆展开的组合来精确跟踪原型层次结构的数组。通过我们的DJS实现，我们证明了类型系统具有足够的表达能力，可以从几个来源的小示例中找到各种棘手的习惯用法，包括流行的书籍JavaScript：The Good Parts和SunSpider基准套件。
2012-08-01 cs.PL
Multiparty Dependent Session Types (Extended Abstract)
今天的程序比以往任何时候都更加分布式和并发，结构化通信是核心。由于缺乏并发性的正式规范/验证，构建和调试这样的程序是困难的。这项工作正式的第一个多方依赖的会话类型作为一个表现力和实用的类型纪律，执行通信协议。类型系统是在多线程$λ$ -演算的设置中制定的，其灵感来自于多角色逻辑，这是我们之前发现的经典逻辑的概括。我们证明了一种新的技术称为无死锁还原的合理性。类型系统的可靠性意味着通信的保真度和没有死锁。
2018-07-31 cs.PL
Dependently Typed Programming based on Automated Theorem Proving
Mella是一种最小依赖类型的程序设计语言和Haskell实现的交互式定理证明器。它的主要目的是研究在一个纯粹和简单的设置自动定理证明器的有效集成。这种集成对于支持依赖类型语言的程序开发是必不可少的。我们集成了等式定理证明器Waldmeister，并在TPTP库中的800多个证明目标上进行了测试。与以前的方法相比，在Mella中重建Waldmeister证明是非常健壮的，并且不会产生显着的证明搜索开销。因此，Mella产生了一个模板，用于在更复杂的语言中集成更有表现力的定理证明器。
2011-12-16 cs.PL
An Effectful Treatment of Dependent Types
为了研究计算效应和依赖类型之间的相互作用，我们将Levy的按推值调用（CBPV）分析从简单扩展到依赖类型论（DTT）。我们定义的天真系统依赖类型的CBPV，dCBPV-，其扩展与Kleisli扩展依赖函数，dCBPV+的原则。我们从句法、范畴语义、具体模型和操作语义的角度对这些系统进行了研究，并考察了它们的影响。我们观察到，虽然dCBPV+的表达能力是必要的，如果我们想要良好定义的调用按值（CBV）和调用按名称（CBN）的DTT翻译，它是一个不那么简单的系统比dCBPV-，在存在一些影响。事实上，为了能够构建特定的模型并在操作语义中保留主语归约属性，我们需要施加某些子类型条件，其思想是，随着某些效果的执行，计算的类型可能只会变得更多（而不是更少）指定。
2016-03-14 cs.PL
Dependent Session Types for Verified Concurrent Programming
本文提出TLLC，扩展双层线性依赖类型理论以支持会话并发，实现并发程序与顺序程序的关系验证，并开发了原型编译器。
2025-10-23 cs.PL
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
我们提出了一个全谱依赖类型的核心语言，其中包括非终止性和计算无关性（又名。擦除），这是一种以前没有研究过的组合。这两个特性相互作用：为了保护类型安全，我们必须小心地只擦除终止表达式。我们的语言设计受到CBV评价的选择以及我们对命题等式的新颖处理的强烈影响，该等式具有异质的、完全擦除的消除形式。
2012-02-14 cs.PL
Dependent Types for Multi-Rate Flows in Synchronous Programming
同步程序设计语言出现于20世纪80年代，作为实现反应式系统的工具，它与来自物理环境的事件交互，并且通常必须在严格的时间约束下进行。在这份报告中，我们在ATS内部编码各种实时原语的实验同步语言称为前奏曲，其中ATS是一个静态类型的语言与ML类似的功能核心，支持依赖类型（的DML风格）和线性类型。我们表明，这些原语上施加的验证要求可以正式表示在ATS中的依赖类型。此外，我们修改了Prelude编译器，自动生成ATS代码从Prelude源。这个修改后的编译器允许我们仅仅依靠ATS中的类型检查来履行源于对Prelude代码进行类型检查的需要的证明义务。而ATS通常被用作通用程序设计语言，我们在此证明，它也可以方便地用于支持某些形式的高级静态检查的语言配备了较少的表达类型。
2017-02-08 cs.PL
Typed Closure Conversion for the Calculus of Constructions
依赖类型语言（如Coq）用于指定和验证源程序的完整功能正确性。类型保持编译可用于通过编译到生成的目标语言程序中来保持这些规范和正确性证明。不幸的是，依赖类型的类型保持编译是困难的。本质上，问题在于依赖类型系统是围绕高级组合抽象来设计的，以决定类型检查，但编译会干扰类型系统规则来推理运行时术语。我们开发了一个类型保持闭包转换的翻译从构造演算（CC）与强依赖对（$Σ$类型）-一个子集的核心语言Coq-到一个类型安全的，依赖类型的编译器中间语言命名为CC-CC。在这项工作中的核心挑战是如何翻译的源类型系统的规则推理功能到目标类型系统的规则推理闭包。为了证明这些规则的合理性，我们通过在CC中给出一个模型来证明CC-CC的可靠性。除了类型保持，我们证明了分离编译的正确性。
2018-08-12 cs.PL
Toward SMT-Based Refinement Types in Agda
依赖类型提供了很大的通用性和强大的功能，但是用它们来开发证明可能是乏味的，并且需要相当多的人工指导。我们建议将可满足性模理论（SMT）为基础的细化类型的依赖类型的语言Agda的努力，以减轻一些负担的依赖类型的编程，并结合两种方法的机械化定理证明的优势。
2021-10-12 cs.PL
Coming to Terms with Your Choices: An Existential Take on Dependent Types
类型级编程是一种越来越流行的获得额外类型安全的方法。不幸的是，在大多数工业上使用的程序设计语言中，它仍然是二等公民。我们提出了一个新的依赖类型系统，子类型和单例类型，其目标是使类型级编程在一个可访问的风格。我们系统的核心是一个非确定性选择算子。我们认为，拥抱非确定性是至关重要的依赖类型，以更广泛的程序员观众，因为现实世界的程序将不可避免地与不精确的类型，甚至不纯的代码。此外，我们表明，单例类型与选择操作符相结合，可以作为许多类型的功能在实践中感兴趣的替代品。我们使用Coq证明助手来建立我们方法的可靠性。我们的稳健性方法模型使用额外的函数参数来表示选择的非确定性。我们使用单例类型和存在类型来表示类型级计算，这些类型量化了选择参数。为了证明我们的类型系统的实用性，我们提出了一个实现作为Scala编译器的修改。我们提供了一个案例研究，其中我们为Spark数据集开发了一个强类型的包装器。
2020-11-15 cs.PL
A Two-Level Linear Dependent Type Theory
本文提出一种两级线性依赖类型理论，通过分层解耦逻辑与程序语义，实现资源安全编程与深度验证的统一语言。
2025-10-06 cs.PL
Propositional Equality for Gradual Dependently Typed Programming
渐进依赖类型可以通过为不精确的类型和证明（其中某些部分已被省略）提供原则性语义来帮助逐步采用依赖类型化代码。然而，目前的渐进依赖类型理论缺乏类型论的一个核心特征：命题平等。Lennon-Bertrand等人证明，当自反证明$\mathit{refl}$是等式类型的唯一闭值时，CIC的命题等式的逐渐扩展违反了静态观测等价。扩展相等的函数在运行时间应该是不可区分的，但是相等和类型不精确的组合允许区分扩展相等但语法不同的函数的上下文。这项工作提出了一个逐渐类型化的语言，支持命题平等。我们通过设计一个等式类型来避免上述问题，其中$\mathit{refl}$不是唯一的封闭居民。相反，每一个相等性证明都携带一个至少与相等项一样精确的项，作为它们似乎相等的证明。这些见证者在程序运行时跟踪部分类型信息，当该信息显示两个等同的术语不一致时，就会引发错误。类型信息的组合被内化为语言的一个构造，并且对于其求值被变量阻塞的函数体被延迟。通过延迟，我们可以确保外延相等的函数组合没有错误，从而防止上下文区分它们。我们描述了设计这个系统的一致性和精度关系的挑战，以及这些挑战的解决方案。最后，我们证明了重要的元理论：类型安全，保守嵌入的CIC，正规性，并逐步保证Siek等人。
2022-05-02 cs.PL
Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments
本文提出了一种通过隐式参数实现依赖数据和共数据类型的算法类型系统，旨在填补极性语言在扩展性方面的空白。
2025-11-19 cs.PL
Dependent-Type-Preserving Memory Allocation
针对依赖类型语言编译后规范被擦除导致外部链接程序可违反内存安全的问题，提出支持依赖内存分配的类型化中间语言及依赖类型保持的编译通行证，以实现链接时类型检查。
2025-09-10 cs.PL
Type Theory as a Language Workbench
语言工作台为语言设计人员提供了一个创建DSL的表达环境。类似地，对机械化元理论的研究表明，依赖类型语言如何提供表达环境来形式化和研究DSL及其元理论属性。但是，我们能说依赖类型的语言有资格作为语言工作台吗？我们说是的！我们已经开发了一个典型的DSL称为Velo，展示不仅依赖类型的技术来实现和操作IR，但依赖类型的语言，使罚款语言工作台。Velo是一种简单的验证语言，具有良好类型的漏洞，并带有完整的编译器管道：解析器，阐述器，REPL，评估器和编译器通道。具体来说，我们描述了我们的设计选择良好类型的IR设计，包括支持良好类型的孔，CSE是如何实现在一个良好类型的设置，以及如何机械化的类型可靠性证明Velo是源的评估。
2023-01-30 cs.PL
Dependently Typed Folds for Nested Data Types
我们提出了一种方法来开发折叠嵌套数据类型使用依赖类型。我们称这种折叠为$\textit{dependently typed folds}$，它们具有以下性质。(1)依赖类型的折叠是由良基递归定义的，它们可以用完全依赖类型的语言来定义。(2)依赖类型的折叠不依赖于映射，映射函数和许多终止函数可以使用依赖类型的折叠来定义。(3)嵌套数据类型的归纳原理来自于依赖类型折叠的定义，由依赖类型折叠定义的程序可以被形式化验证。(4)对于任何嵌套的数据类型，都存在依赖类型的折叠，并且它们可以专用于传统的$\textit{higher-order folds}$。使用各种各样的例子，我们展示了如何编程和理由依赖类型的褶皱。我们还展示了如何获得一般的依赖型褶皱，以及如何将它们专门化到相应的高阶褶皱。
2018-06-13 cs.LO cs.PL
Dependent Multiplicities in Dependent Linear Type Theory
本文提出了一种新型的依赖线性类型论，其中某些变量的多重性（即变量在程序中被使用的次数）可以依赖于其他变量，从而为涉及分支和递归的程序提供精确的资源注解。该类型系统通过将线性逻辑嵌入到依赖类型论中，并指定嵌入逻辑如何与宿主理论交互来实现。我们利用依赖类型论中的自然数推导出具有依赖多重性的量化类型系统。该理论支持W类型，从而为一大类归纳类型提供了系统性的资源感知处理。我们将其语义定义为在对称单子范畴上索引的范畴，从而推广了量化范畴族。现有的依赖类型语言可以轻松地通过我们的系统进行扩展，我们通过在Agda中的实现进行了演示。
2026-05-19 cs.LO cs.PL
Dependently-Typed Formalisation of Typed Term Graphs
我们采用依赖类型的程序设计语言Agda 2探索形式化的非类型化和类型化的长期图形直接作为基于集合的图形结构，通过GS-monoidal类别的Corradini和Gadducci，并作为嵌套的让表达式使用Pouillard和Pottier的NotSoFresh库的变量绑定抽象。
2011-02-14 cs.LO cs.PL
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
本文介绍了带线性依赖类型的实验性量子电路编程语言 Proto-Quipper-D，通过示例展示了依赖类型在构建正确量子电路、实现电路族编程及解决垃圾量子比特类型安全取消计算问题方面的作用。
2020-12-12 cs.PL quant-ph
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
2006-10-11 cs.LO cs.PL
Type safety of rewrite rules in dependent types
依赖类型论的表达能力可以通过对一些附加的计算规则取模来识别类型来扩展。但是，为了保持类型检查的可判定性或系统的逻辑一致性，必须确保这些用户定义的重写规则保持类型。本文给出了一种利用Knuth-Beneficiary完备化检验该性质的新方法。
2020-10-30 cs.LO cs.PL
Guarded Dependent Type Theory with Coinductive Types
我们提出了守护依赖类型论，gDTT，一个扩展的依赖类型论与“后来”的模态和时钟量词的编程和证明与守护递归和共归纳类型。后一种模态用于以模块化的、基于类型的方式确保递归定义的生产力。时钟量词用于控制消除后一种模态，并使用保护递归类型对共归纳类型进行编码。发展gDTT的关键是新型和术语形成者，涉及我们所说的“延迟替代”。这些概括了早期工作中考虑的后一种模态的适用函子规则，并且对于依赖类型的编程和证明至关重要。我们证明了相对于指称模型的类型论的合理性。
2016-01-07 cs.LO cs.PL
A dependent nominal type theory
名义抽象语法是Gabbay和Pitts开创的一种表示名称和绑定的方法。到目前为止，名词化技术大多是用经典逻辑或模型论来研究的，而不是类型论。名词扩展到简单的，依赖的和ML类多态语言的研究，但可判定性和规范化的结果只建立了简单的名义类型论。我们提出了一个LF风格的依赖类型论扩展的名称抽象类型，证明了可靠性和可判定性的β-eta-等价检查，讨论充分性和规范形式通过一个例子，并讨论扩展，如依赖类型的递归和归纳原则。
2012-02-17 cs.LO cs.PL
Dependent Session Types
会话类型提供了一种基于类型的规程，用于在分布式编程中实施通信协议。我们之前已经在多线程$λ$ -线性类型演算的设置中形式化了简单的会话类型。在这项工作中，我们建立在我们以前的工作，提出了一种形式的依赖会话类型（的DML风格）。我们制定的类型系统提供了线性和对偶保证，不需要任何运行时检查或特殊编码。我们制定的依赖会话类型是第一次，它是特别适合于实际的实施。作为一个例子，我们描述了一个用ATS编写的编译到Erlang/Elixir后端的实现。
2017-04-24 cs.DC cs.PL
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
本文提出依赖分层模态类型理论 DeLaM，将分层模态类型理论扩展至依赖类型，在统一框架中支持代码组合执行与类型/项代码的内涵分析，从而为证明助手实现类型安全的策略机制奠定基础。
2024-07-08 cs.LO cs.PL
A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction
我们引入概率依赖类型系统（PDTS）通过一个功能语言的基础上的子系统的直觉类型论，包括依赖的总和和产品，这是扩大到包括随机功能。我们提供了一个基于采样的语义的语言的基础上非确定性的β减少。此外，我们推导出一个概率逻辑的PDTS引入Curry-Howard同构的直接结果。概率逻辑推导出有限离散分布提供了一个通用的表示。
2016-02-23 cs.LO cs.PL
Towards an induction principle for nested data types
针对嵌套数据类型难以推导归纳原理的问题，本文引入依赖类型折叠，并以Bush为例展示推导过程，同时探讨其与传统高阶折叠的关系。
2023-06-16 cs.LO cs.PL
AdapTT: Functoriality for Dependent Type Casts
AdapTT是一种通过抽象适配器概念系统化实现类型构造函子性的依赖类型理论，推导出一般归纳类型构造的类型转换结构定律。
2025-12-08 cs.LO cs.PL
Linear Dependent Types in a Call-by-Value Scenario (Long Version)
线性依赖类型允许精确地捕获lambda项的扩展行为和时间复杂度，当后者由Krivine的抽象机器评估时。在这项工作中，我们表明，同样的范例可以应用到呼叫的价值评估。介绍了Plotkin PCF的线性相关类型系统dlPCFV，其类型反映了CEK机中计算项的复杂性。dlPCFV被证明是合理的，但也是相对完整的：每一个真正的陈述的延伸和有意的行为的条款可以得到，提供所有真正的索引项不等式可以用作假设。
2012-07-24 cs.LO cs.PL
A graded dependent type system with a usage-aware semantics (extended version)
分级类型论提供了一种机制来跟踪和推理类型系统中的资源使用情况。在本文中，我们开发了GraD，一个新的版本，这样一个分级依赖型系统，包括功能，张量积，加法和单位类型。由于标准的操作语义是资源不可知的，我们开发了一个基于堆的操作语义，并证明了一个合理性定理，显示正确的会计资源的使用。从这个定理可以导出一些有用的性质，包括标准型可靠性定理、计算中不受无关资源的干扰以及线性资源的单指针性质。我们希望，我们的工作将提供一个基础，在实际的程序设计语言，如Haskell集成线性，无关性和依赖类型。
2021-01-06 cs.LO cs.PL
Linear Dependent Types and Relative Completeness
本文介绍了一个具有完全高阶递归的λ演算的线性相关类型系统dlPCF，并证明了它是可靠的和相对完备的.完整性在很强的意义上成立：dlPCF不仅能够精确地捕获PCF程序的功能行为（即输出如何与输入相关），而且还能够捕获它们的一些内涵属性，即用Krivine机器评估它们的复杂性。dlPCF是围绕依赖类型和线性逻辑设计的，并在索引项的底层语言上进行参数化，索引项可以进行调优，从而牺牲完整性以换取易处理性。
2012-10-19 cs.LO cs.PL
MiniAgda: Integrating Sized and Dependent Types
大小类型是一种模块化的、理论上易于理解的工具，用于检查递归的终止性和共递归定义的生产力。其基本思想是跟踪类型系统中的结构下降和保护性，以使终止检查健壮并适用于高阶函数和多态性等强抽象。为了研究大小类型在证明助手和基于依赖类型论的程序设计语言中的应用，我们实现了一个核心语言MiniAgda，它具有显式的大小处理。新的考虑是必要的，以合理地集成大小类型与依赖关系和模式匹配，这是可能的概念，如不可访问的模式和参数函数空间。本文提供了一个介绍MiniAgda的例子和非正式的解释的基本原则。
2010-12-22 cs.LO cs.PL
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
本文利用预层模型和余单子 $\ lat$ 刻画 Cocon 的上下文类型语义，并借助带族范畴将其扩展到依赖类型。
2022-06-08 cs.LO cs.PL
Polynomial Time and Dependent Types
本文结合依赖类型与线性类型系统，通过两种方法（禁止可迭代数据构造和基于LFPL的支付方法）捕获多项式时间计算，并证明其可靠性，旨在统一外延与内部推理。
2023-11-14 cs.LO cs.PL
A Permission-Dependent Type System for Secure Information Flow Analysis
我们介绍了一种新的类型系统强制执行安全的信息流在一个命令式语言。我们的工作是出于静态检查潜在的信息泄漏在Android应用程序的问题。为此，我们设计了一个具有Android权限模型的轻量级类型系统，其中权限静态分配给应用程序并用于在应用程序中实施访问控制。我们从Banerjee和Naumann（BN）的类型系统中获得灵感，允许安全类型依赖于应用程序的权限。我们的类型系统的一个新功能是由权限测试引起的条件分支的类型规则，它引入了一个合并运算符的安全类型，允许更精确的安全策略被强制执行。我们的类型系统的可靠性证明了关于不干涉的概念。此外，通过将推理问题归结为安全类型格中的约束求解问题，给出了一个安全类型系统的类型推断算法。
2017-09-27 cs.CR cs.PL
Syntax and Semantics of Linear Dependent Types
本文提出了一种类型论，它把（直觉）线性类型与类型依赖相结合，从而适当地推广了直觉依赖类型论和完全线性逻辑。语法和完整的范畴语义的发展，后者在（严格）索引对称monoidal范畴的理解。以模块化方式处理各种可选类型的成形器。特别是，我们将看到，历史上备受争议的乘法量词和身份类型自然地产生于范畴考虑。这些新的乘法连接词的进一步特点是由几个身份有关的依赖类型论和线性逻辑通常的连接词。最后，详细研究了一类重要的模型，即由值在某个对称monoidal范畴内的族给出的模型。
2015-01-16 cs.LO cs.PL math.CT
Definitional Functoriality for Dependent (Sub)Types -- Extended version
本文将函子定律纳入依赖类型论的定义相等，用于支持自动化证明并导出与隐式包含子类型等价的强制子类型，且在 Coq 中机械化证明列表情形的类型检查可判定性。
2024-04-09 cs.LO cs.PL
Learning Structure-Aware Representations of Dependent Types
Aalto University（阿尔托大学）；University of Bologna（博洛尼亚大学）；Input Output (IOG)（Input Output（IOG））；University of Gothenburg（哥德堡大学）；Chalmers University of Technology（查尔姆斯理工大学）
该研究发布首个支持机器学习应用的大规模精细Agda程序-证明数据集，提出基于结构原则的新型神经架构以表示依赖类型程序，在前提选择任务中超越强基线，打通了Agda生态与机器学习领域的资源互通。
2024-10-30 cs.LG cs.PL
WebPie: A Tiny Slice of Dependent Typing
本文提出小型依赖类型语言 WebPie，涵盖归纳类型、递归与模式匹配，旨在为依赖类型初学者提供理解与系统构建语言的入门教学资源。
2024-04-08 cs.LO cs.PL cs.SC
Foundations of Substructural Dependent Type Theory
本文提出子结构依赖类型的新颖范畴解释与通用理论框架，证明关键元理论性质，并用于构建可在逻辑框架中有效表示线性矢列演算切分容许性的类型论。
2024-01-27 cs.LO cs.PL math.CT
Impredicativity in Linear Dependent Type Theory
School of Computer Science, University of Birmingham（伯明翰大学计算机学院）；iCIS, Radboud University Nijmegen（拉德堡德大学 iCIS）
本文通过构建线性依赖类型理论的实现模型，引入了具有双重解码操作的宇宙，实现了线性归纳类型的编码，并展示了相关性原则。
2026-02-09 cs.LO cs.PL math.CT
Frex: dependently-typed algebraic simplification
本文提出依赖类型化的代数化简库Frex，基于泛代数理论保证化简模块的终止性、可靠性和完备性，并在Idris 2和Agda中实现，支持模块化扩展、证明提取与认证及交互式开发。
2025-07-18 cs.LO cs.PL cs.SC
Linear Dependent Type Theory for Quantum Programming Languages
本文提出量子编程语言需要线性依赖类型理论，通过幺半范畴纤维化定义语义，并扩展Proto-Quipper-M实现依赖类型，提供操作语义和原型。
2022-09-06 cs.LO cs.PL math.CT
