BiSikkel: A Multimode Logical Framework in Agda

on YouTube ↗20m

" summary

Library implements a multimode logical framework (MULF) on top of the existing Sikkel Agda stack, giving a syntactic MST layer, presheaf semantics and a checker that returns semantic denotations; it supports intrinsically typed MST terms, an extrinsically checked proof language, and a proof extraction to Set pipeline that yields ordinary Agda code when a mode is interpreted as the set model. Implementation reworks normalization, substitution and coherence; examples include guarded-stream proofs, but complex extractions currently hit Agda performance limits.

AI-written summary · about

" chapters (12)

1. 0:00Introduction to modalities
2. 1:10Internalizing morphisms as modalities
3. 3:41Implementing modal type theory
4. 5:49Sikkel library in Agda
5. 7:33Extending Sikkel
6. 8:58Guarded recursion example
7. 11:29Multimode framework structure
8. 13:35Soundness in Bicycle
9. 15:01Program and proof extraction
10. 16:49Design choices and limits
11. 17:31Summary and future work
12. 17:53Q&A