BiSikkel: A Multimode Logical Framework in Agda

Explore a 20-minute conference talk from POPL 2025 that introduces BiSikkel, a multimode logical framework implemented in Agda. Learn how researchers from KU Leuven have extended the existing Sikkel library to support multimode proofs about multimode programs within an off-the-shelf proof assistant. The presentation demonstrates how embedding Multimode Type Theory (MTT) as a library enables additional reasoning principles without compromising soundness or compatibility. Discover how BiSikkel carves out a new multimode logical framework (LF over MSTT) from MTT and implements it on top of Sikkel, interpreting both in an existing internal model. The talk showcases practical applications through examples of proving properties about functions manipulating guarded streams and implementing parametricity predicates. The presented work includes reusable artifacts available through Zenodo, making it accessible for further research and experimentation in type theory and proof assistants.