modal-logics
Agda formalisation associated to the paper "Dual-context Calculi for Modal Logic." A preprint can be found at
https://arxiv.org/abs/1602.04860
Contains basic metatheoretic results about dual-context calculi (e.g. admissibility of weakening, contraction, cut) as well as proofs of equivalence with the relevant Hilbert systems (up to provability only).