$\mathsf{LLF}_{\cal P}$：一个逻辑框架，用于使用单子对外部证据、边条件和证明不相关性进行建模
$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
摘要：
我们扩展了建设性的依赖类型论理论的逻辑框架$\mathsf{LF}$与一元，依赖型构造索引的谓词判断，称为锁。这些单子在建立由$\mathsf{LF}$类型编码的对象逻辑的判断时捕获各种可能的证明态度。标准的例子是因式分解出一个约束的验证，或者将其委托给一个外部的神谕，或者提供一些非必然的认识证据，或者简单地丢弃一个认为它不相关的前提条件的证明证据。这种新的逻辑框架称为Lax逻辑框架（$\mathsf{LLF}_{\cal P}$），它是$\mathsf{LF}$的保守扩展，因此它是形式化处理逻辑系统中规则或外部证据中的副条件的合适的元语言。一旦锁类型构造函数${\cal L}^{\cal P}_{M,σ}[\cdot]$的一元性质被充分利用，$\mathsf{LLF}_{\cal P}$就出现了，${\cal L}^{\cal P}_{M,σ}[\cdot]$是由作者和Marina Lenisa在一系列论文中介绍的。锁单子的性质允许使用锁析构函数${\cal U}^{\cal P}_{M,σ}[\cdot]$来代替Moggi的单子$let_T$，从而简化了等式理论。${\cal U}^{\cal P}_{M,σ}[\cdot]$的规则还允许在满足约束后删除monad。基于$\mathsf{LF}$中$\mathsf{LLF}_{\cal P}$的编码，我们采用一种新的间接方法推导出了$\mathsf{LLF}_{\cal P}$的元理论.我们讨论了$\mathsf{LLF}_{\cal P}$中按值调用$λ$演算、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,σ}[\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,σ}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,σ}[\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 $λ$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
