@string{lncs = {LNCS}}
@string{lncslong = {Lecture Notes in Computer Science}}


@Book{TS00,
AUTHOR = "Troelstra, A. S. and Schwichtenberg, H.",
TITLE = "Basic Proof Theory",
EDITION = "second",
PUBLISHER = "Cambridge University Press",
YEAR = 2000,
SERIES = "Cambridge Tracts in Computer Science",
NUMBER = 43
}

@Book{BN99,
AUTHOR = "Baader, F. and Nipkow, T.",
TITLE = "Term Rewriting and All That",
PUBLISHER = "Cambridge University Press",
YEAR = 1999
}

@Book{SU05,
AUTHOR = "S{\"o}rensen, M. and Urzyczyn, P.",
TITLE = "Lectures on the {Curry-Howard Isomorphism}",
PUBLISHER = "Elsevier",
YEAR = 2006,
SERIES = "Studies in Logic and the Foundations of Mathematics",
NUMBER = 149
}



@article{Dyc92,
  author    = {Dyckhoff, R.},
  title     = {{Contraction-Free Sequent Calculi for Intuitionistic Logic}},
  journal   = {J. Symb. Log.},
  volume    = {57},
  number    = {3},
  year      = {1992},
  pages     = {795-807},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{Hud92,
  author    = {Hudelmaier, J.},
  title     = {{An O(n log n)-Space Decision Procedure for Intuitionistic
               Propositional Logic}},
  journal   = {J. Log. Comput.},
  volume    = {3},
  number    = {1},
  year      = {1993},
  pages     = {63-75}
}

@article{MM04,
  author    = {McBride, C. and
               McKinna, J.},
  title     = {{The View from the Left}},
  journal   = {J. Funct. Program.},
  volume    = {14},
  number    = {1},
  year      = {2004},
  pages     = {69-111},
  ee        = {https://doi.org/10.1017/S0956796803004829}
  }

@article{Pfe00,
  author    = {Pfenning, F.},
  title     = {{Structural Cut Elimination: I. Intuitionistic and Classical
               Logic}},
  journal   = {Inf. Comput.},
  volume    = {157},
  number    = {1-2},
  year      = {2000},
  pages     = {84-141}
 }


@misc{Rid06,
AUTHOR = "Ridge, T.",
TITLE = "{Craig's Interpolation Theorem formalised and mechanised in {I}sabelle/{HOL}}",
HOWPUBLISHED = "Arxiv preprint cs.LO/0607058, 2006 - arxiv.org"
}


@article{DM79,
  author    = {Dershowitz, N. and
               Manna, Z.},
  title     = {{Proving Termination with Multiset Orderings}},
  journal   = {Commun. ACM},
  volume    = {22},
  number    = {8},
  year      = {1979},
  pages     = {465-476}
}



@inproceedings{DKL06,
    author =  {Dyckhoff, R. and Kesner, D. and Lengrand, S.}, 
    title  =  {{Strong cut-elimination systems for Hudelmaier's depth-bounded
 sequent calculus for implicational logic}}, 
    booktitle = {Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06)},
    series = {LNAI},
    volume = {4130},
    publisher = {Springer-Verlag},
    editor = {U. Furbach and N. Shankar},
    year = {2006},
    month = aug,
    pages = {347--361},
}

@article{CT06,
  author    = {Ciabattoni, A. and
               Terui, K.},
  title     = {{Towards a Semantic Characterization of Cut-Elimination}},
  journal   = {Studia Logica},
  volume    = {82},
  number    = {1},
  year      = {2006},
  pages     = {95-119}
 }



@Book{NPW05,
AUTHOR = "Nipkow, T. and Paulson, L. and Wenzel, M.",
TITLE = "{A Proof Assistant for Higher-Order Logic}",
PUBLISHER = "Springer-Verlag",
YEAR = 2005,
SERIES = "Lecture Notes in Computer Science",
NUMBER = 2283
}

@inproceedings{Nip02,
  author    = {Nipkow, T.},
  title     = {{Structured Proofs in Isar/HOL}},
  booktitle = {TYPES},
  year      = {2002},
  pages     = {259-278}
}

@Manual{Wen02,
AUTHOR = "Wenzel, M.",
TITLE = "{Isabelle/Isar Reference Manual}",
YEAR = 2002
}

@Unpublished{Pau05,
AUTHOR = "Paulson, L.",
TITLE = "{Isabelle's Logics}",
YEAR = 2005,
NOTE = "{Available at} http://www.cl.cam.ac.uk/research/hvg/Isabelle"
}

@Manual{McB05,
AUTHOR = "McBride, C.",
TITLE = "Epigram: Practical Programming with dependent types"
}


@article{MT05,
  author    = {Miller, D. and
               Tiu, A.},
  title     = {{A Proof Theory for Generic Judgments}},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {6},
  number    = {4},
  year      = {2005},
  pages     = {749-783},
  ee        = {http://doi.acm.org/10.1145/1094622.1094628}
 }




@Book{Kle52,
AUTHOR = "Kleene, S. C.",
TITLE = "Introduction to Metamathematics",
PUBLISHER = "North-Holland Publishing Company",
YEAR = 1952
}

@phdthesis{Ada97,
AUTHOR = "Adams, A.",
TITLE = "Tools and Techniques for Machine-Assisted Meta-Theory",
SCHOOL ="University of St. Andrews",
YEAR = 1997
}

@manual{PS05,
AUTHOR = "Pfenning, F. and Schuermann, C.",
TITLE = "Twelf User's Guide",
YEAR = 2005
}

@misc{Hud98,
AUTHOR = "Hudelmaier, J.",
TITLE = "{Semantische Sequenzenkalk{\"u}le}",
YEAR = 1998,
NOTE = "Habilitationsschrift, Fakult{\"a}t f{\"u}r Informatik der Eberhard-Karls-{\"U}niversit{\"a}t T{\"u}bingen, Germany"
}

@book{Smu68,
AUTHOR = "Smullyan, R.",
TITLE = "First-order logic",
PUBLISHER = "Springer-Verlag",
YEAR = 1968
}

@unpublished{Cha07a,
AUTHOR = "Chapman, P.",
TITLE = "{An Automatic Prover for Sequent Calculus in {I}sabelle}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.dcs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2007
}

@unpublished{Cha07b,
AUTHOR = "Chapman, P.",
TITLE = "{Mechanising Craig's Interpolation Theorem for Intuitionistic Logic in {I}sabelle}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.dcs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2007
}

@inproceedings{CMU08,
  author    = {Chapman, P. and
               McKinna, J. and
               Urban, C.},
  title     = {{Mechanising a Proof of Craig's Interpolation Theorem for
               Intuitionistic Logic in Nominal Isabelle}},
  booktitle = {AISC/MKM/Calculemus},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5144},
  year      = {2008},
  pages     = {38-52}
 
 }



@BOOK{ML84,
AUTHOR = "Martin-L{\"o}f, P.",
TITLE = "Intuitionistic Type Theory",
PUBLISHER = "Bibliopolis",
YEAR = 1984,
SERIES = "Studies in Proof Theory",
NUMBER = 1
}

@BOOK{Tak75,
AUTHOR = "Takeuti, G.",
TITLE = "Proof Theory",
PUBLISHER = "North-Holland Publishing Company",
YEAR = 1975,
SERIES = "Studies in Logic and the Foundations of Mathematics",
NUMBER = 81
}

@misc{Bou96,
  author = "Boulm{\'e}, S.",
  title = "A {Proof of Craig's Interpolation Theorem} in {C}oq",
  YEAR = 1996,
  NOTE = "{A}vailable at citeseer.ist.psu.edu/480840.html"  }
  
@incollection{MP93,
    author = "McKinna, J. and  Pollack, R.",
    title = "{Pure Type Systems Formalized}",
    booktitle = "Proceedings 1st Int.\ Conf.\ on Typed Lambda Calculi and Applications, {TLCA}'93, Utrecht",
    volume = "664",
    publisher = "Springer-Verlag",
	SERIES = lncs,
    editor = "M. Bezem and J. F. Groote",
    pages = "289--305",
    year = 1993,
    url = "citeseer.ist.psu.edu/mckinna93pure.html" }
    
    
@unpublished{Cha07c,
AUTHOR = "Chapman, P.",
TITLE = "Mechanising Craig's Interpolation Theorem for Intuitionistic Logic in {I}sabelle, {Proof Script}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.dcs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2007
}

@unpublished{Cha07d,
AUTHOR = "Chapman, P.",
TITLE = "{First Year Report}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.dcs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2007
}

@unpublished{Cha08b,
AUTHOR = "Chapman, P.",
TITLE = "{Formalising Proofs of Cut Admissibility}",
NOTE = "{University of St Andrews Computer Science Research Report}",
YEAR = 2008
}

@unpublished{Cha08d,
AUTHOR = "Chapman, P.",
TITLE = "{A Formalisation of Contraction Admissibility for G4ip}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.cs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2008
}


@unpublished{Ch08,
AUTHOR = "Chapman, P.",
TITLE = "{Syntactic Conditions for Invertibility in Sequent Calculi}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.cs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2008
}

@unpublished{Cha08e,
AUTHOR = "Chapman, P.",
TITLE = "{A Formalised Proof of Cut Admissibility}",
NOTE = "{University of St Andrews Computer Science Research Report,} available at www.cs.st-andrews.ac.uk/{$\sim$}pc",
YEAR = 2008
}



@INPROCEEDINGS{TU05,
AUTHOR = "Tasson, C. and Urban, C.",
TITLE = "Nominal techniques in {I}sabelle/{HOL}",
BOOKTITLE = "{Proceedings of the 20th International Conference on Automated Deduction (CADE 2005)}",
YEAR = 2005,
PUBLISHER = "Springer-{V}erlag",
SERIES = lncs,
VOLUME = 3632,
PAGES = "38-53"

}

@article{Pit03,
 author = {Pitts, A. M.},
 title = {{Nominal Logic, a First-Order Theory of Names and Binding}},
 journal = {Inf. Comput.},
 volume = {186},
 number = {2},
 year = {2003},
 issn = {0890-5401},
 pages = {165--193},
 doi = {https://doi.org/10.1016/S0890-5401(03)00138-X},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }


@Manual{Coq,
AUTHOR = "{Coq Development Team}",
TITLE = "{The Coq Proof Assistant Reference Manual Version 8.1}",
YEAR = 2006,
NOTE = "{A}vailable at http://coq.inria.fr/V8.1/refman/index.html"

}


@misc{CXZ03,
  author = "Chen, C. and Zhu, D. and Xi, H.",
  title = "{Implementing Cut Elimination: A Case Study of Simulating Dependent Types
    in Haskell}",
  note = "{Available at: http://www.cs.bu.edu/$\sim$hwxi/academic/papers/CutElim.}",
  year = "2003",
  url = "citeseer.ist.psu.edu/article/chen03implementing.html" }
  
  @article{BU01,
  author    = {C. Urban and
               G. M. Bierman},
  title     = {Strong Normalisation of Cut-Elimination in Classical Logic},
  journal   = {Fundam. Inform.},
  volume    = {45},
  number    = {1-2},
  year      = {2001},
  pages     = {123-155}
}

  
  
  

@article{DN00,
  author    = {Dyckhoff, R. and
               Negri, S.},
  title     = {{Admissibility of Structural Rules for Contraction-Free Systems
               of Intuitionistic Logic}},
  journal   = {J. Symb. Log.},
  volume    = {65},
  number    = {4},
  year      = {2000},
  pages     = {1499-1518},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{JMX07,
  author    = {Jhala, R. and
               Majumdar, R. and
               Xu, R-G.},
  title     = {{State of the Union: Type Inference Via Craig Interpolation}},
   booktitle     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 13th International Conference, TACAS 2007, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2007 Braga, Portugal, March
               24 - April 1, 2007, Proceedings},
 
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4424},
 
  pages     = {553-567},
  ee        = {https://doi.org/10.1007/978-3-540-71209-1_43},
   year = {2007}
}

@inproceedings{McM05,
  author    = {McMillan, K. L.},
  title     = {{Applications of Craig Interpolants in Model Checking}},
 booktitle     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 11th International Conference, TACAS 2005, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8,
               2005, Proceedings},
 
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3440},
  year      = {2005},
  pages = {1-12}

}

