A graded dependent type system with a usage-aware semantics (extended version)

Multi-graded Featherweight Java

Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a variable is needed. We extend the type system of Featherweight Java to be resource-aware, parametrically on an arbitrary grade algebra modeling a specific usage of resources. We prove that this type system is sound with respect to a resource-aware version of reduction, that is, a well-typed program has a reduction sequence which does not get stuck due to resource consumption. Moreover, we show that the available gra…

具有擦除功能的分级模态依赖类型理论

A Graded Modal Dependent Type Theory with Erasure, Formalized

本文提出一种具有分级模态的依赖类型理论，通过参数化的模态结构跟踪变量使用，重点研究擦除模态下的函数参数擦除特性，并在Agda中形式化了该理论的元理论性质。

不耗尽，不浪费：大步语义的资源感知可靠性

Don't exhaust, don't waste: Resource-aware soundness for big-step semantics

通过扩展lambda演算的语义和类型系统，实现资源使用追踪，确保良类型程序在计算中既不耗尽也不浪费资源，并采用余归纳技术证明资源感知可靠性。

资源感知主动对象的公平终止

Fair Termination for Resource-Aware Active Objects

本文提出资源感知主动对象的核心演算与类型系统，结合分级语义和同步会话的公平终止技术，保证良类型程序总能最终终止。

Work Analysis with Resource-Aware Session Types

While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this article presents an analysis for statically deriving worst-case bounds on the total work performed by message-passing processes. To decompose interacting processes into components that can be analyzed in isolation, the analysis is based on novel resource-aware session types, which describe protocols and resource contracts for inter-proces…

Resource-Aware Session Types for Digital Contracts

Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nom…