一句话：综述 Contextual Types 的起源与能力：将类型与类型上下文配对，用于刻画部分程序、机器化元理论与元编程。
Contextual objects 将一个对象 M 与其有意义的类型上下文 Ψ 一起刻画；Contextual Types 则把这一思想内化到类型论中，用类型 A 与上下文 Ψ 的配对表示对象在 Ψ 中良类型。本文是教程式综述，回顾该思想的起源，并展示其在刻画部分程序、机器化元理论以及元编程中的能力。作者从简单类型设置出发，梳理将 contextual types 推广到依赖类型理论的既有工作，并讨论未来研究方向。全文不报告新实验，而是提供概念统一与路线图。
Contextual objects characterize an object M together with the typing context Ψ in which it is meaningful. This idea is then also internalized within the type theory itself using the notion of a contextual type which pairs the type A of an object together with the context Ψ in which the object is well-typed. In this tutorial, we review the origins of this idea and show its power in characterizing partial programs, mechanizing meta-theory, and meta-programming. Starting from the simply typed setting, we give an overview of existing work which adopts contextual types to dependent type theories and touch on future research directions.
DOI 原文 ·
@inproceedings{paperbot5520,
title = {Contextual Types, Explained},
author = {Brigitte Pientka},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394735}
}