@InProceedings{GP99,
 isbn = {0-7695-0158-3},
  author = 	 {Gabbay, J. and Pitts, A. M.},
  title = 	 {{A New Approach to Abstract Syntax Involving Binders}},
  booktitle = 	 {14th Annual Symposium on Logic in Computer Science},
  year = 	 1999,
  publisher =    {IEEE Computer Society Press},
 address = {Washington, DC, USA},
  pages = 	 {214--224},
 }
 
 @Book{BRV08,
AUTHOR = "Blackburn, P. and de Rijke, M. and Venema, Y.",
TITLE = "Modal Logic",

PUBLISHER = "Cambridge University Press",
YEAR = 2000,
SERIES = "Cambridge Tracts in Computer Science",
NUMBER = 53
}

 @article{ Vor70,
    author = "Vorob'ev, N.",
    title = "{A New Algorithm for Derivability in the Constructive Propositional Calculus}",
    journal = "American Mathematical Society Translations",
    pages = "37-71",
    year = "1970",
    volume = "94" }
    
@article{Ras07,
  author    = {Rasga, J.},
  title     = {{Sufficient conditions for cut elimination with complexity
               analysis}},
  journal   = {Ann. Pure Appl. Logic},
  volume    = {149},
  number    = {1-3},
  year      = {2007},
  pages     = {81-99}
 }

