\section{Conclusion and future work}
\label{sec:related}

Finding a cut-free sequent calculus for $\fill$ has been a notoriously
difficult problem, as we have reviewed in our introduction, and
involved candidate proof systems that turned out to be incomplete.
Indeed, our initial attempt at the soundness proof for one candidate
proof system was found to be flawed, only after we attempted to
formalise it in Isabelle/HOL.  Our formalisation finally establishes
convincingly that our deep nested calculus $\filldn$ is both sound and
complete for $\fill$.  Apart from our $\filldn$, all other
existing proof calculi for $\fill$ still require complex annotations
to ensure cut-elimination.

Taking a broader perspective, we have shown a detailed formalisation
of a methodology for deriving a deep nested sequent calculus for a
logic from its categorical semantics via a display calculus and a
shallow nested sequent calculus for a natural extension containing new
additional connectives. For future work, we plan to apply this same
formalised methodology to derive deep nested sequent calculi for a
wide range of
logics~\cite{Brunnler09AML,poggiolesi-tree-hypersequents,Gore10AiML,Gore11LMCS,Strassburger13,Park13}.
There are indications that a substantial part of our current
formalisation can be adapted to such logics.

A crucial difference between these logics and $\fill$ is the
additional structural rules of contraction and weakening. Contraction
and weakening give rise to ``additive'' context splitting in branching
rules, where contexts are duplicated across both premises. Our
multiplicative context splitting is actually more general and can
simulate such additive splitting, when contraction and weakening are
present. Thus we think a similar formalisation effort for, say, nested
sequent calculi for modal logics~\cite{Gore11LMCS}, would benefit
significantly from our current formalisation.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
