一句话：在守卫类型论中为带概率选择与递归类型的 FPC⊕ 建立操作与指称语义，并支持充分性与上下文等价推理。
构造性类型论将逻辑与编程统一，便于在类型论内推理程序，但递归与概率选择等计算效应难以直接表示，限制了其适用性。本文在守卫类型论中定义并推理 FPC⊕：一个带概率选择与递归类型的编程语言。作者用高阶归纳类型表示有限分布，用守卫递归建模递归，分别给出 FPC⊕ 的操作语义与指称语义，并建立二者之间的关系。该关系可用于证明充分性（adequacy），还可用于在上下文等价意义下推理程序。结果表明，守卫类型论能为含递归与概率效应的语言提供统一的语义与推理框架。
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it is challenging to extend these applications to languages with recursion and computational effects such as probabilistic choice, because these features are not easily represented in constructive type theory. We show how to define and reason about FPC ⊕ , a programming language with probabilistic choice and recursive types, in guarded type theory. We use higher inductive types to represent finite distributions and guarded recursion to model recursion. We define both operational and denotational semantics of FPC ⊕ , as well as a relation between the two. The relation can be used to prove adequacy, but we also show how to use it to reason about programs up to contextual equivalence.
@article{paperbot3243,
title = {Modelling Recursion and Probabilistic Choice in Guarded Type Theory},
author = {Philipp Stassen and Rasmus Ejlers Møgelberg and Maaike Annebet Zwart and Alejandro Aguirre and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704884}
}