一句话：在 Agda 的 Sikkel 库上实现多模态逻辑框架 µLF，支持对多模态程序进行证明并抽取到元语言。
在现成证明助手中嵌入多模态类型论（MTT）可以安全地引入额外推理原则，并借助内部模型实现嵌入语言与元语言之间的程序/证明抽取和互操作。已有 Sikkel 库为 Agda 实现了多模态简单类型论（MSTT）及依赖 MTT 的内部预层模型，但尚不能在多模态程序之上书写多模态证明。本文从 MTT 中提炼出一个基于 MSTT 的新多模态逻辑框架 µLF，并在 Sikkel 之上实现，将其与 MSTT 一同解释到已有内部模型中；同时改进语法、语义与抽取三层。作者通过证明 Guarded Stream 操作函数的性质及参数性谓词实例展示了 µLF 的用途。
Embedding Multimode Type Theory (MTT) as a library enables the usage of additional reasoning principles in off-the-shelf proof assistants without risking soundness or compatibility. Moreover, by interpreting embedded MTT terms in an internally constructed model of MTT, we can extract programs and proofs to the meta language and obtain interoperability between the embedded language and the metalanguage. The existing Sikkel library for Agda achieves this for Multimode Simple Type Theory (MSTT) with an internal presheaf model of dependent MTT. In this work, we add, on top of the simply-typed layer, a logical framework in which users can write multimode proofs about multimode Sikkel programs, still in an off-the-shelf proof assistant. To this end, we carve out of MTT a new multimode logical framework µLF over MSTT and implement it on top of Sikkel, interpreting both in the existing internal model. In the process, we further extend and improve the original codebase for each of the three layers (syntax, semantics and extraction) of Sikkel. We demonstrate the use of µLF by proving some properties about functions manipulating guarded streams and by implementing an example involving parametricity predicates.
@article{CeulemansND25,
title = {BiSikkel: A Multimode Logical Framework in Agda},
author = {Joris Ceulemans and Andreas Nuyts and Dominique Devriese},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704844}
}