首页/论文/1909.01465

arXiv 1909.014652019-09cs.PL

Towards Gradual Checking of Reference Capabilities

Kiko Fernandez-Reyes, Isaac Oscar Gariano, James Noble, Tobias Wrigstad

备注：: draft

英文摘要：

Concurrent and parallel programming is difficult due to the presence of memory side-effects, which may introduce data races. Type qualifiers, such as reference capabilities, can remove data races by restricting sharing of mutable data. Unfortunately, reference capability languages are an all-in or nothing game, i.e., all the types must be annotated with reference capabilities. In this work in progress, we propose to mix the ideas from the reference capability literature with gradual typing, leading to gradual reference capabilities.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Approximate Normalization and Eager Equality Checking for Gradual Inductive Families

Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In particular, migrating code to these languages is challenging. Gradual typing can make dependently-typed languages easier to use by mixing static and dynamic checking in a principled way. With gradual types, programmers can incrementally migrate code to a dependently typed language. However, adding gradual types to dependent types creates a new challenge: mixing decidable type-checking and incremental migration in a full-f…

2021-07-10cs.PL

Gradual Tensor Shape Checking

Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where users can improve the precision of the inference by …

2023-03-25cs.PL

Putting gradual types to work

In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual typing. We discuss our implementation and challenges faced -- specifically how gradual typing rules apply to our representation of composite and recur…

2021-01-28cs.PL

扩展渐进验证器的规范能力以支持纯函数

Expanding Specification Capabilities of a Gradual Verifier with Pure Functions

本文通过引入纯函数扩展Gradual C0的规范能力，提升其在复杂表达式处理和观察方法编码方面的效能。

2025-11-27cs.PL

Sums of Uncertainty: Refinements Go Gradual

A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program annotated with refinements passes type checking, pattern-matching failures become impossible. Unfortunately, refinement is a monolithic property of a type, exacerbating the difficulty of adding refinement types to nontrivial programs. Gradual typing has explored how to incrementally move between static typing and dynamic typing. We develop a type system of grad…

2020-09-19cs.PL

Monotonic References for Gradual Typing

We describe an alternative approach to handling mutable references (aka. pointers) within a gradually typed language that has different efficiency characteristics than the prior approach of Herman et al. [2010]. In particular, we reduce the costs of reading and writing through references in statically typed regions of code. We reduce the costs to be the same as they would in a statically typed language, that is, simply the cost of a load or store instruction (for primitive data types). This reduction in cost is especially important for programmers who would like to use gradual typing to facili…

2014-07-12cs.PL

更多相关论文收起更多论文

渐进敏感性类型化

Gradual Sensitivity Typing

本文提出并形式化了渐进敏感性类型化语言 GSoul，通过支持未知敏感性和区间有界不精确性，使程序可从无静态敏感性信息平滑演进到动静混合检查，并证明其满足渐进保证与度量保持性。

2025-03-12cs.PL

A Gradual Type System for Elixir

Elixir is a functional programming language with dynamic typing. We propose a gradual type system that makes it possible to perform type-checking on a significant fragment of the language. An important feature of the type system is that it does not require any syntactic change to Elixir. Type information is provided by means of function signatures which are declared in terms of Elixir typespec directives. The proposed type system is based on subtyping and is backward compatible, as it allows the presence of untyped code fragments. We have implemented a prototype of the type-checker in Elixir i…

2021-04-16cs.PL

Graduality from Embedding-projection Pairs (Extended Version)

Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland's (dynamic) gradual guarantee, which says that giving components of a program more precise types only adds runtime type checking, and does not otherwise change behavior. In this paper, we give a semantic reformulation of the gradual guarantee called graduality. We change the name to promote the analogy that graduality is to gradual typing what parametricity is to polymorphism. Each give…

2018-07-08cs.PL

Gradual Typing for Extensibility by Rows

This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the dynamic row type, which represents a statically unknown part of a row, and consistency for row types, which allows injecting static row types into the dynamic row type and, conversely, projecting the dynamic row type to any static row type. While consistency captures the behavior of the dynamic row type statically, it makes the semantics of a gradually typed language incoherent when combined with row equivalence which identifies row types up to field reordering. To solve this problem, we d…

2019-10-22cs.PL

渐进式元编程

Gradual Metaprogramming

针对Python嵌入的动态类型DSL生成静态类型数据管道代码时存在的错误检测晚、定位难问题，提出渐进式元编程，通过代码片段类型检查与拼接时增量运行时检查实现迁移路径、早检测、准定位，并定义MetaGTLC演算及机械化证明其有效性。

2025-08-20cs.PL

Type Checking Extracted Methods

Many object-oriented dynamic languages allow programmers to _extract methods_ from objects and treat them as functions. This allows for flexible programming patterns, but presents challenges for type systems. In particular, a simple treatment of method extraction would require methods to be contravariant in the receiver type, making overriding all-but-impossible. We present a detailed investigation of this problem, as well as an implemented and evaluated solution. Method extraction is a feature of many dynamically-typed and gradually-typed languages, ranging from Python and PHP to Flow and Typ…

2021-11-19cs.PL

渐进概率λ演算

A Gradual Probabilistic Lambda Calculus

University of Chile（智利大学）；Millennium Institute of Foundational Research on Data (IMFD)（数据基础研究千年研究所）；National University of Singapore（新加坡国立大学）

本文提出并形式化了GPLC，一种渐进源概率λ演算，通过二元概率选择运算符实现静态与动态检查的渐进过渡，支持渐进引入/移除类型和概率注解，证明了其类型安全性和渐进保证。

2026-10-16cs.PL

Which of My Transient Type Checks Are Not (Almost) Free?

One form of type checking used in gradually typed language is transient type checking: whenever an object 'flows' through code with a type annotation, the object is dynamically checked to ensure it has the methods required by the annotation. Just-in-time compilation and optimisation in virtual machines can eliminate much of the overhead of run-time transient type checks. Unfortunately this optimisation is not uniform: some type checks will significantly decrease, or even increase, a program's performance. In this paper, we refine the so called "Takikawa" protocol, and use it to identify which …

2019-09-12cs.PL

用证据编译渐进类型

Compiling Gradual Types with Evidence

University of Chile（智利大学）

本文提出GrEv编译器，基于证据实现高效渐进类型化，实验显示其性能优于基于转换的编译器。

2025-12-27cs.PL

捕获演算中Box推断的形式化

Formalizing Box Inference for Capture Calculus

针对捕获演算中Box符号负担重、难以集成到主流语言的问题，本文提出Box推断的形式化方案，构建半算法变体及类型层推断系统，并证明其可靠性与完备性。

2023-06-10cs.PL

丰富数据感知的声明式规范的高效一致性检查（扩展版）

Efficient Conformance Checking of Rich Data-Aware Declare Specifications (Extended)

Universidade de Santiago de Compostela（圣地亚哥-德孔波斯特拉大学）；Free University of Bozen-Bolzano（博尔扎诺自由大学）；INESC-ID/Instituto Superior Técnico, Universidade de Lisboa（INESC-ID/里斯本技术学院，里斯本大学）

本文针对具有通用数据类型和数据条件的 data-aware Declare 规范，提出结合 A* 搜索与 SMT 求解的新算法，高效计算数据感知最优对齐，实验证明其性能达到或超越现有方法并支持更强的数据依赖表达力。

2025-06-30cs.AIcs.DBcs.PL