\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.

The formalisation and verification described here was a significant task:
it was the major activity for an experienced Isabelle user (Dawson) 
for about seven months, not including
some months more working on the proof which ultimately was found to be flawed
(see \S\ref{s-intro}).
and not counting the proof of Thm~\ref{thm:cutad-verif}, reused from 
\cite{DBLP:conf/tphol/DawsonG02}.
The most difficult single part of it was the proof of Lemma~\ref{lm:permute},
discussed in \S\ref{sec:eqshallowdeep}.  
The difficulty in defining a nested sequent datatype containing multisets of
nested sequents (see \S\ref{sec:eqdlshallow}) was also significant.
The value of the formal verification is clear since it led
us to find the flaw in the previous attempt at a proof.

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
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 difference between these logics and $\fill$ is the
use of ``additive'' context splitting in branching
rules, where contexts are duplicated across premises. In the presence of contraction rules, our
multiplicative context splitting can simulate such additive splitting, just as in the traditional
sequent calculus. That is, one can apply contraction to duplicate every formula occurrence
in the context before splitting them.  
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: 