@article{Neg05,
  author    = {Negri, S.},
  title     = {{Proof Analysis in Modal Logic}},
  journal   = {Journal of Philosophical Logic},
  volume    = {34},
  year      = {2005},
  pages     = {507-544}
 }


@inproceedings{AZ06,
  author    = {Zamansky, A. and
               Avron, A.},
  title     = {{Canonical {G}entzen-Type Calculi with (n, k)-ary Quantifiers}},
  booktitle = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  year      = {2006},
  pages     = {251-265}
}

@inproceedings{CT07,
  author    = {Ciabattoni, A. and
               Terui, K.},
  title     = {{Modular Cut-Elimination: Finding Proofs or Counterexamples}},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning,
               13th International Conference, LPAR 2006, Phnom Penh, Cambodia,
               November 13-17, 2006, Proceedings},
  year      = {2006},
  pages     = {135-149}
}

@unpublished{Daw08,
author = {Dawson, J.E.},
title = {Isabelle Files},
year = {2008},
note = {Available at http://users.rsise.anu.edu.au/$\sim$jeremy/isabelle/}

}


@article{GP94,
  author    = {Galmiche, D. and
               Perrier, G.},
  title     = {{On Proof Normalization in Linear Logic}},
  journal   = {Theor. Comput. Sci.},
  volume    = {135},
  number    = {1},
  year      = {1994},
  pages     = {67-110}
}


@book{Res99,
	address = {London},
	author = {Restall, G.  },
	booktitle = {An Introduction to Substructural Logics},
	citeulike-article-id = {376124},
	keywords = {bibtex-import, logic},
	posted-at = {2005-11-02 00:24:05},
	priority = {0},
	publisher = {Routledge},
	title = {An Introduction to Substructural Logics},
	year = {1999}
}

@book{NvP01,
	Address = {Cambridge},
	Author = {Negri, S. and von Plato, J.},
	Publisher = {Cambridge University Press},
	Title = {Structural Proof Theory},
	Year = {2001}}

@article{LH05,
  author    = {Lutovac, T. and
               Harland, J.},
  title     = {{Issues in the Analysis of Proof-Search Strategies in Sequential
               Presentations of Logics}},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {125},
  number    = {2},
  year      = {2005},
  pages     = {115-147}
  
}

@book{Dra88,
AUTHOR = "Dragalin, A. G. ",
TITLE = "{Mathematical Intuitionism}",

PUBLISHER = "{American Mathematical Society}",
YEAR = 1988,
SERIES = "{Translations of Mathematical Monographs}",
NUMBER = 67
}

@inproceedings{Gha95,
  author    = {Ghani, N.},
  title     = {{\ss}n-Equality for Coproducts},
  booktitle = {Typed Lambda Calculi and Applications, Second International
               Conference on Typed Lambda Calculi and Applications, TLCA
               '95, Edinburgh, UK, April 10-12, 1995, Proceedings},
  year      = {1995},
  pages     = {171-185},
 publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {902}

}

@inproceedings{AL01,
  author = {Avron, A. and Lev, I.},
 
   title = {Canonical Propositional {G}entzen-Type Systems},
  booktitle     = {Automated Reasoning, First International Joint Conference,
               IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2083},
  year      = {2001}

}

@article{Avr91,
  author    = {Avron, A.},
  title     = {Simple Consequence Relations},
  journal   = {Inf. Comput.},
  volume    = {92},
  number    = {1},
  year      = {1991},
  pages     = {105-140}
}

@article{HOS94,
  author    = {Hori, R. and
               Ono, H. and
               Schellinx, H.},
  title     = {Extending Intutionistic Linear Logic with Knotted Structural
               Rules},
  journal   = {Notre Dame Journal of Formal Logic},
  volume    = {35},
  number    = {2},
  year      = {1994},
  pages     = {219-242}
}


@article{Bel82,
  author    = {Belnap Jr., N.},
  title     = {{Display Logic}},
  journal   = {Journal of Philosophical Logic},
  volume    = {11},
 
  year      = {1982},
  pages     = {375-417}
}

@book{Cur63,
AUTHOR = "Curry, H. B. ",
TITLE = "{Foundations of Mathematical Logic}",

PUBLISHER = "{McGraw-Hill Book Company}",
YEAR = 1963,
SERIES = "{McGraw-Hill Series in Higher Mathematics}"
}

@book{SS08,
AUTHOR = "Shoesmith, D.J. and Smiley, T. J. ",
TITLE = "{Multiple-Conclusion Logic}",

PUBLISHER = "{Cambridge University Press}",
YEAR = 2008
}

@unpublished{ChaIsa,
author = {Chapman,P.},
title = {Isabelle Files},
year = {2009},
note = {Available at www.cs.st-andrews.ac.uk/{$\sim$}pc/isabelle}

}


@article{Kan06,
  author    = {M. Kanazawa},
  title     = {Computing interpolants in implicational logics},
  journal   = {Ann. Pure Appl. Logic},
  volume    = {142},
  number    = {1-3},
  year      = {2006},
  pages     = {125-201}
 
}

@article{Gir87,
  author    = {J-Y. Girard},
  title     = {Linear Logic},
  journal   = {Theoretical Computer Science},
  volume    = {50},
  year      = {1987},
  pages     = {1-102}
}


@inproceedings{Bru06,
  author    = {K. Br{\"u}nnler},
  title     = {Deep Inference and Its Normal Form of Derivations},
  booktitle = {Logical Approaches to Computational Barriers, Second Conference
               on Computability in Europe, CiE 2006, Swansea, UK, June
               30-July 5, 2006, Proceedings},
  year      = {2006},
  pages     = {65-74},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3988}
 }


@article{Kle52b,
  author    = {Kleene, S. C.},
  title     = {Permutability of inferences in {G}entzen's calculi {LK} and {LJ}},
  journal   = {Memoirs of the American Mathematical Society},
  volume    = {10},
  year      = {1952},
  pages     = {1-26}
}

@article{DP99,
  author    = {R. Dyckhoff and
               L. Pinto},
  title     = {Permutability of Proofs in Intuitionistic Sequent Calculi},
  journal   = {Theor. Comput. Sci.},
  volume    = {212},
  number    = {1-2},
  year      = {1999},
  pages     = {141-155}
 }
 
 @inproceedings{Sha92,
  author    = {N. Shankar},
  title     = {Proof Search in the Intuitionistic Sequent Calculus},
  booktitle = {Automated Deduction - CADE-11, 11th International Conference
               on Automated Deduction, Saratoga Springs, NY, USA, June
               15-18, 1992, Proceedings},
  year      = {1992},
  pages     = {522-536},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {607}
}


@article{Gir91,
  author    = {J-Y. Girard},
  title     = {A New Constructive Logic: Classical Logic},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {1},
  number    = {3},
  year      = {1991},
  pages     = {255-296}
}

@inproceedings{DL06,
  author    = {R. Dyckhoff and
               S. Lengrand},
  title     = {LJQ: A Strongly Focused Calculus for Intuitionistic Logic},
  booktitle = {Logical Approaches to Computational Barriers, Second Conference
               on Computability in Europe, CiE 2006, Swansea, UK, June
               30-July 5, 2006, Proceedings},
  year      = {2006},
  pages     = {173-185},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3988}
 }


@book{Gen69,
AUTHOR = "Gentzen, G. ",
TITLE = "{The Collected Papers of {G}erhard {G}entzen}",

PUBLISHER = "{North-Holland Publishing Company}",
YEAR = 1969
}

@inproceedings{Nor09,
  author    = {U. Norell},
  title     = {Dependently typed programming in Agda},
  booktitle = {Proceedings of TLDI'08: 2008 ACM SIGPLAN International Workshop
               on Types in Languages Design and Implementation, Savannah,
               GA, USA, January 24, 2009},
  year      = {2009},
  pages     = {1-2},
  publisher = {ACM}
 }

@unpublished{epilogue,
 title = {Epilogue for Epigram},
 note = {Available at http://www.e-pig.org/epilogue/},
 author = {C. McBride}
}


@inproceedings{Cor07,
  author    = {P. Corbineau},
  title     = {A Declarative Language for the Coq Proof Assistant},
  booktitle = {Types for Proofs and Programs, International Conference,
               TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised
               Selected Papers},
  pages     = {69-84},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4941},
  year      = {2008}
  }


@article{CH88,
  author    = {T. Coquand and
               G. P. Huet},
  title     = {The Calculus of Constructions},
  journal   = {Inf. Comput.},
  volume    = {76},
  number    = {2/3},
  year      = {1988},
  pages     = {95-120}
}

@inproceedings{PP89,
  author    = {F. Pfenning and
               C. Paulin-Mohring},
  title     = {Inductively Defined Types in the Calculus of Constructions},
  booktitle = {Mathematical Foundations of Programming Semantics},
  year      = {1989},
  pages     = {209-228},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {442}
}

@Book{BC04,
  author       = "Bertot, Y. and Cast\'eran, P.",
  title        = "{Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions}",
  series       = "Texts in Theoretical Computer Science",
  year         = "2004",
  publisher    = "Springer Verlag",
  url          = "http://www.labri.fr/publications/l3a/2004/BC04"
}


@unpublished{mizar,
 title = {Mizar website},
 note = {Available at http://www.mizar.org/},
 author = {Mizar team}
}

@article{ABW07,
  author    = {B. E. Aydemir and
               A. Bohannon and
               S. Weirich},
  title     = {Nominal Reasoning Techniques in Coq: (Extended Abstract)},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {174},
  number    = {5},
  year      = {2007},
  pages     = {69-77},
  ee        = {https://doi.org/10.1016/j.entcs.2007.01.028}
}

@inproceedings{Wen06,
  author    = {M. Wenzel},
  title     = {Structured Induction Proofs in Isabelle/Isar},
  booktitle = {Mathematical Knowledge Management, 5th International Conference,
               MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings},
  year      = {2006},
  pages     = {17-30},
   publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4108}
}

@article{deB72,
  author    = {N. G. de Bruijn},
  title     = {Lambda Calculus Notation with nameless dummies, a tool for automatic formula manipulation with application to the Church-Rosser Theorem},
  journal   = {Indagationes Mathematicae},
  volume    = {34},
  number    = {5},
  year      = {1972},
  pages     = {381-392},
  ee        = {https://doi.org/10.1016/j.entcs.2007.01.028}
}

@PHDTHESIS{Ras02,
    author       = {T. M. Rasmussen},
    title        = {Interval logic. Proof theory and theorem proving},
    year         = {2002},
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}"
    
}


@inproceedings{DG02,
  author    = {J. E. Dawson and
               R. Gor{\'e}},
  title     = {Formalised Cut Admissibility for Display Logic},
  booktitle = {Theorem Proving in Higher Order Logics, 15th International
               Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23,
               2002, Proceedings},
  year      = {2002},
  pages     = {131-147},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2410}
}

@article{DG01,
  author    = {J. E. Dawson and
               R. Gor{\'e}},
  title     = {Embedding Display Calculi into Logical Frameworks: Comparing
               Twelf and Isabelle},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {42},
  year      = {2001},
  ee        = {http://www.elsevier.nl/locate/entcs/volume42.html}
 
}

@inproceedings{UZ08,
  author    = {C. Urban and
               B. Zhu},
  title     = {Revisiting Cut-Elimination: One Difficult Proof Is Really
               a Proof},
  booktitle = {Rewriting Techniques and Applications, 19th International
               Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008,
               Proceedings},
  year      = {2008},
  pages     = {409-424},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5117}
}


@PHDTHESIS{Urb00,
    author       = {C. Urban},
    title        = {Classical Logic and Computation},
    year         = {2000},
    school       = "Cambridge University"
    
}

@PHDTHESIS{Sch00,
    author       = {C. Sch{\"u}rmann},
    title        = {Automating the Meta Theory of Deductive Systems},
    year         = {2000},
    school       = "Carnegie Mellon University"
    
}

@inproceedings{BNU07,
  author    = {C. Urban and
               S. Berghofer and
               M. Norrish},
  title     = {Barendregt's Variable Convention in Rule Inductions},
  booktitle = {Automated Deduction - CADE-21, 21st International Conference
               on Automated Deduction, Bremen, Germany, July 17-20, 2007,
               Proceedings},
  year      = {2007},
  pages     = {35-50},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603}
}

@book{Bar81,
 author = {H. Barendregt},
 title = {The Lambda Calculus: Its Syntax and Semantics},
 publisher = {Elsevier},
 series = {Studies in Logic and the Foundations of Mathematics},
 number = {103},
 year = {1981}
}

@inproceedings{HL09,
  author    = {H. Herbelin and
               G. Lee},
  title     = {Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic
               Sequent Calculus},
  booktitle = {Logic, Language, Information and Computation, 16th International
               Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings},
  year      = {2009},
  pages     = {209-217},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5514}
}


@inproceedings{BDN09,
  author    = {A. Bove and
               P. Dybjer and U. Norell},
  title     = {A Brief Overview of Agda - Functional Programming with Dependent Types},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International
               Conference, TPHOLs 2009, Munich, Germany, August 17-20,
               2009, Proceedings},
  year      = {2009},
  pages     = {?},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {?}
}

@book{Sch77,
 author = {K. Sch{\"u}tte},
 title = {Proof Theory},
 publisher = {Springer-Verlag},
  year = {1977}
}

@book{AZ03,
 author = {M. Aigner and G. M . Ziegler},
 title = {Proofs from the Book},
 publisher = {Springer-Verlag},
  year = {2003}
}

@article{Son75,
 author = {O. Sonobe},
 title = {{A Gentzen-type formulation of some intermediate propositional logics}},
 journal = {Journal of Tsuda College},
 year = {1975},
 volume = {7}


}
