@InProceedings{altenkirch-formalization-LEGO,
  author =       {Thorsten Altenkirch},
  title =  
    {A Formalization of the Strong Normalization Proof for System F in LEGO},
  editor = 	 {Marc Bezem, Jan Frisco Groote},
  booktitle =    {Typed Lambda Calculi and Applications},
  pages = 	{13--28},
  series = {LNCS 664}, 
  year =         1993,
  publisher =    {Springer}
  }

@Unpublished{dawson-gore-machine-checked-strong-normalisation-lics,
  author =       {Jeremy E. Dawson and Rajeev Gore},
  title =        {A New Machine-checked Proof of Strong Normalisation 
                   for Display Logic},
  year =         2001,
  month =        {December},
  note =      {\url{http://discus.anu.edu.au/~rpg/CutElim/},
  Submitted to LICS-2002.}
}

@Book{elmasri-navathe-database,
  author =       {R~A Elmasri and S~B Navathe},
  title =        {Fundamentals of Database Systems},
  publisher =    {Benjamin/Cummings, Redwood City},
  year =         1994,
  edition =      {2nd}
}

@Book{HOL-introduction,
  author =       {M~J~C Gordon and T~F Melham},
  title =        {Introduction to HOL: a Theorem Proving Environment for Higher
		 Order Logic},
  publisher =    {Cambridge University Press},
  year =         1993
}

@Article{church-types,
  author =       {A Church},
  title =        {A formulation of the simple theory of types},
  journal =      {Journal of Symbolic Logic},
  year =         1940,
  volume =       5,
  pages =        {56-68}
}

@Article{mili-relational,
  author =       {A Mili},
  title =        {A relational approach to the design of deterministic
		  programs},
  journal =      {Acta Informatica},
  year =         1983,
  volume =       20,
  pages =        {315-328}
}

@Article{pym-harland-uniform,
  author =       {D Pym and J Harland},
  title =    
    {A Uniform Proof-theoretic Investigation of Linear Logic Programming},
  journal =      {J.\ of Logic and Computation},
  year =         1994,
  volume =       4,
  pages =        {175-207}
}

@TechReport{harrison-metatheory-reflection,
  author =       {J Harrison},
  title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
  year =         1995,
  number =       {CRC-053},
  institution =  {SRI International Cambridge Computer Science Research Centre},
  note =         {\url{http://www.abo.fi/~jharriso/}}
}

@Article{crossley-poernomo-fred,
  author =		 {J N Crossley and I Poernomo},
  title =		 {Fred: An approach to generating real, correct,
                  reusable programs from proofs},
  journal =		 {Journal of Universal Computer Science},
  year =		 2001,
  volume =		 7,
  number =		 1,
  note =         {\url{http://www.csse.monash.edu.au/~jnc/}},
  annote =		 {don't have}
}

@InCollection{kracht-power,
  author =       {M Kracht},
  title =        {Power and Weakness of the Modal Display Calculus},
  booktitle =    {Proof Theory of Modal Logics},
  publisher =    {Kluwer},
  year =         1996,
  editor =       {H Wansing},
  pages =        {92-121}
}

@InCollection{matthews-theory-metatheory,
  author =       {S Matthews},
  title =        {A Theory and its Metatheory in {FS$_0$}},
  booktitle =    {What is a logic system?},
  publisher =    {Oxford University Press},
  year =         1994,
  editor =       {Dov~M~Gabbay},
  pages =        {329-354}
}

@InProceedings{mikhajlova-vonwright-isomorphism,
  author =       {Anna Mikhajlova and Joakim von Wright},
  title =        {Proving Isomorphism of First-Order Proof Systems in {HOL}},
  editor = 	 {J Grundy and M Newey},
  booktitle =    {Theorem Proving in Higher-Order Logics},
  pages = 	{295--314},
  series = {LNCS 1479}, 
  year =         1998,
  publisher =    {Springer}
  }

@techreport{isabelle-object,
AUTHOR = " Lawrence C. Paulson",
TITLE = "Isabelle's Logics",
NOTE = "15 February 2001, \texttt{doc/logics.dvi}
in the Isabelle distribution"
}

@techreport{isabelle-ref,
AUTHOR = " Lawrence C. Paulson",
TITLE = "The Isabelle Reference Manual",
NOTE = "15 February 2001, \texttt{doc/ref.dvi}
in the Isabelle distribution"
}

@techreport{IsLogHOL,
AUTHOR = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
TITLE = "Isabelle's Logics: HOL",
NOTE = "15 February 2001, \texttt{doc/logics-HOL.dvi}
in the Isabelle distribution"
}