2 papers
cs.LO2026
Bounded Modal Logic: Explicit Scope Dependencies in Multi-Stage Programming
Yuito Murase, Akinori Maniwa
It is widely known that proof systems for modal logic can be interpreted as type systems for multi-stage programming (MSP). However, existing modal-logical foundations for MSP do n…
cs.LO2024
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
Akinori Maniwa, Ryo Kashima
The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby com…