I encoded the multi-type deduction calculus for DEL in the proof assistant Isabelle with the aim of generating derivations of inferences in the calculus. Specifically, it involved expanding, improving and modifying a prior implementation of a simpler calculus so as to build a software tool for the multi-type calculus.
Multi-type Display Calculus in Isabelle
calculus embedding