在 Coq 中对宽松逻辑框架 LLFP 的定义式实现，以支持快速而宽松的推理
计算机科学中的逻辑
2019-10-25 v1
摘要
宽松逻辑框架 LLFP 由包括最后两位作者在内的一支团队提出，旨在为集成不同证明开发工具提供概念框架，从而允许外部证据以及推迟、委托或分解旁条件。特别地，LLFP 允许减少执行证明无关检查的次数。在本文中，我们给出 LLFP 在 Coq 中的一种浅层、实为定义式的实现，即我们使用 Coq 同时作为 LLFP 的主框架与预言机。这阐明了支撑 Lock-types 机制的原理，也暗示了如何以 LLFP 的特性扩展 Coq。随后将该派生证明编辑器用于开发一个新兴范式（在逻辑与实现层面）的案例研究，我们遵循 Danielsson 等人 [6] 称之为快速而宽松的推理。该范式以正确性换取效率，并相当于将繁琐或计算密集的检查推迟或与主任务并行，直到我们确实确信预期目标可以实现。典型例子包括 CPU 中的分支预测与乐观并发控制。
引用
@article{arxiv.1910.10848,
title = {A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning},
author = {Fabio Alessi and Alberto Ciaffaglione and Pietro Di Gianantonio and Furio Honsell and Marina Lenisa},
journal= {arXiv preprint arXiv:1910.10848},
year = {2019}
}
备注
In Proceedings LFMTP 2019, arXiv:1910.08712