%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \bibliographystyle{plain}

% \bibliography{../ce,/home/discus/disk1/rpg/bib/fm,/home/discus/disk1/rpg/bib/modal,/home/discus/disk1/rpg/bib/mtl,/home/discus/disk1/rpg/bib/logic,/home/discus/disk1/rpg/bib/tl,/home/discus/disk1/rpg/bib/paracon,/home/discus/disk1/rpg/bib/linear,/home/discus/disk1/rpg/bib/algebra,/home/discus/disk1/rpg/bib/relevant,/home/discus/disk1/rpg/bib/dl,/home/discus/disk1/rpg/bib/atp}

\begin{thebibliography}{10}

\bibitem{belnap-display}
N~D {Belnap}.
\newblock Display logic.
\newblock {\em J.\ of Philosophical Logic}, 11:375--417, 1982.

% \bibitem{borisavljevic-dosen-petric-permuting-cut-with-contraction}
% M Borisavljevic, K Dosen, and Z Petric.
% \newblock On permuting cut with contraction.
% \newblock {\em Mathematical Structures in Computer Science}, 10:99--136, 2000.

% \bibitem{church-types}
% A~Church.
% \newblock A formulation of the simple theory of types.
% \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.

\bibitem{fill-csl}
\newblock
Ranald Clouston, Jeremy Dawson, Rajeev Gor\'e \& Alwen Tiu.
\newblock Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic.
\newblock In Proc.\ CSL, 2013. DETAILS

\bibitem{dawson-gore-embedding-comparing}
J~E Dawson and R Gor{\'e}.
\newblock Embedding display calculi into logical frameworks: Comparing {T}welf
  and {I}sabelle.
\newblock {\em ENTCS} 42, 89--103.
%\newblock In C~Fidge (Ed), {\em Proc.\ CATS 2001}, {\em ENTCS}, 42:89--103,
% \url{http://www.elsevier.nl/gej-ng/31/29/23/68/show/Products/notes/cover.htt},
2001. Elsevier.

\bibitem{dawson-gore-cut-admissibility}
J~E Dawson and R Gor{\'e}.
\newblock Formalised Cut Admissibility for Display Logic. 
\newblock In Proc.\ TPHOLS'02, LNCS 2410, 131--147, Springer, 2002.

% \bibitem{dawson-gore-machine-checked-strong-normalisation}
% Jeremy~E.~Dawson and Rajeev Gor{\'e}.
% A New Machine-checked Proof of Strong Normalisation for Display Logic.
% In Computing: The Australasian Theory Symposium, 2003, ENTCS 78, 16--35, Elsevier.

\bibitem{abella-gacek}
A~Gacek.
\newblock The Abella interactive theorem prover (system description)
\newblock In Proc.\ IJCAR 2008 LNCS~5195:154-161, Springer, 2008.

\bibitem{HOL-introduction}
M~J~C Gordon and T~F Melham.
\newblock {\em Introduction to {HOL}: a Theorem Proving Environment for Higher
  Order Logic}.
\newblock Cambridge University Press, 1993.

\bibitem{gore-india}
R~Gor\'e.
Invited talk in the Third Indian Conference on Logic and its
Applications, Chennai, January 2009.

\bibitem{gr-valentini}
R~Gor\'e and R~Ramanayake.
Valentini's Cut-elimination for Provability Logic Resolved.
Proc.\ AiML 2008, pp 67-86, College Publications
\url{http://users.rsise.anu.edu.au/~rpg/publications.html}

% \bibitem{gore-relalg}
% R~Gor{\'{e}}.
% \newblock Cut-free display calculi for relation algebras.
% \newblock In Proc.\ CSL96, LNCS 1258, 198--210, Springer, 1997.

\bibitem{Lei81}
D~Leivant. 
\newblock On the Proof Theory of the Modal Logic for Arithmetic Provability.
Journal of Symbolic Logic, 46:531–538, 1981.

\bibitem{mints-jaegerfest}
Grigori Mints.
\newblock Two Examples of Cut-Elimination for Non-classical Logics.
(talk, set of slides).
\newblock J\"agerfest, Bern (?), December 2013

\bibitem{moen} 
A~Moen. 
\newblock The proposed algorithms for eliminating cuts in the
provability calculus GLS do not terminate. 
\newblock NWPT 2001, Norwegian Computing Center, 2001-12-10
  \url{http://publ.nr.no/3411}

\bibitem{IsLogHOL}
T Nipkow, L~C. Paulson, and M Wenzel.
\newblock Isabelle's logics: {HOL}.
\newblock Technical report.
\newblock 15 February 2001, \texttt{doc/logics-HOL.dvi} in the Isabelle
  distribution.

\bibitem{isabelle-ref}
L~C. Paulson.
\newblock The {Isabelle} reference manual.
\newblock Technical report.
\newblock 15 February 2001, \texttt{doc/ref.dvi} in the Isabelle distribution.

\bibitem{pfenning-structural-lics94}
F Pfenning.
\newblock Structural cut elimination.
\newblock In {\em Proc.\ LICS 94}, 1994.

\bibitem{pym-harland-uniform}
D. Pym and J. Harland.
\newblock A Uniform Proof-theoretic Investigation of Linear Logic Programming.
\newblock J.\ of Logic and Computation 4:2:175-207, 1994.

\bibitem{twelf-system}
F~Pfenning and C~Schürmann. 
\newblock System description:
           Twelf --- a meta-logical framework for deductive systems. 
\newblock In Proc.\ CADE-16, pages 202--206, Springer-Verlag LNAI 1632.

\bibitem{Sol76}
R~M~Solovay. 
\newblock Provability Interpretations of Modal Logic. Israel Journal
of Mathematics, 25:287–304, 1976.

\bibitem{Val83}
S~Valentini. 
\newblock The Modal Logic of Provability: Cut-elimination. Journal of
Philosophical Logic, 12:471–476, 1983.

\bibitem{wansing-displaying-modal-logic}
H Wansing.
\newblock {\em Displaying Modal Logic}, volume~3 of {\em Trends in Logic}.
\newblock Kluwer Academic Publishers, Dordrecht, August 1998.

\end{thebibliography}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
