一句话：扩展 LF 提出 Lax Logical Framework LLF_𝒫，用 Lock monad 表达边条件、外部证据与证明无关性，并证明其保守性。
该论文针对逻辑框架难以直接表达规则边条件、外部判定证据和证明无关性的问题，在构造性依赖类型理论 LF 上引入由判断谓词索引的 monadic 依赖类型构造子 Lock，以刻画核查约束、委托外部 oracle、提供非必然证据或丢弃前提见证等证明态度。作者充分利用 Lock 的 monad 性质，形成 Lax Logical Framework LLF_𝒫，并用 Lock 析构子替代 Moggi 的 let_T 简化等式理论；约束满足后还可移除 monad。元理论通过在 LF 中编码 LLF_𝒫 的间接方法建立，证明 LLF_𝒫 是 LF 的保守扩展，并讨论 call-by-value λ 演算、Hoare 逻辑和 Fitch-Prawitz 朴素集合论的编码。
We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,\sigma}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory. Comment: Accepted for publication in LMCS
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{HonsellLMS17,
title = {$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads},
author = {Furio Honsell and Luigi Liquori and Petar Maksimovic and Ivan Scagnetto},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:2)2017}
}