Bibliography on Logical Frameworks in BibTeX format

Editor: Frank Pfenning, fp at cs.cmu.edu
Last Updated: Tue Aug  3 1999
Size: 449 entries

This is a bibliography on logical frameworks.  I am including systems
specifically designed as logical frameworks as well as individual experiments
carried out in other systems which have a meta-logical character.  General
purpose theorem provers such as Coq, LEGO, Nqthm, NuPrl and others have been
omitted in order to keep my task managable, except for a basic reference or
two.  I generally followed the generic BibTeX conventions, using the bibtex.el
library for Emacs.  I have some lightweight tools to convert this to HTML
format for inclusion on the World-Wide Web, and to generate subsets based on
keywords, authors, etc.  Drop me a line if you are interested in these tools.
An HTML formatted version of this bibliography should be accessible under
 http://www.cs.cmu.edu/~fp/lfs-bib.html
Entries contain URL's where available which in many cases should allow
one to preview papers directly simply by following hypertext links.
Some conventions I used are detailed below.

This, like any bibliography, is incomplete.  Any corrections, updates,
comments, suggestion, new entries, new URL's for papers, etc. are very much
appreciated.

Entry Names: Last name of the first author, followed by year of publication.
  If this is ambiguous, I added a descriptive suffix (e.g. lics, cade,
  tr [techreport], phd [phdthesis]).  If it's still ambiguous I added
  a single letter a, b, etc.  According to common convention, auxiliary
  words are now added to the key as in `deBruijn' or `vandePol'.

Field Format: All fields are delimited by double-quotes or single symbols.
  This tremendously simplifies various Emacs functions for search and display.
  Diacritical marks must therefore be enclosed in {} so that BibTeX is not
  confused about the extent of the field (e.g. "Bengt Nordstr{\"o}m").

Strings: I did not use any strings or abbreviations so that each entry is
  self-contained and may be copied to other bibliography files.

url = "..."  If the paper's publication venue is on the
  World-Wide Web (for example, in an electronic journal or
  proceedings), this is the URL to locate it.  I have a style
  which interpret this field produce an appropriate hypertext
  reference for later conversion to HTML.

urlhtml = "..."
urldvi = "..."
urlps = "..."   More specific fields than url containing direct pointers
  to a HTML, DVI, or PostScript file where available, even if this paper
  is not published primarily on the Web.  Several may be present.

keywords = "k1, ..., kn" Indexing papers on a reasonably expressive set of
  keywords is very hard, so I refrained from doing it.  If a paper was clearly
  relevant to one or more of the `standard' frameworks listed below I used
  them as keywords, separated by commas.  Here is the complete current list of
  keywords:
	ALF            --- related to ALF
	Automath       --- related to Automath
	Elf            --- related to Elf (more specific than LF)
	FS0            --- related to FS0
	Isabelle       --- related to Isabelle
	lambda-Prolog  --- related to lambda-Prolog
	LF             --- related to (Edinburgh) LF
	linear         --- related to substructural frameworks
	misc           --- everything else
	Pi             --- related to Pi (partial induction)
	rewriting      --- related to rewriting and logical frameworks
	unification    --- related to unification and logical frameworks
  Using the Emacs tools I mentioned above, it is easy to extract all entries
  matching one of these keywords.  These will not show up on the LaTeX
  or HTML formatted versions of the bibliography.  Suggestions on how to
  do this gracefully would be appreciated!

author = "..."  Full names as far as available in <first name> <last name>
  format.

title = "..." Capitalized according to standard (American?) convention.  This
  will be de-capitalized for most bibliography styles as appropriate.

booktitle = "..."  For conferences I used "Proceedings of the ..." instead of
  the way the title sometimes appears on the cover ("Automated Deduction, 11th
  International Conference, Proceedings")

month = ...  Here is recently changed to using standard abbreviations
  jan feb mar apr may jun jul aug sep oct nov dec as recommended in the
  BibTeX documentation, since it allows uniform formatting in different
  styles.

year = "..." For a conference, the year of the conference and not necessarily
  the year in which the proceedings appeared.

address = "..." For a conference or workshop, the location where it was held.
  Otherwise the address of the publisher or institution.

publisher = "..." For Springer lecture notes I used "Springer-Verlag LNCS nnn"
  instead of the cumbersome and verbose series and number fields.


@InCollection{Aczel91,
  author =	"Peter Aczel and David P. Carlisle and Nax Mendler",
  title =       "Two Frameworks of Theories and Their Implementation in
		  {Isabelle}",
  booktitle =	"Logical Frameworks",
  publisher =	"Cambridge University Press",
  year =	"1991",
  editor =	"G. Huet and G. Plotkin",
  pages =	"3--39",
  keywords =	"Isabelle"
}

@InProceedings{Agerholm97,
  author = 	 "Sten Agerhold and Jacob Frost",
  title = 	 "An {Isabelle}-based Theorem Prover for {VDM-SL}",
  editor =	 "E. Gunter and A. Felty",
  pages =        "1--16",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
                  Proving in Higher Order Logics (TPHOLs'97)",
  address =      "Murray Hill, New Jersey",
  year =	 1997,
  month =	 aug,
  keywords =	 "Isabelle"
}

@PhdThesis{Altenkirch93phd,
  author = 	"Thorsten Altenkirch",
  title = 	"Constructions, Inductive Types and Strong Normalization",
  school = 	"University of Edinburgh",
  year = 	"1993",
  month =	nov,
  note =	"Available as Technical Report CST-106-93",
  keywords =	"misc"
}

@InProceedings{Altenkirch93tlca,
  author = 	"Thorsten Altenkirch",
  title = 	"A Formalization of the Strong Normalization Proof for {System
		  F} in {LEGO}", 
  booktitle = 	"Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications", 
  address =	"Utrecht, The Netherlands",
  month =	mar,
  year = 	"1993",
  pages =	"13--28",
  editor = 	"M. Bezem and J.F. Groote",
  publisher = 	"Springer-Verlag LNCS 664",
  keywords =	"misc"
}

@Manual{Altenkirch94,
  title = 	 "A User's Guide to {ALF}",
  author =	 "Thorsten Altenkirch and Veronica Gaspes and Bengt
		  Nordstr{\"o}m and Bj{\"o}rn von Sydow", 
  organization = "Chalmers University of Technology",
  address =	 "Sweden",
  year =	 1994,
  month =	 may,
  keywords =	 "ALF",
  urlps =	 "file://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z"
}

@InProceedings{Altenkirch96,
  author = 	 "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
  title = 	 "Reduction-Free Normalization for a Polymorphic System",
  editor =	 "E. Clarke",
  pages =	 "98--106",
  booktitle =	 "Proceedings of the 11th Annual Symposium on Logic in
                  Computer Science",
  year =	 1996,
  publisher =	 "IEEE Computer Society Press",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "misc"
}

@InProceedings{Artemov99cade,
  author = 	 "Sergei N. Artemov",
  title = 	 "On Explicit Reflection in Theorem Proving and Formal
		  Verification",
  editor =	 "Harald Ganzinger",
  pages =	 "267--281",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNAI 1632",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "misc"
}

@PhdThesis{Anderson93,
  author =	"Penny Anderson",
  title	=	"Program Derivation by Proof Transformation",
  school =	"Carnegie Mellon University",
  month	=	oct,
  year =	"1993",
  note =	"Available as Technical Report CMU-CS-93-206",
  url =  	"ftp://babar.inria.fr/pub/croap/anderson/thesis",
  keywords =	"LF, Elf"
}

@InProceedings{Anderson94cade,
  author =	"Penny Anderson",
  title	=	"Representing Proof Transformations for Program Optimization",
  booktitle =	"Proceedings of the 12th International Conference on Automated
		  Deduction",
  address =	"Nancy, France",
  publisher =	"Springer-Verlag LNAI 814",
  month	=	jun,
  year =	"1994",
  pages =       "575--589",
  url =	        "ftp://babar.inria.fr/pub/croap/anderson/cade94",
  keywords =	"LF, Elf"
}

@InProceedings{Anderson94lpar,
  author =	"Penny Anderson",
  title	=	"Program Extraction in a Logical Framework Setting",
  booktitle =	"Proceedings of the 5th International Conference on Logic
		  Programming and Automated Reasoning",
  editor =      "Frank Pfenning",
  publisher =	"Springer-Verlag LNAI 822",
  address =	"Kiev, Ukraine",
  month	=	jul,
  year =	"1994",
  pages =	"144--158",
  urlhtml =	"ftp://babar.inria.fr/pub/croap/anderson/lpar94",
  keywords =	"LF, Elf"
}

@InProceedings{Appel99ccs,
  author = 	 "Andrew W. Appel and Edward W. Felten",
  title = 	 "Proof-Carrying Authentication",
  editor =	 "G. Tsudik",
  booktitle =	 "Proceedings of the 6th Conference on Computer and
		  Communications Security",
  year =	 1999,
  publisher =	 "ACM Press",
  address =	 "Singapore",
  month =	 nov,
  note =	 "To appear",
  keywords =	 "LF, Elf"
}

@InProceedings{Appel99iclp,
  author = 	 "Andrew W. Appel and Amy P. Felty",
  title = 	 "Lightweight Lemmas in Lambda Prolog",
  editor =	 "Danny De Schreye",
  booktitle =	 "Proceedings of the International Conference on Logic
		  Programming (ICLP'99)",
  year =	 1999,
  publisher =	 "MIT Press",
  address =	 "Las Cruces, New Mexico",
  month =	 dec,
  note =	 "To appear",
  keywords =	 "lambda-Prolog, LF, Elf"
}

@Unpublished{Appel99un,
  author = 	 "Andrew W. Appel and Amy P. Felty",
  title = 	 "A Semantic Model of Types and Machine Instructions for
		  Proof-Carrying Code",
  note = 	 "Submitted",
  year =	 1999,
  month =	 jul,
  keywords =	 "LF, Elf"
}

@InProceedings{Argon96,
  author = 	 "Pablo Arg{\'o}n and John Mullins and Olivier Roux",
  title = 	 "A Correct Compiler Construction Using {Coq}",
  editor =	 "Didier Galmiche",
  pages = 	 "3--12",
  booktitle =	 "Informal Proceedings of the Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1996,
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =     "misc"
}

@Misc{Aspinall91,
  author = 	"David R. Aspinall",
  title = 	"{Isabelle Modules}: a New Theory Mechanism for {Isabelle}",
  howpublished = 	"Undergraduate dissertation, University of Cambridge",
  year = 	1991,
  keywords =	"Isabelle"
}

@InProceedings{Aspinall96,
  author = 	 "David Aspinall and Adriana Compagnoni",
  title = 	 "Subtyping Dependent Types",
  editor =	 "E. Clarke",
  pages =	 "86--97",
  booktitle =	 "Proceedings of the 11th Annual Symposium on Logic in
                  Computer Science",
  year =	 1996,
  publisher =	 "IEEE Computer Society Press",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "LF"
}

@InProceedings{Avenhaus94,
  author =	"J{\"u}rgen Avenhaus and Carlos Lor{\'\i}a-S{\'a}enz",
  title =	"Higher Order Conditional Rewriting and Narrowing",
  editor =	"J.-P. Jouannaud",
  booktitle =	"Proceedings of the First International Conference on
		  Constraints in Computational Logics",
  year =	1994,
  address =	"Munich, Germany",
  month =	sep,
  pages =       "269--284",
  publisher =   "Springer-Verlag LNCS 845",
  keywords = 	"rewriting"
}

@Article{Avron92,
  author = 	"Arnon Avron and Furio A. Honsell and Ian A. Mason and Robert
		  Pollack",
  title = 	"Using Typed Lambda Calculus to Implement Formal Systems on a
		  Machine",
  journal =	"Journal of Automated Reasoning",
  year =	1992,
  volume =	9,
  number =	3,
  pages =       "309--354",
  note =        "A preliminary version appeared as University of Edinburgh
		  Report ECS-LFCS-87-31",
  keywords = 	"LF"
}

@InProceedings{Ballarin95,
  author = 	 "Clemens Ballarin and Karsten Homann and Jacques Calmet",
  title = 	 "Theorems and Algorithms: An Interface between {Isabelle} and
		  {Maple}",
  booktitle = 	 "International Symposium on Symbolic and Algebraic
		  Computation",
  editor =	 "A. H. M. Levelt",
  year =	 1995,
  publisher =	 "ACM Press",
  pages =	 "150--157",
  keywords =     "Isabelle",
  urlps = 	 "http://iaks-www.ira.uka.de/iaks-calmet/papers/issac-95.ps.gz"
}

@InProceedings{Ballarin98,
  author = 	 "Clemens Ballarin and Lawrence C. Paulson",
  title = 	 "Reasoning about Coding Theory: The Benefits We Get from
		  Computer Algebra",
  editor =	 "J. Calmet and J. Plaze",
  pages =	 "55--66",
  booktitle =	 "Proceedings of the International Conference on Artificial
		  Intelligence and Symbolic Computation (AISC'98)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNAI 1476",
  address =	 "Plattsburgh, New York",
  month =	 sep,
  keywords =	 "Isabelle",
  urldvi =	 "http://www.cl.cam.ac.uk/users/lcp/papers/aisc98.dvi.gz"
}

@InCollection{Barendregt92,
  author = 	 "Henk P. Barendregt",
  title = 	 "Lambda Calculi With Types",
  booktitle =	 "Handbook of Logic in Computer Science",
  publisher =	 "Oxford University Press",
  year =	 1992,
  editor =	 "S. Abramsky and D. Gabbay and T.S.E. Maibaum",
  volume =	 2,
  chapter =	 2,
  pages =	 "117--309",
  keywords =	 "misc"
}

@InProceedings{Basin91,
  author =	"David Basin and Doug Howe",
  title =	"Some Normalization Properties of {Martin-L\"of's} Type
		  Theory, and Applications",
  booktitle =	"Theoretical Aspects of Computer Software",
  address =	"Sendai, Japan",
  month =	sep,
  year =	1991,
  publisher =	"Springer-Verlag LNCS 526",
  pages =	"475--494",
  keywords =	"misc"
}

@InCollection{Basin93le,
  author =	"David A. Basin and Robert L. Constable",
  title =       "Metalogical Frameworks",
  booktitle =   "Logical Environments",
  publisher =   "Cambridge University Press",
  year =        1993,
  editor =      "G. Huet and G. Plotkin",
  pages =       "1--29",
  keywords = 	"misc"
}

@InProceedings{Basin93ssd,
  author =	"David A. Basin and Alan Bundy and Ina Kraan and Se{\'a}n
		  Matthews",
  title =	"A Framework for Program Development Based on Schematic Proof",
  booktitle =	"Proceedings of the 7th International Workshop on Software
		  Specification and Design",
  publisher =	"IEEE Computer Society Press",
  year =	1993,
  pages =	"162--171",
  keywords = 	"Isabelle"
}

@InProceedings{Basin94iclp,
  author = 	 "David A. Basin",
  title = 	 "{IsaWhelk}: {Whelk} Interpreted in {Isabelle}",
  editor =	 "Pascal Van Hentenryck",
  pages =	 741,
  booktitle =	 "Proceedings of the Eleventh International Conference on
		  Logic Programming",
  year =	 1994,
  publisher =	 "MIT Press",
  address =	 "Genoa, Italy",
  month =	 jun,
  note =	 "Abstract",
  keywords =	 "Isabelle",
  urldvi =	 "ftp://mpi-sb.mpg.de/pub/papers/conferences/Basin-ICLP94.dvi.Z"
}

@InProceedings{Basin94lopstr,
  author =	"David A. Basin",
  title =	"Logic Frameworks for Logic Programs",
  booktitle =	"4th International Workshop on Logic Program Synthesis and
		  Transformation",
  publisher =	"Springer-Verlag LNCS 883",
  address =     "Pisa, Italy",
  month =       jun,
  year =	1994,
  pages =       "1--16",
  urlps =       "http://www.mpi-sb.mpg.de/guide/staff/basin/pubs/lopstr94.ps.Z",
  keywords = 	"Isabelle"
}

@InProceedings{Basin95,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "A Modular Presentation of Modal Logics in a Logical
                  Framework",
  editors =      "J. Ginzburg and Z. Khasidashvili and C. Vogel and
		  J.-J. L{\'e}vy and E. Vallduv{\'\i}",
  booktitle =	 "The Tbilisi Symposium on Language, Logic and
                  Computation: Selected Papers",
  year =	 1998,
  publisher =    "CSLI Publications",
  notes =        "Selected papers from the symposium in Tblisi, Georgia,
		  October 1995",
  keywords =	 "Isabelle",
  url     =		 "http://www.mpi-sb.mpg.de/~luca/Publications/ampomlialf.ps"
}

@InProceedings{Basin96cade,
  author = 	 "David Basin and Se{\'a}n Matthews",
  title = 	 "Structuring Metatheory on Inductive Definitions",
  editor =	 "M.A. McRobbie and J.K. Slaney",
  pages =	 "171--185",
  booktitle =	 "Proceedings of the 13th International Conference on
		  Automated Deduction (CADE-13)",
  year =	 1996,
  publisher =	 "Springer-Verlag LNAI 1104",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "FS0"
}

@InProceedings{Basin96frocos,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "A Topography of Labelled Modal Logics",
  editor =	 "F. Baader and K.U. Schulz",
  pages =        "75--92",
  booktitle =	 "Proceedings of the First International Workshop on Frontiers
                  of Combining Systems (FroCoS'96)",
  year =	 1996,
  publisher =	 "Kluwer Academic Publishers",
  month =	 mar,
  keywords =	 "Isabelle",
  urlps =	 "http://www.mpi-sb.mpg.de/guide/staff/basin/pubs/frocos96.ps.Z"
}

@InProceedings{Basin96kr,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "Implementing Modal and Relevance Logics in a Logical
		  Framework",
  editor =	 "L.C. Aiello and J. Doyle and S.C. Shapiro",
  pages =	 "386--397",
  booktitle =	 "Proceegins of the Fifth International Conference on
		  Knowledge Representation and Reasoning (KR'96)",
  year =	 1996,
  publisher =	 "Morgan Kaufmann Publishers",
  keywords =	 "Isabelle"
}

@Article{Basin97jlc,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "Labelled Propositional Modal Logics: Theory and Practice",
  journal =	 "Journal of Logic and Computation",
  year =	 1997,
  volume =	 7,
  number =	 6,
  pages =	 "685--717",
  keywords =	 "misc"
}
		  
@InProceedings{Basin97ki,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "Labelled Quantified Modal Logics",
  editor =	 "G. Brewka and C. Habel and B. Nebel",
  pages =	 "171--182",
  booktitle =	 "Proceedings of the 21st German Annual Conference on
		  Artificial Intelligence (KI'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNAI 1303",
  keywords =	 "misc"
}

@Article{Basin98jlli,
  author = 	 "David Basin and Se{\'a}n Matthews and Luca Vigan{\`o}",
  title = 	 "Labelled Modal Logic: Quantifiers",
  journal =	 "Journal of Logic, Language, and Information",
  year =	 1998,
  volume =	 7,
  number =	 3,
  month =        jul,
  pages =	 "237--263",
  keywords =	 "misc"
}

@InProceedings{Bella98cav,
  author = 	 "Giampaolo Bella and Lawrence C. Paulson",
  title = 	 "Machanising {BAN} {Kerberos} by the Inductive Method",
  editor =	 "A.J. Hu and M.Y. Vardi",
  pages =	 "416--427",
  booktitle =	 "Proceedings of the 10th International Conference on
		  Computer-Aided Verification (CAV'98)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1427",
  address =	 "Vancouver, B.C., Canada",
  month =	 jun,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/users/lcp/papers/Bella/cav98.ps.gz"
}

@InProceedings{Bella98esorics,
  author = 	 "Giampaolo Bella and Lawrence C. Paulson",
  title = 	 "Kerberos Version {IV}: Inductive Analysis of the Secrecy Goals",
  editor =	 "J.-J. Quisquater",
  pages =	 "361--375",
  booktitle =	 "Proceedings of the 5th European Symposium on Research in
		  Computer Security",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1485",
  address =	 "Louvain-la-Neuve, Belgium",
  month =	 sep,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/users/lcp/papers/Bella/esorics98.ps.gz"
}

@InProceedings{Bertot94,
  author = 	 "Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry",
  title = 	 "Proof by Pointing",
  editor =	 "M. Hagiya and J.C. Mitchell",
  pages =	 "141--160",
  booktitle =	 "Proceedings of the International Symposium on Theoretical
		  Aspects of Computer Softward",
  year =	 1994,
  publisher =	 "Springer-Verlag LNCS 789",
  address =	 "Sendai, Japan",
  month =	 apr,
  urlps =	 "ftp://babar.inria.fr/pub/croap/BraTypes/proof-by-pointing.ps.gz",
  keywords =	 "misc"
}

@MastersThesis{Betarte93,
  author = 	 "Gustavo Betarte",
  title = 	 "A Case Study in Machine-Assisted Proofs: The Integers Form
		  an Integral Domain",
  school = 	 "Chalmers University of Technology and University of
		  G{\"o}teborg",
  year = 	 1993,
  address =	 "Sweden",
  month =	 nov,
  type =	 "Licentiate Thesis",
  keywords =	 "ALF"
}
		  
@InProceedings{Blanqui99rta,
  author = 	 "Fr{\'e}d{\'e}ric Blanqui and Jean-Pierre Jouannaud and
		  Mitsuhiro Okada",
  title = 	 "The Calculus of Algebraic Constructions",
  editor =	 "P. Narendran and M. Rusinowitch",
  pages =	 "301--316",
  booktitle =	 "Proceedings of the 10th International Conference on
		  Rewriting Techniques and Applications (RTA-99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1631",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "rewriting, misc",
  urlps =	 "http://www.lri.fr/~blanqui/publis/rta99full.ps.gz"
}
		  
@InProceedings{Borovansky98,
  author = 	 "Peter Borovansk{\'y} and Claude Kirchner and H{\'e}l{\`e}ne
		  Kirchner and Pierre-Etienne Moreau and Christophe
		  Ringeissen",
  title = 	 "An Overview of {ELAN}",
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  volume =	 15,
  series =	 "Electronic Notes in Theoretical Computer Science",
  booktitle =	 "Proceedings of the International Workshop on Rewriting Logic
		  and its Applications",
  year =	 1998,
  publisher =	 "Elsevier Science",
  address =	 "Pont-{\`a}-Mousson, France",
  month =	 sep,
  url =		 "http://www.elsevier.com/locate/entcs/volume15.html"
}

@PhdThesis{Brown96,
  author = 	 "Jason J. Brown",
  title = 	 "Presentations of Unification in a Logical Framework",
  school = 	 "University of Oxford",
  year = 	 1996,
  month =	 jan,
  keywords =	 "LF, unification"
}

@InProceedings{Broy94,
  author = 	"Manfred Broy and Ursula Hinkel and Tobias Nipkow and
		  Christian Prehofer and Birgit Schieder",
  title = 	"Interpreter Verification for a Functional Language",
  booktitle =	"Proceedings of the 14th Conference on Foundations of Software
		  Technology and Theoretical Computer Science",
  publisher =	"Springer-Verlag LNCS 880",
  year = 	1994,
  pages =	"77--88",
  editor =      "P.S. Thiagarajan",
  url     =		"http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs94.html",
  keywords = 	"Isabelle"
}

@InProceedings{Burstall91,
  author =	"Rod Burstall and Furio Honsell",
  title	=	"Operational Semantics in a Natural Deduction Setting",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages	=	"185--214",
  year =	"1991",
  keywords = 	"LF"
}

@InProceedings{Caires94,
  author = 	 "Luis Caires and Luis Monteiro",
  title = 	 "Higher-Order Polymorphic Unification for Logic Programming",
  editor =	 "Pascal Van Hentenryck",
  pages =	 "419--433",
  booktitle =	 "Proceedings of the Eleventh International Conference on
		  Logic Programming",
  year =	 1994,
  publisher =	 "MIT Press",
  address =	 "Genoa, Italy",
  month =	 "June",
  keywords =	 "lambda-Prolog, unification"
}

@Unpublished{Calderon95,
  author = 	 "Guillermo Calder{\'o}n",
  title = 	 "Implementing {Martin-L{\"o}f's} Theory of Types in a
		  Higher-Order Logic Programming Language",
  note = 	 "Submitted",
  year =	 1995,
  month =	 may,
  keywords =	 "misc"
}

@InProceedings{Cant92ml,
  author =	"A. Cant and M. A. Ozols",
  title =	"A Verification Environment for {ML} Programs",
  booktitle =	"Workshop on ML and its Applications",
  address =	"San Francisco, California",
  editor =	"Peter Lee",
  month =	jun,
  year =	1992,
  pages =	"151--156",
  organization =	"ACM SIGPLAN",
  keywords = 	"Isabelle"
}

@TechReport{Cant92tr,
  author =	"A. Cant",
  title =	"Program Verification Using Higher Order Logic",
  institution =	"Electronics Research Laboratory, DSTO",
  year =	1992,
  number =	"ERL-0600-RR",
  keywords = 	"Isabelle"
}

@TechReport{Cant94,
  author = 	 "A. Cant and M. A. Ozols",
  title = 	 "An Approach to Automated Reasoning About Operational
		  Semantics",
  institution =  "Electronics Research Laboratory, DSTO",
  year = 	 1994,
  address =	 "Salisbury, South Astralia",
  keywords =	 "Isabelle"
}

@InProceedings{Cervesato96elp,
  author = 	 "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
  title = 	 "Efficient Resource Management for Linear Logic Proof Search",
  editor =	 "R. Dyckhoff and H. Herre and P. Schroeder-Heister",
  booktitle =	 "Proceedings of the 5th International Workshop on Extensions
		  of Logic Programming",
  year =	 1996,
  pages =        "67--81",
  publisher =	 "Springer-Verlag LNAI 1050",
  address =	 "Leipzig, Germany",
  month =	 mar,
  keywords =	 "linear",
  urldvi =	 "http://www.cs.cmu.edu/~fp/papers/elp96.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/elp96.ps.gz"
}

@InProceedings{Cervesato96lics,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Logical Framework",
  editor =	 "E. Clarke",
  booktitle =	 "Proceedings of the Eleventh Annual Symposium on Logic in
                  Computer Science",
  year =	 1996,
  publisher =	 "IEEE Computer Society Press",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  pages =	 "264--275",
  keywords =	 "LF, Elf, linear",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/lics96.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/lics96.ps.gz"
}

@PhdThesis{Cervesato96phd,
  author = 	 "Iliano Cervesato",
  title = 	 "A Linear Logical Framework",
  school = 	 "Dipartimento di Informatica, Universit{\`a} di Torino",
  month =	 feb,
  year = 	 1996,
  keywords =     "LF, Elf, linear"
}

@InProceedings{Cervesato96pstt,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "Linear Higher-Order Pre-Unification",
  editor =	 "D. Galmiche",
  booktitle =	 "Informal Proceedings of the Workshop on Proof Search in
	          Type-Theoretic Language",
  year =	 1996,
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  urlps =        "http://www.cs.cmu.edu/~fp/papers/pstt96.ps.gz",
  keywords =	 "LF, Elf, linear, unification"
}

@InProceedings{Cervesato97lics,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "Linear Higher-Order Pre-Unification",
  editor =	 "Glynn Winskel",
  booktitle =	 "Proceedings of the Twelfth Annual Sumposium on Logic
                  in Computer Science (LICS'97)",
  pages =        "422-433",
  year =	 1997,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Warsaw, Poland",
  month =	 jun,
  keywords =	 "linear, unification, LF, Elf",
  urldvi =	 "http://www.cs.cmu.edu/~fp/papers/lics97.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/lics97.ps.gz"
}
		  
@Article{Cervesato97tcs,
  author = 	 "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
  title = 	 "Efficient Resource Management for Linear Logic Proof Search",
  journal =	 "Theoretical Computer Science",
  year =	 1997,
  note =	 "To appear in a special issue on Proof Search in
		  Type-Theoretic Languages, D. Galmiche, editor",
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/erm97.ps.gz"
}

@TechReport{Cervesato97tr,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Spine Calculus",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1997,
  number =	 "CMU-CS-97-125",
  month =	 apr,
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/CMU-CS-97-125.ps.gz"
}
		  
@Article{Cervesato98ic,
  author = 	 "Iliano Cervesato and Frank Pfenning",
  title = 	 "A Linear Logical Framework",
  journal =	 "Information and Computation",
  year =	 1998,
  note =	 "To appear in a special issue with
		  invited papers from LICS'96, E. Clarke, editor",
  keywords =     "LF, Elf, linear",		  
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/llf97.ps.gz"
}
		  
@InProceedings{Cervesato98jicslp,
  author = 	 "Iliano Cervesato",
  title = 	 "Proof-Theoretic Foundation of Compilation in Logic
		  Programming Languages",
  editor =	 "J. Jaffar",
  pages =	 "115--129",
  booktitle =	 "Proceedings of the 1998 Joint International Conference
		  and Symposium on Logic Programming (JICSLP'98)",
  year =	 1998,
  publisher =	 "MIT Press",
  address =	 "Manchester, UK",
  month =	 jun,
  keywords =	 "LF, Elf",
  urlps =	 "http://theory.stanford.edu/~iliano/papers/jicslp98.ps.gz"
}

@PhdThesis{Chirimar95phd,
  author = 	 "Jawahar Lal Chirimar",
  title = 	 "Proof Theoretic Approach to Specification Languages",
  school = 	 "University of Pennsylvania",
  year = 	 1995,
  month =	 may,
  urlps =	 "file://ftp.cis.upenn.edu/pub/papers/chirimar/phd.ps.gz",
  keywords =	 "linear"
}

@TechReport{Ciesielski91,
  author =	"Boleslaw Ciesielski and Mitchell Wand",
  title	=	"Using the Theorem Prover {Isabelle-91} to Verify a Simple
		  Proof of Compiler Correctness", 
  institution =	"College of Computer Science, Northeastern University",
  number =	"NU-CCS-91-20",
  month	=	dec,
  year =	"1991",
  keywords =	"Isabelle"
}
		  
@InProceedings{Clavel99rta,
  author = 	 "M. Clavel and F. Dur{\'a}n and S. Eker and P. Lincoln and
		  N. Mart{\'\i}-Oliet and J. Meseguer and J.F. Quesada",
  title = 	 "The {Maude} System",
  editor =	 "P. Narendran and M. Rusinowitch",
  pages =	 "240--243",
  booktitle =	 "Proceedings of the 10th International Conference on
		  Rewriting Techniques and Applications (RTA-99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1631",
  address =	 "Trento, Italy",
  month =	 jul,
  note =	 "System Description",
  keywords =	 "rewriting"
}

@PhdThesis{Coen92,
  author =	"Martin D. Coen",
  title =	"Interactive Program Derivation",
  school =	"University of Cambridge",
  note =	"Available as Computer Laboratory Technical Report 272",
  year =	1992,
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR272-mc-interactive-program-derivation.dvi.gz",
  keywords = 	"Isabelle"
}

@Book{Constable86,
  author =	"Robert L. Constable and others",
  title	=	"Implementing Mathematics with the Nuprl Proof Development
		  System",
  publisher =	"Prentice-Hall",
  address =	"Englewood Cliffs, New Jersey",
  year =	"1986",
  keywords = 	"misc"
}

@InCollection{Constable90,
  author = 	 "Robert Constable and Douglas Howe",
  title = 	 "{NuPrl} as a General Logic",
  booktitle =	 "Logic and Computation",
  publisher =	 "Academic Press",
  year =	 1990,
  editor =	 "P. Odifreddi",
  keywords =	 "misc"
}
		  
@InProceedings{Coquand91,
  author =	"Thierry Coquand",
  title =	"An Algorithm for Testing Conversion in Type Theory",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"255--279",
  year =	"1991",
  keywords = 	"LF, ALF"
}

@InProceedings{Coquand92typesa,
  author =	"Thierry Coquand",
  title =       "Pattern Matching with Dependent Types",
  booktitle =   "Proceedings of the Workshop on Types for Proofs and Programs",
  address =     "B{\aa}stad, Sweden",
  year =        "1992",
  pages =       "71--83",
  keywords = 	"ALF"
}

@InProceedings{Coquand92typesb,
  author =	"Catarina Coquand",
  title =       "A proof of normalization for simply typed lambda calculus
		  written in {ALF}",
  booktitle =	"Proceedings of the Workshop on Types for Proofs and Programs",
  address =	"B{\aa}stad, Sweden",
  year =        "1992",
  pages =       "85--92",
  keywords = 	"ALF"
}

@InProceedings{Coquand93csl,
  author = 	 "Catarina Coquand",
  title = 	 "From Semantics to Rules: A Machine Assisted Analysis",
  editor = 	 "E. B{\"o}rger and Y. Gurevich and K. Meinke",
  pages =	 "91--105",
  booktitle =	 "Proceedings of the 7th Workshop on Computer Science Logic",
  year =	 1993,
  publisher =	 "Springer-Verlag LNCS 832",
  keywords =	 "ALF"
}

@InProceedings{Coquand93types,
  author =	"Thierry Coquand and Jan M. Smith",
  title =	"What is the Status of Pattern Matching in Type Theory?",
  booktitle =	"Proceedings of the Workshop on Types for Proofs and Programs",
  address =	"Nijmegen, The Netherlands",
  year =	"1993",
  pages =	"91--94",
  keywords = 	"ALF"
}

@Article{Coquand94,
  author = 	"Thierry Coquand and Bengt {Nordstr\"om} and Jan M.
		  Smith and {Bj\"orn} von Sydow",
  title = 	"Type Theory and Programming",
  journal =	"Bulletin of the European Association for Theoretical Computer
		  Science",
  month =       feb,
  volume =	"52",
  pages =	"203--228",
  year =	"1994",
  keywords =	"ALF"
}

@InProceedings{Cornes95,
  author = 	 "C. Cornes and D. Terrasse",
  title = 	 "Automating Inversion and Inductive Predicates in {Coq}",
  pages =	 "85--104",
  booktitle =	 "Proceedings of the Workshop on Types for Proofs and Programs",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 1158",
  address =	 "Torino, Italy",
  month =	 jun,
  keywords =     "misc",
  urlps =        "file://babar.inria.fr/pub/croap/terrasse/types95.ps"
}

@InProceedings{Courant97,
  author = 	 "Judicael Courant",
  title = 	 "A Module Calculus for Pure Type Systems",
  editor =	 "R. Hindley",
  booktitle =	 "Proceedings fo the Third International Conference on
                  Typed Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "misc"
}

@TechReport{Courant99,
  author = 	 "Judica{\"e}l Courant",
  title = 	 "{MC:} A Modular Calculus for {Pure Type Systems}",
  institution =  "CNRS Universit{\'e} Paris Sud",
  year = 	 1999,
  type =	 "Rapport de Recherche",
  number =	 1217,
  month =	 jun
}

@InProceedings{Curien96,
  author = 	 "R{\'e}gis Curien and Zhenyu Qian and Hui Shi",
  title = 	 "Efficient Second-Order Matching",
  editor =	 "Harald Ganzinger",
  pages =	 "317--331",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "unification"
}

@TechReport{DaRosa94,
  author = 	 "Silvia da Rosa and Alberto Pardo",
  title = 	 "Representing Program Transformation in {Martin-L{\"o}f's}
		  Type Theory",
  institution =  "Instituto de Computaci{\'o}n, Facultad de Ingenieria,
		  Universidad de la Republica Oriental del Uruguay",
  year = 	 1994,
  address =	 "Montevideo, Uruguay",
  keywords =     "misc"
}

@TechReport{Danvy95,
  author = 	 "Olivier Danvy and Frank Pfenning",
  title = 	 "The Occurrence of Continuation Parameters in {CPS} Terms",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1995,
  number =	 "CMU-CS-95-121",
  month =	 feb,
  keywords =     "LF, Elf",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/cpsocc95.ps.gz"
}

@InProceedings{Dawson98jelia,
  author = 	 "Jeremy E. Dawson and Rajeev Gor{\'e}",
  title = 	 "A Mechanised Proof System for Relation Algebra using Display
		  Logic",
  editor =	 "J. Dix and L. Fari{\~n}as del Cerro and U. Furbach",
  pages =	 "264--278",
  booktitle =	 "Proceedings of the European Workshop on Logics in Artificial
		  Intelligence (JELIA'98)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNAI 1478",
  address =	 "Dagstuhl, Germany",
  month =	 oct,
  keywords =	 "Isabelle",
  urlps =	 "ftp://arp.anu.edu.au/pub/papers/gore/dRA.ps.gz"
}

@InProceedings{Dawson98ai,
  author = 	 "Jeremy E. Dawson and Rajeev Gor{\'e}",
  title = 	 "A Mechanisation of Classical Tense Display Logic",
  editor =	 "G. Antoniou and J. Slaney",
  pages =	 "107--118",
  booktitle =	 "Proceedings of the 11th Australian Joint Conference on
		  Artificial Intelligence (AI'98)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNAI 1502",
  address =	 "Brisbane, Australia",
  month =	 jul,
  keywords =	 "Isabelle",
  urlps =	 "ftp://arp.anu.edu.au/pub/papers/gore/dkt.ps.gz"
}

@InProceedings{DeBruijn68,
  author = 	"N.G. de Bruijn",
  title = 	"The Mathematical Language {AUTOMATH}, Its Usage, and Some of
		  Its Extensions",
  editor =	"M. Laudet",
  pages =	"29--61",
  booktitle =	"Proceedings of the Symposium on Automatic Demonstration",
  year =	1968,
  publisher =	"Springer-Verlag LNM 125",
  address =	"Versailles, France",
  month =	dec,
  keywords = 	"Automath"
}

@Article{DeBruijn72,
  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 =	"Indag. Math.",
  volume =	"34",
  number =	"5",
  year =	"1972",
  pages	=	"381--392",
  keywords = 	"Automath"
}

@TechReport{DeBruijn78,
  author = 	"N.G. de Bruijn",
  title = 	"{AUT-QE} without Type Inclusion",
  institution = "Department of Mathematics, Eindhoven University of
		  Technology",
  year = 	1978,
  type =	"Memorandum",
  number =	"1978-04",
  month =	aug,
  keywords = 	"Automath"
}

@InCollection{DeBruijn80,
  author = 	"N.G. de Bruijn",
  title = 	"A Survey of the Project {AUTOMATH}",
  booktitle =	"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus
		  and Formalism",
  publisher =	"Academic Press",
  year =	1980,
  editor =	"J.P. Seldin and J.R. Hindley",
  pages =	"579--606",
  keywords = 	"Automath"
}

@InCollection{DeBruijn84,
  author = 	"N.G. de Bruijn",
  title = 	"Formalization of Constructivity in {AUTOMATH}",
  booktitle =	"Papers Dedicated to J.J. Seidel, P.J. de Doelder, J. de
		  Graaf and J.H van Lint",
  publisher =	"Department of Mathematics and Computing Science, Eindhoven
		  University of Technology",
  year =	 1984,
  note =	"EUT Report 84-WSK-03",
  pages =	"76--101",
  keywords = 	"Automath"
}

@InCollection{DeBruijn87,
  author = 	"N.G. de Bruijn",
  title = 	"Generalizing {AUTOMATH} by Means of a Lambda-Typed Lambda
		  Calculus",
  booktitle =	"Mathematical Logic and Theoretical Computer Science",
  publisher =	"Marcel Dekker",
  year =	1987,
  editor =	"D.W. Kueker and E.G.K. Lopez-Escobar and C.H. Smith",
  volume =	106,
  series =	"Lecture Notes in Pure and Applied Mathematics",
  pages =	"71--92",
  address =	"New York",
  keywords = 	"Automath"
}

@InProceedings{DeBruijn88,
  author = 	"N.G. de Bruijn",
  title = 	"The Use of Justification Systems for Integrated Semantics",
  editor = 	"P. Martin-L{\"o}f and G. Mints",
  pages =	"9--24",
  booktitle =	"Proceedings of the International Conference on Computer
		  Logic {COLOG'88}",
  address =     "Tallinn, Estonia",
  year =	1988,
  publisher =	"Springer-Verlag LNCS 417",
  month =	dec,
  keywords = 	"Automath"
}

@Article{DeBruijn91ic,
  author = 	"N.G. de Bruijn",
  title = 	"Telescopic Mappings in Typed Lambda Calculus",
  journal =	"Information and Computation",
  year =	1991,
  volume =	91,
  number =	2,
  pages =	"189--204",
  month =	apr,
  keywords = 	"Automath"
}

@InProceedings{DeBruijn91lf,
  author = 	"N.G. de Bruijn",
  title = 	"A Plea for Weaker Frameworks",
  editor =	"G. Huet and G. Plotkin",
  pages =	"40--67",
  booktitle =	"Logical Frameworks",
  year =	1991,
  publisher =	"Cambridge University Press",
  keywords = 	"Automath"
}

@InCollection{DeBruijn93,
  author = 	"N.G. de Bruijn",
  title = 	"Algorithmic Definition of Lambda-Typed Lambda Calculus",
  booktitle =	"Logical Environment",
  publisher =	"Cambridge University Press",
  year =	1993,
  editor =	"G. Huet and G. Plotkin",
  pages =	"131--145",
  keywords = 	"Automath"
}

@InProceedings{Despeyroux94,
  author =	"Jo{\"e}lle Despeyroux and Andr\'e Hirschowitz",
  title =	"Higher-Order Abstract Syntax with Induction in {Coq}",
  editor =	"Frank Pfenning",
  pages =	"159--173",
  booktitle =	"Proceedings of the {5th} International Conference on Logic
		  Programming and Automated Reasoning",
  year =	1994,
  publisher =	"Springer-Verlag LNAI 822",
  address =	"Kiev, Ukraine",
  month =	jul,
  urlps =	"ftp://babar.inria.fr/pub/croap/jdespeyroux/lpar94.ps.gz",
  keywords = 	"misc"
}

@InProceedings{Despeyroux95,
  author = 	 "Jo{\"e}lle Despeyroux and Amy Felty and Andr\'e Hirschowitz",
  title = 	 "Higher-Order Abstract Syntax in {Coq}",
  editor =	 "M. Dezani-Ciancaglini and G. Plotkin",
  booktitle =	 "Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 902",
  address =	 "Edinburgh, Scotland",
  month =	 apr,
  pages =	 "124--138",
  urlps =	 "ftp://babar.inria.fr/pub/croap/jdespeyroux/tlca95.ps.gz",
  keywords =     "misc"
}

@TechReport{Despeyroux96,
  author = 	 "Jo{\"e}lle Despeyroux and Frank Pfenning and Carsten
                  Sch{\"u}rmann",
  title = 	 "Primitive Recursion for Higher-Order Abstract Syntax",
  institution =  "Carnegie Mellon University",
  year = 	 1996,
  type =	 "Technical Report",
  number = 	 "CMU-CS-96-172",
  month =	 sep,
  keywords =     "misc",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/CMU-CS-96-172.dvi.gz",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/CMU-CS-96-172.ps.gz",
}

@InProceedings{Despeyroux97,
  author = 	 "Jo{\"e}lle Despeyroux and Frank Pfenning and Carsten
                  Sch{\"u}rmann",
  title = 	 "Primitive Recursion for Higher-Order Abstract Syntax",
  editor =	 "R. Hindley",
  pages =	 "147--163",
  booktitle =	 "Proceedings of the Third International Conference on
                  Typed Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "misc",
  note =	 "An extended version is available as Technical Report
                  CMU-CS-96-172, Carnegie Mellon University",
  urldvi =	 "http://www.cs.cmu.edu/~fp/papers/tlca97.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/tlca97.ps.gz"
}

@InProceedings{Devillers97,
  author = 	 "Marco Devillers and David Griffioen and Olaf M{\"u}ller",
  title = 	 "Possibly Infinite Sequences in Theorem Provers: A
		  Comparative Study",
  editor =	 "E.L. Gunter and A. Felty",
  pages =	 "89--104",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
		  Proving in Higher Order Logics (TPHOLs'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1275",
  address =	 "Murray Hill, New Jersey",
  month =	 aug,
  keywords =	 "Isabelle",
  urlhtml =	 "http://wwwbroy.informatik.tu-muenchen.de/~mueller/publications.html"
}

@InProceedings{Dietzen91ilps,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"A Declarative Alternative to {assert} in Logic Programming",
  booktitle =	"International Logic Programming Symposium",
  publisher =	"MIT Press",
  editor =	"Vijay Saraswat and Kazunori Ueda",
  pages =	"372--386",
  month =	oct,
  year =	"1991",
  keywords = 	"lambda-Prolog"
}

@PhdThesis{Dietzen91phd,
  author =	"Scott Dietzen",
  title =	"A Language for Higher-Order Explanation-Based Learning",
  school =	"School of Computer Science, Carnegie Mellon University",
  year =	"1991",
  note =	"Available as Technical Report CMU-CS-92-110",
  keywords = 	"lambda-Prolog"
}

@Article{Dietzen92,
  author =	"Scott Dietzen and Frank Pfenning",
  title =	"Higher-Order and Modal Logic as a Framework for
		  Explanation-Based Generalization",
  journal =	"Machine Learning",
  year =	"1992",
  volume =	"9",
  pages =	"23--55",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Dowek93tlca,
  author =	"Gilles Dowek",
  title =	"The Undecidability of Typability in the
                  Lambda-Pi-Calculus",
  booktitle =	"Proceedings of the International Conference on
                  Typed Lambda Calculi and Applications",
  editor =	"M. Bezem and J.F. Groote",
  publisher =	"Springer-Verlag LNCS 664",
  address =	"Utrecht, The Netherlands",
  month =	mar,
  year =	"1993",
  pages =	"139--145",
  keywords = 	"LF"
}

@TechReport{Dowek93tr,
  author =	"Gilles Dowek and Amy Felty and Hugo Herbelin and
		  G{\'e}rard Huet and Chet Murthy and Catherine Parent and
		  Christine Paulin-Mohring and Benjamin Werner",
  title =	"The {Coq} Proof Assistant User's Guide",
  institution =	"INRIA",
  address =	"Rocquencourt, France",
  type =	"Rapport Techniques",
  number =	"154",
  year =	"1993",
  note =	"Version 5.8",
  keywords = 	"misc"
}

@InProceedings{Dowek93types,
  author = 	 "Gilles Dowek and G{\'e}rard Huet and Benjamin Werner",
  title = 	 "On the Definition of the Eta-Long Normal Form in Type
		  Systems of the Cube",
  editor =	 "Herman Geuvers",
  booktitle =	 "Informal Proceedings of the Workshop on Types for Proofs and
		  Programs",
  year =	 1993,
  address =	 "Nijmegen, The Netherlands",
  month =	 may,
  urlps =	 "http://pauillac.inria.fr/~dowek/eta.ps.gz"
}

@InProceedings{Dowek95,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude
		  Kirchner",
  title = 	 "Higher-Order Unification via Explicit Substitutions",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 "June",
  pages =	 "366--374",
  keywords =     "unification"
}

@InProceedings{Dowek96jicslp,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner
                  and Frank Pfenning",
  title = 	 "Unification via Explicit Substitutions: The Case of
                  Higher-Order Patterns",
  booktitle = 	 "Proceedings of the Joint International Conference and
                  Symposium on Logic Programming",
  editor = 	 "M. Maher",
  year = 	 "1996",
  publisher =    "MIT Press",
  address = 	 "Bonn, Germany",
  month = 	 sep,
  pages =        "259--273",
  notes =        "Extended version available as Rapport de Recherche No.~3591,
		  INRIA, December 1998",
  keywords =     "unification",
  urldvi = 	 "http://www.cs.cmu.edu/~fp/papers/jicslp96.dvi.gz",
  urlps = 	 "http://www.cs.cmu.edu/~fp/papers/jicslp96.ps.gz"
}
		  
@InProceedings{Dowek99rta,
  author = 	 "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude Kirchner",
  title = 	 "{HOL}-$\lambda\sigma$: An Intentional First-Order Expression
		  of Higher-Order Logic",
  editor =	 "P. Narendran and M. Rusinowitch",
  pages =	 "317--331",
  booktitle =	 "Proceedings of the 10th International Conference on
		  Rewriting Techniques and Applications (RTA-99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1631",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "unification, misc"
}

@TechReport{Duggan93tra,
  author =       "Dominic Duggan",
  title =        "Unification with Extended Patterns",
  institution =  "University of Waterloo",
  year =         1993,
  number =       "CS-93-37",
  address =      "Waterloo, Ontario, Canada",
  month =        jul,
  note =         "Revised March 1994 and September 1994",
  url     =	"http://nuada.uwaterloo.ca/dduggan/papers.html#hou-paper",
  keywords =	"unification"
}

@TechReport{Duggan93trb,
  author =       "Dominic Duggan",
  title =        "Higher-Order Substitutions",
  institution =  "University of Waterloo",
  year =         1993,
  number =       "CS-93-44",
  address =      "Waterloo, Ontario, Canada",
  month =        oct,
  note =         "Revised September 1994",
  url     =		"http://nuada.uwaterloo.ca/dduggan/papers.html#hosubst-paper",
  keywords =	"misc"
}

@InProceedings{Duggan94,
  author =       "Dominic Duggan",
  title =        "Logical Closures",
  editor =       "Frank Pfenning",
  pages =        "114--129",
  booktitle =    "Proceedings of the 5th International Conference on Logic
		  Programming and Automated Reasoning", 
  address =	 "Kiev, Ukraine",
  publisher =    "Springer-Verlag LNAI 822",
  month =        jul,
  year =         1994,
  keywords =	 "misc"
}

@Article{Dybjer89,
  author =	"Peter Dybjer and Herbert Sander",
  title =       "A Functional Programming Approach to the Specification and
		  Verification of Concurrent Systems", 
  journal =	"Formal Aspects of Computing",
  volume =	1,
  pages =	"303-319",
  year =	1989,
  keywords =	"Isabelle"
}

@InProceedings{Dyckhoff94,
  author = 	 "Roy Dyckhoff and Lu{\'\i}s Pinto",
  title = 	 "Uniform Proofs and Natural Deduction",
  editor =	 "D. Galmiche and L. Wallen",
  pages =	 "17--23",
  booktitle =	 "Proceedings of the Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1994,
  address =	 "Nancy, France",
  month =	 jul,
  keywords =	 "misc",
  urlps =	 "http://www-theory.dcs.st-and.ac.uk/~rd/publications/upnd.ps"
}

@InProceedings{Dyckhoff98,
  author = 	 "Lu{\'\i}s Pinto and Roy Dyckhoff",
  title = 	 "Sequent Calculi for the Normal Terms of the $\lambda\Pi$-
		  and $\lambda\Pi\Sigma$-Calculi",
  editor =	 "D. Galmiche",
  volume =	 17,
  series =	 "Electronic Notes in Theoretical Computer Science",
  booktitle =	 "Proceedings of the Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1998,
  publisher =	 "Elsevier Science",
  address =	 "Lindau, Germany",
  month =	 jul,
  keywords =     "LF, Elf",
  url =		 "http://www.elsevier.com/locate/entcs/volume17.html"
}

@InProceedings{Elliott89,
  author =	"Conal Elliott",
  title =	"Higher-Order Unification with Dependent Types",
  booktitle =	"Rewriting Techniques and Applications",
  address =	"Chapel Hill, North Carolina",
  publisher =	"Springer-Verlag LNCS 355",
  editor =	"N. Dershowitz",
  month =	apr,
  year =	"1989",
  pages =	"121--136",
  urlps =	"http://www.cs.cmu.edu/~fp/elf-papers/rta89.ps.gz",
  keywords = 	"LF, unification"
}

@PhdThesis{Elliott90,
  author =	"Conal M. Elliott",
  title =	"Extensions and Applications of Higher-Order Unification",
  school =	"School of Computer Science, Carnegie Mellon University",
  month =	may,
  year =	"1990",
  note =	"Available as Technical Report CMU-CS-90-134",
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/elliott90.dvi.gz",
  urlps =       "http://www.cs.cmu.edu/~fp/elf-papers/elliott90.ps.gz",
  keywords = 	"LF, unification"
}

@InCollection{Elliott91,
  author =	"Conal Elliott and Frank Pfenning",
  title =	"A Semi-Functional Implementation of a Higher-Order Logic
		  Programming Language",
  booktitle =	"Topics in Advanced Language Implementation",
  publisher =	"MIT Press",
  year =	"1991",
  pages =	"289--325",
  editor =	"Peter Lee",
  url =  	"http://www.cs.cmu.edu/~fp/papers/elpsml-paper.tar.gz",
  keywords = 	"lambda-Prolog, LF, Elf"
}

@TechReport{Eriksson88,
  author =	"Lars-Henrik Eriksson and Lars Halln{\"a}s",
  title =	"A Programming Calculus Based on Partial Inductive
		  Definitions",
  institution =	"Swedish Institute of Computer Science",
  year =	1988,
  type =	"SICS Research Report",
  number =	"R88013",
  keywords = 	"Pi"
}

@InProceedings{Eriksson92,
  author =	"Lars-Henrik Eriksson",
  title =	"A Finitary Version of the Calculus of Partial Inductive
		  Definitions",
  editor =	"L.-H. Eriksson and L. Halln{\"a}s and P. Schroeder-Heister",
  pages =	"89--134",
  booktitle =	"Proceedings of the Second International Workshop on
		  Extensions of Logic Programming",
  year =	1992,
  publisher =	"Springer-Verlag LNAI 596",
  address =	"Stockholm, Sweden",
  month =	jan,
  keywords = 	"Pi"
}

@InProceedings{Eriksson93elp,
  author =	"Lars-Henrik Eriksson",
  title =	"Finitary Partial Inductive Definitions as a General Logic",
  editor =	"R. Dyckhoff",
  booktitle =	"Proceedings of the 4th International Workshop on Extensions
		  of Logic Programming",
  year =	1993,
  publisher =	"Springer-Verlag LNAI 798",
  keywords = 	"Pi"
}

@PhdThesis{Eriksson93phd,
  author =	"Lars-Henrik Eriksson",
  title =	"Finitary Partial Inductive Definitions and General Logic",
  school =	"Department of Computer and System Sciences, Royal Institute
		  of Technology",
  year =	1993,
  address =	"Stockholm",
  keywords = 	"Pi"
}

@InProceedings{Eriksson94,
  author =	"Lars-Henrik Eriksson",
  title =	"Pi: An Interactive Derivation Editor for the
		  Calculus of Partial Inductive Definitions",
  editor =	"A. Bundy",
  booktitle =	"Proceedings of the 12th International Conference on
		  Automated Deduction",
  year =	1994,
  publisher =	"Springer Verlag LNAI 814",
  address =	"Nancy, France",
  month =	jun,
  pages =	"821--825",
  keywords = 	"Pi"
}

@InProceedings{Feferman88,
  author =	"Solomon Feferman",
  title =	"Finitary Inductive Systems",
  booktitle =	"Proceedings of Logic Colloquium {'88}",
  editor =	"R. Ferro",
  pages =	"191--220",
  publisher =	"North-Holland",
  address =	"Padova, Italy",
  month =	aug,
  year =	1988,
  keywords = 	"FS0"
}

@InProceedings{Felty88cade,
  author =	"Amy Felty and Dale Miller",
  title =	"Specifying Theorem Provers in a Higher-Order Logic
		  Programming Language",
  editor =	"Ewing Lusk and Ross Overbeek",
  booktitle =	"Proceedings of the Ninth International Conference on Automated
		  Deduction",
  address =	"Argonne, Illinois",
  publisher =	"Springer-Verlag LNCS 310",
  pages =	"61--80",
  month =	may,
  year =	1988,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Felty89elp,
  author =	"Amy Felty",
  editor =	"Peter Schroeder-Heister",
  title =	"A Logic Program for Transforming Sequent Proofs to
		  Natural Deduction Proofs",
  booktitle =	"Proceedings of the International Workshop on Extensions of
		  Logic Programming",
  address =	"T{\"u}bingen, Germany",
  month =	dec,
  publisher =	"Springer-Verlag LNAI 475",
  pages =	"157--178",
  year =	"1989",
  urlps =	"ftp://ftp.research.bell-labs.com/dist/felty/welp91.ps.gz",
  keywords = 	"lambda-Prolog"
}

@PhdThesis{Felty89phd,
  author =	"Amy Felty",
  title =	"Specifying and Implementing Theorem Provers in a
		  Higher-Order Logic Programming Language",
  school =	"University of Pennsylvania",
  month =	aug,
  year =	1989,
  note =	"Available as Technical Report MS-CIS-89-53",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Felty90,
  author =	"Amy Felty and Dale Miller",
  title =	"Encoding a Dependent-Type {$\lambda$}-Calculus in a Logic
		  Programming Language",
  booktitle =	"10th International Conference on Automated Deduction",
  address =	"Kaiserslautern, Germany",
  editor =	"M.E. Stickel",
  publisher =	"Springer-Verlag LNCS 449",
  month =	jul,
  year =	"1990",
  pages =	"221--235",
  urlps =	"ftp://ftp.research.bell-labs.com/dist/felty/cade10.ps.gz",
  keywords = 	"lambda-Prolog, LF"
}

@InProceedings{Felty91elp,
  author =	"Amy Felty",
  title =	"A Logic Programming Approach to Implementing Higher-Order
		  Term Rewriting",
  booktitle =	"Proceedings of the Second International Workshop on
		  Extensions of Logic Programming",
  address =	"Stockholm, Sweden",
  editor =	"Lars-Henrik Eriksson and Lars Halln{\"{a}}s and Peter
		  Schroeder-Heister",
  pages =	"135--161",
  publisher =	"Springer-Verlag LNAI 596",
  month =	jan,
  year =	1991,
  urlps =	"ftp://ftp.research.bell-labs.com/dist/felty/welp92.ps.gz",
  keywords = 	"lambda-Prolog, rewriting"
}

@InProceedings{Felty91lf,
  author =	"Amy Felty",
  title =	"Encoding Dependent Types in an Intuitionistic Logic",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon D. Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"214--251",
  year =	1991,
  urlps =       "ftp://ftp.research.bell-labs.com/dist/felty/lf91.ps.gz",
  keywords = 	"lambda-Prolog, LF"
}

@Article{Felty93jar,
  author =	"Amy Felty",
  title =	"Implementing Tactics and Tacticals in a Higher-Order Logic
		  Programming Language",
  journal =	"Journal of Automated Reasoning",
  volume =	"11",
  number =	"1",
  year =	1993,
  month =	aug,
  pages =	"43--81",
  urlps =       "ftp://ftp.research.bell-labs.com/dist/felty/jar.ps.gz",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Felty93lics,
  title =	"Encoding the Calculus of Constructions in a Higher-Order
		  Logic",
  author =	"Amy Felty",
  pages =	"233-244",
  booktitle =	"Eighth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Montreal, Canada",
  editor =	"M. Vardi",
  month =	jun,
  year =	"1993",
  urlps =       "ftp://ftp.research.bell-labs.com/dist/felty/lics93.ps.gz",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Felty94cade,
  author =	"Amy Felty and Douglas Howe",
  title =	"Tactic Theorem Proving with Refinement-Tree Proofs and
		  Metavariables",
  booktitle =	"Proceedings of the 12th International Conference
		  on Automated Deduction",
  address =	"Nancy, France",
  editor =	"Alan Bundy",
  pages =	"605--619",
  publisher =	"Springer-Verlag LNAI 596",
  month =	jun,
  year =	1994,
  urlps =       "ftp://ftp.research.bell-labs.com/dist/felty/cade12.ps.gz",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Felty94lpar,
  author = 	 "Amy Felty and Douglas Howe",
  title = 	 "Generalization and Reuse of Tactic Proofs",
  editor =	 "Frank Pfenning",
  pages =	 "1--15",
  booktitle =	 "Proceedings of the 5th International Conference on Logic
		  Programming and Automated Reasoning",
  year =	 1994,
  publisher =	 "Springer-Verlag LNAI 822",
  address =	 "Kiev, Ukraine",
  month =	 jul,
  keywords =	 "lambda-Prolog"
}

@InProceedings{Fettig96,
  author = 	 "Roland Fettig and Bernd L{\"o}chner",
  title = 	 "Unification of Higher-Order Patterns in a Simply Typed
		  Lambda-Calculus with Finite Products and Terminal Type",
  editor =	 "Harald Ganzinger",
  pages =	 "347--361",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "unification"
}

@InProceedings{Fiore99lics,
  author = 	 "Marcelo Fiore and Gordon Plotkin and Daniele Turi",
  title = 	 "Abstract Syntax and Variable Binding",
  editor =	 "G. Longo",
  pages =	 "193--202",
  booktitle =	 "Proceedings of the 14th Annual Symposium on Logic in
		  Computer Science (LICS'99)",
  year =	 1999,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "misc"
}
		  
@InProceedings{Fleuriot98,
  author = 	 "Jacques D. Fleuriot and Lawrence C. Paulson",
  title = 	 "A Combination of Nonstandard Analysis and Geometry Theorem
		  Proving, with Application to {Newton's} {Principia}",
  editor =	 "C. Kirchner and H. Kirchner",
  pages =	 "3--16",
  booktitle =	 "Proceedings of the 15th International Conference on
		  Automated Deduction (CADE-15)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNAI 1421",
  address =	 "Lindau, Germany",
  month =	 jul,
  keywords =	 "Isabelle"
}

@MastersThesis{Fridlender93,
  author = 	 "Daniel Fridlender",
  title = 	 "Ramsey's Theorem in Type Theory",
  school = 	 "Chalmers University of Technology and University of
		  G{\"o}teborg",
  year = 	 1993,
  address =	 "Sweden",
  month =	 oct,
  type =	 "Licentiate Thesis",
  keywords =	 "ALF"
}

@TechReport{Frost95,
  author = 	 "Jacob Frost",
  title = 	 "A Case Study of Co-induction in {Isabelle}",
  institution =  "University of Cambridge, Computer Laboratory",
  year = 	 1995,
  number =	 359,
  month =	 feb,
  note =	 "Revised version of CUCL 308, August 1993",
  keywords =	 "Isabelle"
}

@InProceedings{Frost96,
  author = 	 "J. Frost and I. A. Mason",
  title = 	 "An Operational Logic of Effects",
  editor =	 "M.E. Houle and P. Eades",
  pages =	 "147--156",
  booktitle =	 "Proceedings of Computing: Australasian Theorem Symposium
		  (CATS'96)",
  year =	 1996,
  address =	 "Melbourne, Australia",
  month =	 jan,
  urlps =        "http://maths.une.edu.au/~iam/Data/Papers/96cats.ps",
  keywords =     "Isabelle"
}

@InCollection{Gabbay94handbook,
  author = 	 "Dov M. Gabbay",
  title = 	 "Classical vs Non-Classical Logic",
  booktitle =	 "Handbook of Logic in Artificial Intelligence and Logic Programming",
  publisher =	 "Oxford University Press",
  year =	 1994,
  editor =	 "D.M. Gabbay and C.J. Hogger and J.A. Robinson",
  volume =	 2,
  chapter =	 "2.6",
  keywords =	 "misc"
}

@TechReport{Gabbay94tr,
  author = 	 "Dov M Gabbay",
  title = 	 "Labelled Deductive Systems, Volume 1 --- Foundations",
  institution =  "Max-Planck-Institut f{\"u}r Informatik",
  year = 	 1994,
  number =	 "MPI-I-94-223",
  pages =	 465,
  address =	 "Saarbr{\"u}cken, Germany",
  urlhtml =      "http://www.mpi-sb.mpg.de/papers/reports/abstracts.html#MPI-I-94-223",
  keywords =     "misc"
}
		  
@Book{Gabbay95,
  title = 	 "What is a Logical System?",
  publisher = 	 "Oxford University Press",
  year = 	 1995,
  editor =	 "D. M. Gabbay",
  keywords =	 "misc"
}

@Book{Gabbay96,
  author = 	 "Dov M. Gabbay",
  title = 	 "Labelled Deductive Systems",
  publisher = 	 "Oxford University Press",
  year = 	 1996,
  volume =	 1,
  keywords =	 "misc"
}

@InProceedings{Gabbay99lics,
  author = 	 "Murdoch Gabbay and Andrew Pitts",
  title = 	 "A New Approach to Abstract Syntax Involving Binders",
  editor =	 "G. Longo",
  pages =	 "214--224",
  booktitle =	 "Proceedings of the 14th Annual Symposium on Logic in
		  Computer Science (LICS'99)",
  year =	 1999,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "misc"
}

@PhdThesis{Gardner92,
  author =	"Philippa Gardner",
  title =	"Representing Logics in Type Theory",
  school =	"University of Edinburgh",
  month =	jul,
  year =	"1992",
  note =	"Available as Technical Report CST-93-92",
  keywords = 	"LF"
}

@InProceedings{Gardner93,
  author =	"Philippa Gardner",
  title =	"A New Type Theory for Representing Logics",
  editor =	"Andrei Voronkov",
  pages =	"146--157",
  booktitle =	"Proceedings of the 4th International Conference on Logic
		  Programming and Automated Reasoning (LPAR'93)",
  year =	1993,
  publisher =	"Springer-Verlag LNAI 698",
  address =	"St.~Petersburg, Russia",
  month =	jul,
  keywords = 	"LF"
}

@InProceedings{Gaspes92,
  author =	"Veronica Gaspes and Jan M. Smith",
  title =	"Machine Checked Normalization Proofs for Typed Combinator
		  Calculi",
  booktitle =	"Proceedings of the Workshop on Types for Proofs and Programs",
  address =	"B{\aa}stad, Sweden",
  year =	"1992",
  pages =	"177--192",
  keywords = 	"ALF"
}

@TechReport{Gehrke94tra,
  author = 	"Wolfgang Gehrke",
  title = 	"Proof of the Decidability of the Uniform Word
		  Problem for Monads Assisted by {Elf}",   
  institution =	"RISC",
  year = 	 1994,
  number =	"94-66",
  address =	"Linz, Austria",
  month =	aug,
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/monad94.dvi.gz",
  keywords =	"LF, Elf, rewriting"
}

@TechReport{Gehrke94trb,
  author = 	"Wolfgang Gehrke",
  title = 	"Problems in Rewriting Applied to Categorical Concepts by the
		  Example of a Computational Comonad",
  institution = "Carnegie Mellon University",
  year = 	1994,
  number =	"CMU-CS-94-207",
  address =	"Pittsburgh, Pennsylvania",
  month =	oct,
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/comonad94.dvi.gz",
  keywords =	"LF, Elf, rewriting"
}

@PhdThesis{Gehrke95phd,
  author = 	 "Wolfgang Gehrke",
  title = 	 "Decidability Results for Categorical Notions Related to
		  Monads by Rewriting Techniques",
  school = 	 "Research Institute for Symbolic Computation",
  address =	 "Linz, Austria",
  year = 	 1995,
  month =	 may,
  note =	 "Available as RISC Report Number 95-30",
  urlps =	 "http://www.cs.cmu.edu/~fp/elf-papers/gehrke95.ps.gz",
  keywords =	 "LF, Elf, rewriting"
}

@InProceedings{Gehrke95rta,
  author = 	 "Wolfgang Gehrke",
  title = 	 "Problems in Rewriting Applied to Categorical Concepts by the
		  Example of a Computational Comonad",
  editor =	 "Jieh Hsiang",
  booktitle =	 "Proceedings of the Sixth International Conference on
		  Rewriting Techniques and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 914",
  address =	 "Kaiserslautern, Germany",
  month =	 apr,
  pages =	 "210--224",
  urlps =        "http://www.cs.cmu.edu/~fp/elf-papers/rta95.ps.gz",
  keywords =	 "rewriting, LF, Elf"
}

@InProceedings{Geuvers92,
  author =	"Herman Geuvers",
  title =	"The {Church-Rosser} Property for {$\beta\eta$}-Reduction in
		  Typed $\lambda$-Calculi",
  booktitle =	"Seventh Annual {IEEE} Symposium on Logic in Computer Science",
  editor =	"A. Scedrov",
  address =	"Santa Cruz, California",
  month =	jun,
  year =	"1992",
  pages =	"453--460",
  keywords = 	"LF"
}
		  
@InProceedings{Ghani97,
  author = 	 "Neil Ghani",
  title = 	 "Eta-Expansions in Dependent Type Theory --- The Calculus of
		  Constructions",
  editor =	 "P. de Groote and J.R. Hindley",
  pages =	 "164--180",
  booktitle =	 "Proceedings of the Third International Conference on Typed
		  Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1210",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "rewriting"
}

@Article{Girard93,
  author =	"Jean-Yves Girard",
  title =	"On the Unity of Logic",
  journal =	"Annals of Pure and Applied Logic",
  volume =	"59",
  year =	"1993",
  pages =	"201--217",
  publisher =	"North-Holland",
  keywords = 	"linear"
}

@InProceedings{Goguen99,
  author = 	 "Healfdene Goguen",
  title = 	 "Soundness of the Logical Framework for Its Typed Operational
		  Semantics",
  editor =	 "Jean-Yves Girard",
  pages =	 "177--197",
  booktitle =	 "Proceedings of the 4th International Conference on Typed
		  Lambda Calculi and Applications (TLCA'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1581",
  address =	 "L'Aquila, Italy",
  month =	 apr,
  keywords =	 "LF"
}

@Article{Goldfarb81,
  author =	"Warren D. Goldfarb",
  title =	"The Undecidability of the Second-Order Unification Problem",
  journal =	"Theoretical Computer Science",
  volume =	"13",
  year =	"1981",
  pages =	"225--230",
  keywords = 	"unification"
}

@Book{Gordon93,
  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
}

@InProceedings{Gordon96,
  author = 	 "Andrew D. Gordan and Tom Melham",
  title = 	 "Five Axioms of Alpha-Conversion",
  editor =	 "J. von Wright and J. Grundy and J. Harrison",
  pages =	 "173--191",
  booktitle =	 "Proceedings of the 9th International Conference on Theorem
		  Proving in Higher Order Logics (TPHOLs'96)",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1125",
  address =	 "Turku, Finland",
  month =	 aug,
  keywords =	 "misc"
}

@InProceedings{Gunter89,
  author =	"Elsa L. Gunter",
  editor =	"Peter Schroeder-Heister",
  title =	"Extensions to Logic Programming Motivated by the Construction
		  of a Generic Theorem Prover",
  booktitle =	"Proceedings of the International Workshop on Extensions of
		  Logic Programming",
  address =	"T{\"u}bingen, Germany",
  publisher =	"Springer-Verlag LNAI 475",
  year =	"1989",
  pages =	"223--244",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Haberstrau94,
  author =	"Marianne Haberstrau",
  title =	"{ECOLOG}: An Environment for Constraint Logics",
  editor =	"J.-P. Jouannaud",
  booktitle =	"Proceedings of the First International Conference on
		  Constraints in Computational Logics",
  year =	1994,
  address =	"Munich, Germany",
  month =	sep,
  pages =       "237--252",
  publisher =   "Springer-Verlag LNCS 845",
  keywords = 	"rewriting"
}

@Article{Hagiya89,
  author =	"Masami Hagiya",
  title =	"Generalization from Partial Parameterization in Higher-Order
		  Type Theory",
  journal =	"Theoretical Computer Science",
  year =	"1989",
  volume =	"63",
  pages =	"113--139",
  keywords = 	"unification"
}

@InProceedings{Hagiya90,
  author =	"Masami Hagiya",
  title =	"Programming by Example and Proving by Example Using
		  Higher-order Unification",
  booktitle =	"Proceedings of the 10th International Conference on Automated
		  Deduction",
  editor =	"M. E. Stickel",
  publisher =	"Springer-Verlag LNAI 449",
  address =	"Kaiserslautern, Germany",
  month =	jul,
  year =	"1990",
  pages =	"588--602",
  keywords = 	"unification"
}

@InProceedings{Hagiya91,
  author =	"Masami Hagiya",
  title =	"From Programming-by-Example to Proving-by-Example",
  booktitle =	"Proceedings of the International Conference on Theoretical
		  Aspects of Computer Software",
  editor =	"T. Ito and A. R. Meyer",
  publisher =	"Springer-Verlag LNCS 526",
  address =	"Sendai, Japan",
  month =	sep,
  year =	"1991",
  pages =	"387--419",
  keywords = 	"unification"
}

@TechReport{Hagiya95,
  author = 	 "Masami Hagiya and Yozo Toda",
  title = 	 "On Implicit Arguments",
  institution =  "Department of Information Science, University of Tokyo",
  year = 	 1995,
  number =	 "91-1",
  month =	 jan,
  keywords =	 "misc",
  urlps =	 "ftp://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/takasu/z.ps"
}

@Article{Halang95,
  author = 	 "W. A. Halang and B. Kr{\"a}mer and N. V{\"o}lker",
  title = 	 "Formally Verified Building Blocks in Functional Logic
                  Diagrams for Emergency Shutdown System Design",
  journal =	 "High Integrity Systems",
  year =	 1995,
  volume =	 1,
  number =	 3,
  pages =	 "277--286",
  keywords =	 "Isabelle",
  annote =	 "Contains Isabelle verification of a timer program."
}

@InCollection{Hallnas87,
  author =	"Lars Halln{\"a}s",
  title =	"A Note on the Logic of a Logic Program",
  booktitle =	"Proceedings of the Workshop on Programming Logic",
  publisher =	"University of G{\"o}teborg and Chalmers University of
		  Technology, Report PMG-R37",
  year =	1987,
  keywords = 	"Pi"
}

@Article{Hallnas91,
  author =	"Lars Halln{\"a}s",
  title =	"Partial Inductive Definitions",
  journal =	"Theoretical Computer Science",
  year =	1991,
  volume =	87,
  number =	1,
  pages =	"115--142",
  month =	sep,
  keywords = 	"Pi"
}

@InProceedings{Hannan88iclp,
  author =	"John Hannan and Dale Miller",
  title =	"Uses of Higher-Order Unification for Implementing Program
		  Transformers",
  editor =	"Kenneth A. Bowen and Robert A. Kowalski",
  booktitle =	"Fifth International Logic Programming Conference",
  address =	"Seattle, Washington",
  publisher =	"MIT Press",
  pages =	"942--959",
  month =	aug,
  year =	1988,
  keywords = 	"lambda-Prolog"
}

@TechReport{Hannan88tr,
  author =	"John Hannan and Dale Miller",
  title =	"Enriching a Meta-Language with Higher-Order Features",
  institution =	"University of Pennsylvania",
  number =	"MS-CIS-88-45",
  month =	jun,
  year =	1988,
  keywords =	"lambda-Prolog"
}

@InCollection{Hannan89meta,
  author =	"John Hannan and Dale Miller",
  title =	"A Meta-Logic for Functional Programming",
  chapter =	"24",
  booktitle =	"Meta-Programming in Logic Programming",
  editor =	"H. Abramson and M. Rogers",
  publisher =	"MIT Press",
  pages =	"453-476",
  year =	1989,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan89mpc,
  author =	"John Hannan and Dale Miller",
  title =	"Deriving Mixed Evaluation from Standard Evaluation for a
		  Simple Functional Programming Language",
  booktitle =	"Proceedings of the International Conference on Mathematics of
		  Program Construction",
  editor =	"J.L.A. van de Snepscheut",
  publisher =	"Springer-Verlag LNCS 375",
  year =	1989,
  pages =	"239--255",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan90,
  author =	"John Hannan and Dale Miller",
  title =	"From Operational Semantics to Abstract Machines: Preliminary
		  Results",
  booktitle =	"Proceedings of the 1990 ACM Conference on Lisp and Functional
		  Programming",
  editor =	"M. Wand",
  address =	"Nice, France",
  pages =	"323--332",
  year =	1990,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan91elp,
  author =	"John Hannan",
  title =	"Implementing {$\lambda$}-Calculus Reduction Strategies
		  in Extended Logic Programming Languages",
  booktitle =	"Proceedings of the Second Workshop on Extensions to Logic
		  Programming",
  editor =	"Lars-Henrik Eriksson and Lars Halln{\"{a}}s and Peter
		  Schroeder-Heister",
  publisher =	"Springer-Verlag LNAI 596",
  pages =	"193--219",
  month =	jan,
  year =	1991,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan91pepm,
  author =	"John Hannan",
  title =	"Staging Transformations for Abstract Machines",
  booktitle =	"Proceedings of the {ACM SIGPLAN} Symposium on Partial
		  Evaluation and Semantics Based Program Manipulation",
  editor =	"P. Hudak and N. Jones",
  address =	"New Haven, Connecticut",
  pages =	"130--141",
  month =	jun,
  year =	"1991",
  keywords = 	"lambda-Prolog"
}

@PhdThesis{Hannan91phd,
  author =	"John J. Hannan",
  title =	"Investigating a Proof-Theoretic Meta-Language for Functional
		  Programs",
  school =	"University of Pennsylvania",
  month =	jan,
  year =	1991,
  note =	"Available as Technical Report MS-CIS-91-09",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan92lics,
  author =	"John Hannan and Frank Pfenning",
  title =	"Compiler Verification in {LF}",
  booktitle =	"Seventh Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Santa Cruz, California",
  month =	jun,
  year =	"1992",
  editor =	"Andre Scedrov",
  pages =	"407--418",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/lics92.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/lics92.ps.gz",
  keywords = 	"LF, Elf"
}

@Article{Hannan92mscs,
  author =	"John Hannan and Dale Miller",
  title =	"From Operational Semantics to Abstract Machines",
  journal =	"Mathematical Structures in Computer Science",
  volume =	"2",
  number =	"4",
  year =	"1992",
  pages =	"415--459",
  keywords = 	"lambda-Prolog",
  urldvi =	"ftp://ftp.cse.psu.edu/pub/hannan/mscs.dvi"
}

@Article{Hannan93jfp,
  author =	"John Hannan",
  title =	"Extended Natural Semantics",
  journal =	"Journal of Functional Programming",
  year =	"1993",
  volume =	"3",
  number =	"2",
  pages =	"123--152",
  month =	apr,
  urldvi =	"ftp://ftp.cse.psu.edu/pub/hannan/jfp.dvi",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Hannan93pepm,
  author =	"John Hannan",
  title =	"Searching for Semantics",
  booktitle =	"Proceedings of the ACM SIGPLAN Symposium on Partial
		  Evaluation and Semantics Based Program Manipulation",
  editor =	"D. Schmidt",
  address =	"Copenhagen, Denmark",
  pages =	"1--12",
  month =	jun,
  year =	"1993",
  urldvi =      "ftp://ftp.cse.psu.edu/pub/hannan/pepm.dvi",
  keywords = 	"LF, Elf"
}

@InProceedings{Harland97,
  author = 	 "James Harland and David Pym",
  title = 	 "Resource-Distribution via Boolean Constraints",
  editor =	 "W. McCune",
  pages =	 "222--236",
  booktitle =	 "Proceedings of the 14th International Conference on
		  Automated Deduction (CADE-14)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNAI 1249",
  address =	 "Townsville, Australia",
  month =	 jul,
  keywords =	 "linear"
}

@InProceedings{Harper87,
  author =	"Robert Harper and Furio Honsell and Gordon Plotkin",
  title =	"A Framework for Defining Logics",
  booktitle =	"Symposium on Logic in Computer Science",
  publisher =	"IEEE Computer Society Press",
  month =	jun,
  year =	"1987",
  pages =	"194--204",
  keywords = 	"LF"
}

@TechReport{Harper88,
  author = 	 "Robert Harper",
  title = 	 "An Equational Formulation of {LF}",
  institution =  "University of Edinburgh",
  year = 	 1988,
  number =	 "ECS-LFCS-88-67",
  keywords =	 "LF, Elf"
}

@InProceedings{Harper89cat,
  author =	"Robert Harper and Donald Sannella and Andrzej Tarlecki",
  title =	"Logic Representation",
  booktitle =	"Proceedings of the Workshop on Category Theory and Computer
		  Science",
  address =	"Manchester, UK",
  pages =	"250--272",
  editor =	"D.H. Pitt and D.E. Rydeheard and P. Dybjer and A.M. Pitts and
		  A. Poigne\'{e}",
  publisher =	"Springer-Verlag LNCS 389",
  month =	sep,
  year =	"1989",
  keywords = 	"LF"
}

@InProceedings{Harper89lics,
  author =	"Robert Harper and Donald Sannella and Andrzej Tarlecki",
  title =	"Structure and Representation in {LF}",
  booktitle =	"Fourth Annual Symposium on Logic in Computer Science",
  address =	"Pacific Grove, California",
  publisher =	"IEEE Computer Society Press",
  month =	jun,
  year =	"1989",
  pages =	"226--237",
  keywords = 	"LF"
}

@TechReport{Harper90,
  author =	"Robert Harper",
  title =	"Systems of Polymorphic Type Assignment in {LF}",
  institution =	"Carnegie Mellon University",
  address =	"Pittsburgh, Pennsylvania",
  number =	"CMU-CS-90-144",
  month =	jun,
  year =	"1990",
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/pta90.dvi.gz",
  keywords = 	"LF"
}

@Article{Harper93jacm,
  author =	"Robert Harper and Furio Honsell and Gordon Plotkin",
  title =	"A Framework for Defining Logics",
  journal =	"Journal of the Association for Computing Machinery",
  volume =	"40",
  number =	"1",
  month =	jan,
  year =	"1993",
  pages =	"143--184",
  urldvi =	"http://www.cs.cmu.edu/~fp/elf-papers/jacm93.dvi.gz",
  keywords = 	"LF"
}

@Article{Harper94,
  author = 	 "Robert Harper and Donald Sannella and Andrzej Tarlecki",
  title = 	 "Structured Presentations and Logic Representations",
  journal =	 "Annals of Pure and Applied Logic",
  year =	 1994,
  volume =	 67,
  pages =	 "113--160",
  keywords =	 "LF",
  urlps =	 "http://www.dcs.ed.ac.uk/staff/dts/pub/apal.ps"
}
		  
@Article{Harper98jlc,
  author = 	 "Robert Harper and Frank Pfenning",
  title = 	 "A Module System for a Programming Language Based on
		  the {LF} Logical Framework",
  journal =	 "Journal of Logic and Computation",
  year =	 1998,
  volume =	 8,
  number =	 1,
  pages =	 "5--31",
  keywords =	 "LF, Elf"
}

@TechReport{Harrison97,
  author = 	 "John Harrison",
  title = 	 "Floating Point Verification in {HOL} {Light}: The
		  Exponential Function",
  institution =  "University of Cambridge Computer Laboratory",
  year = 	 1997,
  number =	 428,
  keywords =	 "misc",
  urlhtml =	 "http://www.cl.cam.ac.uk/users/jrh/papers/tang.html"
}

@InProceedings{Hatcliff95,
  author = 	 "John Hatcliff",
  title = 	 "Mechanically Verifying the Correctness of an Offline Partial
		  Evaluator",
  booktitle = 	 "Proceedings of the 7th International Symposium on
		  Programming  Languages: Implementations, Logics and
		  Programs",
  editor =	 "M. Hermenegildo and S.D. Swierstra",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 982",
  address =	 "Utrecht, The Netherlands",
  month =	 "September",
  pages =	 "279--298",
  keywords =     "LF, Elf",
  urlps =	 "http://www.diku.dk/research-groups/topps/personal/hatcliff/plilp95.ps.gz"
}

@InProceedings{Hasegawa99tlca,
  author = 	 "Masahito Hasegawa",
  title = 	 "Logical Predicates for Intuitionistic Linear Type Theories",
  editor =	 "Jean-Yves Girard",
  pages =	 "198--212",
  booktitle =	 "Proceedings of the 4th International Conference on Typed
		  Lambda Calculi and Applications (TLCA'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1581",
  address =	 "L'Aquila, Italy",
  month =	 apr,
  keywords =	 "linear"
}

@Article{Hedberg91,
  author = 	"Michael Hedberg",
  title = 	"Normalizing the Associative Law --- an Experiment with
		 {Martin-L\"of's} Type Theory",
  journal = 	"Formal Aspects of Computing",
  year = 	1991,
  volume = 	3,
  pages = 	"218--252",
  note =	"Extended version available as Licentiate Thesis, Chalmers
		  University of Technology, 1990",
  keywords =	"Isabelle"
}

@InProceedings{Hill95,
  author = 	 "Steve Hill and Simon Thompson",
  title = 	 "Miranda in {Isabelle}",
  editor =	 "L.C. Paulson",
  pages =	 "122--135",
  booktitle =	 "Proceedings of the First Isabelle Users Workshop",
  year =	 1995,
  publisher =	 "University of Cambridge Computer Laboratory",
  month =	 sep,
  note =	 "Availabe as Technical Report 397",
  keywords =	 "Isabelle",
  url =		 "http://www.cs.ukc.ac.uk/pubs/1995/209"
}

@InProceedings{Hirschkoff97,
  author = 	 "Daniel Hirschkoff",
  title = 	 "A Full Formalization of Pi-Calculus Theory in the
                  {Calculus of Constructions}",
  editor =	 "E. Gunter and A. Felty",
  pages =        "153--169",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
                  Proving in Higher Order Logics (TPHOLs'97)",
  address =      "Murray Hill, New Jersey",
  year =	 1997,
  month =	 aug,
  keywords =	 "misc"
}

@Article{Hodas94ic,
  author =	"Joshua Hodas and Dale Miller",
  title =	"Logic Programming in a Fragment of Intuitionistic Linear
		  Logic", 
  journal =	"Information and Computation",
  year =	"1994",
  volume=	"110",
  number=	"2",
  pages=	"327--365",
  note =	"A preliminary version appeared in the Proceedings of the
		  Sixth Annual IEEE Symposium on Logic in Computer Science,
		  pages 32--42, Amsterdam, The Netherlands, July 1991",
  urlps =	"file://ftp.cis.upenn.edu/pub/papers/miller/ic94.ps.Z",
  keywords =	"linear"
}

@PhdThesis{Hodas94phd,
  author =	"Joshua S. Hodas",
  title =	"Logic Programming in Intuitionistic Linear Logic: Theory,
		  Design, and Implementation",
  school =	"University of Pennsylvania, Department of Computer and
		  Information Science",
  year =	"1994",
  keywords = 	"linear"
}
		  
@InProceedings{Hofmann99lics,
  author = 	 "Martin Hofmann",
  title = 	 "Semantical Analysis for Higher-Order Abstract Syntax",
  editor =	 "G. Longo",
  pages =	 "204--213",
  booktitle =	 "Proceedings of the 14th Annual Symposium on Logic in
		  Computer Science (LICS'99)",
  year =	 1999,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "misc"
}

@Article{Huet73,
  author =	"G\'{e}rard Huet",
  title =	"The Undecidability of Unification in Third Order Logic",
  journal =	"Information and Control",
  volume =	"22",
  number =	"3",
  year =	"1973",
  pages =	"257--267",
  keywords = 	"unification"
}

@Article{Huet75,
  author =	"G\'{e}rard Huet",
  title =	"A Unification Algorithm for Typed $\lambda$-Calculus",
  journal =	"Theoretical Computer Science",
  volume =	"1",
  year =	"1975",
  pages =	"27--57",
  keywords = 	"unification"
}

@TechReport{Huet93,
  author =	"G\'{e}rard Huet",
  title =	"An Analysis of {B{\"o}hm's} Theorem",
  institution =	"INRIA",
  year =	1993,
  number =	2008,
  address =	"Rocquencourt, France",
  month =	aug,
  keywords = 	"misc"
}

@Article{Huet94,
  author = 	 "G{\'e}rard Huet",
  title = 	 "Residual Theory in $\lambda$-Calculus: A Formal Development",
  journal =	 "Journal of Functional Programming",
  year =	 1994,
  volume =	 4,
  number =	 3,
  pages =	 "371--394",
  month =	 jul,
  note =	 "Preliminary version available as INRIA Technical Report
		  2009, August 1993",
  keywords =	 "misc"
}

@Article{Ishtiaq98,
  author = 	 "Samin Ishtiaq and David Pym",
  title = 	 "A Relevant Analysis of Natural Deduction",
  journal =	 "Journal of Logic and Computation",
  year =	 1998,
  volume =	 8,
  number =	 6,
  pages =	 "809--838",
  keywords =	 "LF, linear"
}

@InProceedings{Jayaraman91,
  author =	"Bharat Jayaraman and Gopalan Nadathur",
  title =	"Implementation Techniques for Scoping Constructs in Logic
		  Programming",
  editor =	"Koichi Furukawa",
  booktitle =	"Proceedings of the Eighth International Logic Programming
		  Conference",
  address =	"Paris, France",
  publisher =	"MIT Press",
  pages =	"871--886",
  month =	jun,
  year =	"1991",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Jouannaud99lics,
  author = 	 "J.-P. Jouannaud and A. Rubio",
  title = 	 "The Higher-Order Recursive Path Ordering",
  editor =	 "G. Longo",
  pages =	 "402--411",
  booktitle =	 "Proceedings of the 14th Annual Symposium on Logic in
		  Computer Science (LICS'99)",
  year =	 1999,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "rewriting"
}
		  
@PhdThesis{Jutting77,
  author =	"{L.S. van Benthem} Jutting",
  title =	"Checking {Landau's} ``{Grundlagen}'' in the {AUTOMATH}
		  System",
  school =	"Eindhoven University of Technology",
  year =	1977,
  keywords = 	"Automath"
}

@InProceedings{Jutting93,
  author = 	"{L.S. van Benthem} Jutting and James McKinna and
                 Robert Pollack",
  title = 	"Checking Algorithms for {P}ure {T}ype {S}ystems",
  booktitle = 	"Proceedings of the International Workshop on
                 Types for Proofs and Programs",
  month =	may,
  address =	"Nijmegen, The Netherlands",
  editor = 	"Henk Barendregt and Tobias Nipkow",
  pages =	"19--61",
  publisher = 	"Springer-Verlag LNCS 806",
  year = 	"1994",
  keywords =	"misc"
}

@InProceedings{Kahrs95,
  author = 	 "Stefan Kahrs",
  title = 	 "Towards a Domain Theory for Termination Proofs",
  editor =	 "Jieh Hsiang",
  booktitle =	 "Proceedings of the Sixth International Conference on
		  Rewriting Techniques and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 914",
  address =	 "Kaiserslautern, Germany",
  month =	 apr,
  pages =	 "241--255",
  keywords =	 "rewriting"
}

@MastersThesis{Kammuller95,
  author = 	"F. Kamm{\"u}ller",
  title = 	"Experimental Support of a Proof Programming Language with
		  {Isabelle}",
  school = 	"Technical University Berlin",
  year = 	1995,
  type =	"Diplomarbeit",
  keywords =	"isabelle",
  urlps =	"http://www.cs.tu-berlin.de/~simons/papers/kammuellerda.ps.gz"
}

@InProceedings{Kirchner94,
  author =	"Claude Kircher and H{\'e}l{\`e}ne Kirchner and Marian Vittek",
  title =	"Implementing Computational Systems with Constraints",
  booktitle =	"Proceedings of the First Workshop on Principles
		  and Practice of Constraints Programming",
  editor =	"P. van Hentenryck and V. Saraswat",
  publisher =	"MIT Press",
  address =	"Newport, Rhode Island",
  month =	apr,
  year =	"1993",
  keywords = 	"rewriting"
}

@Book{Kirchner98,
  title = 	 "Proceedings of the International Workshop on Rewriting Logic
		  and its Applications",
  publisher = 	 "Elsevier Science",
  year = 	 1998,
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  volume =	 15,
  series =	 "Electronic Notes in Theoretical Computer Science",
  address =	 "Pont-{\`a}-Mousson, France",
  month =	 sep,
  keywords =	 "rewriting",
  url =		 "http://www.elsevier.com/locate/entcs/volume15.html"
}

@InProceedings{Kohlhase93,
  author =	"Michael Kohlhase and Frank Pfenning",
  title =	"Unification in a {$\lambda$}-Calculus with Intersection
		  Types",
  booktitle =	"Proceedings of the International Logic Programming Symposium",
  editor =	"Dale Miller",
  publisher =	"MIT Press",
  address =	"Vancouver, Canada",
  month =	oct,
  year =	"1993",
  pages =	"488--505",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/ilps93.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/ilps93.ps.gz",
  keywords = 	"unification, LF, Elf"
}

@InProceedings{Kolyang96fme,
   author =	"Kolyang and T. Santen and B. Wolff",
   booktitle =  "Symposium on Industrial Benefits and Advances in Formal
		 Methods (FME'96)",
   editor = 	"M.-C. Gaudel and J. Woodcock",
   pages = 	"629--648",
   publisher = 	"Springer-Verlag LNCS 1051",
   title = 	"Correct and User-Friendly Implementation of Transformation
   		 Systems",
   month =	mar,
   address =	"Oxford, England",
   year = 	1996,
   urlps = 	"http://www.informatik.uni-bremen.de/~bu/papers/yats.ps.gz",
   keywords =	"Isabelle"
}

@InProceedings{Kolyang96tphol,
   author =	"Kolyang and T. Santen and B. Wolff",
   booktitle =  "Proceedings of the 9th International Conference on Theorem
		 Proving in Higher Order Logics",
   address =	"Turku, Finland",
   editor =	"J. von Wright and J. Grundy and J. Harrison",
   pages =	"283--298",
   publisher =  "Springer-Verlag LNCS 1125",
   title = 	"A Structure Preserving Encoding of {Z} in {Isabelle/HOL}",
   month =	aug,
   year =       "1996",
   keywords =	"Isabelle"
}

@InProceedings{Kolyang97tapsoft,
  author = 	 "Kolyang and C. L{\"u}th and T. Meier and B. Wolff",
  title = 	 "{TAS} and {IsaWin}: Generic Interfaces for
                  Transformational Program Development and Theorem Proving",
  editor =	 "M. Bidoit and M. Dauchet",
  pages =	 "855--858",
  booktitle =	 "Proceedings of the Seventh International Joint
                  Conference on the Theory and Practice of Software
                  Development (TAPSOFT'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1214",
  address =	 "Lille, France",
  month =	 apr,
  note =	 "System abstract",
  keywords =	 "Isabelle"
}

@InProceedings{Kolyang97tsvv,
  author = 	 "Kolyang and C. L{\"u}th and T. Meier and B. Wolff",
  title = 	 "Generic Interfaces for Transformation Systems and
                  Interactive Theorem Provers",
  editor =	 "K. Berghammer and J. Peleska and B. Buth",
  booktitle =	 "Proceedings of the International Workshop for Tool
                  support in Verification and Validation",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS",
  keywords =	 "Isabelle"
}

@InProceedings{Kwon93,
  author = 	 "Keehand Kwon and Gopalan Nadathur and Debra Sue Wilson",
  title = 	 "Implementing a Notion of Modules in the Logic Programming
		  Language {$\lambda$Prolog}",
  editor =	 "E. Lamma and P. Mello",
  pages =	 "359--393",
  booktitle =	 "Proceedings of the Third International Workshop on
		  Extensions of Logic Programming",
  year =	 1993,
  publisher =	 "Springer-Verlag LNAI 660",
  address =	 "Bologna, Italy",
  month =	 feb,
  keywords =	 "lambda-Prolog",
  urldvi =	 "http://cs-www.uchicago.edu/~gopalan/papers/modimp.dvi.Z"
}

@Article{Kwon94cl,
  author =	"Keehang Kwon and Gopalan Nadathur and Debra Sue Wilson",
  title =	"Implementing Polymorphic Typing in a Logic Programming
		  Language",
  journal =	"Computer Languages",
  volume =	"20",
  number =	"1",
  pages =	"25--42",
  year =	"1994",
  urldvi =      "http://cs-www.uchicago.edu/~gopalan/papers/typesimp.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@PhdThesis{Kwon94phd,
  author = 	 "Keehang Kwon",
  title = 	 "Towards a Verified Abstract Machine for a Logic Programming
		  Language with a Notion of Scope",
  school = 	 "Department of Computer Science, Duke University",
  year = 	 1994,
  month =	 dec,
  note =	 "Available as Technical Report CS-1994-36",
  keywords =	 "lambda-Prolog",
  urlps =	 "ftp://ftp.cs.duke.edu/dist/papers/lprolog/scopeimp-ver.ps.Z"
}

@Book{Landau30,
  author =	"Edmund Landau",
  title =	"Grundlagen der Analysis",
  publisher =	"Akademische Verlagsgesellschaft",
  year =	1930,
  address =	"Leipzig, Germany",
  note =	"English translation {\it Foundations of Analysis}, Chelsea
		  Publishing Company, 1951",
  keywords = 	"Automath"
}

@InProceedings{Leclerc95,
  author = 	 "F. Leclerc",
  title = 	 "Termination Proof of Term Rewriting System with the Multiset
		  Path Ordering and Derivation Length: A Complete Development
		  in the {Calculus of Constructions}", 
  editor =	 "M. Dezani-Ciancaglini and G. Plotkin",
  booktitle =	 "Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 902",
  address =	 "Edinburgh, Scotland",
  month =	 apr,
  pages =	 "312--327",
  keywords =     "rewriting, misc"
}

@PhdThesis{Leleu98,
  author = 	 "Pierre Leleu",
  title = 	 "Induction et Syntaxe Abstraite d'Ordre Sup{\'e}rieur
		  dans les Th{\'e}ories Typ{\'e}es",
  school = 	 "Ecole Nationale des Ponts et Chaussees",
  year = 	 1998,
  address =	 "Marne-la-Vallee, France",
  month =	 dec,
  keywords =	 "misc"
}

@InProceedings{Lester94,
  author = 	 "D. Lester and S. Mintchev",
  title = 	 "Towards Machine-Checked Compiler Correctness for
		  Higher-Order Languages",
  editor =       "L. Pacholski and J. Tiuryn",
  booktitle =	 "Proceedings of the 8th Workshop on Computer Science Logic (CSL'94)",
  year =	 1994,
  address =      "Kazimierz, Poland",
  month =        sep,
  publisher =	 "Springer LNCS 933",
  keywords =     "Isabelle"
}

@InProceedings{Levy96,
  author = 	 "Jordi Levy",
  title = 	 "Linear Second-Order Unification",
  editor =	 "Harald Ganzinger",
  pages =	 "332--346",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "unification"
}

@PhdThesis{Liang95,
  author = 	 "Chuck Liang",
  title = 	 "Object-Level Substitution, Unification and Generalization in
		  Meta-Logic",
  school = 	 "University of Pennsylvania",
  year = 	 1995,
  month =	 aug,
  keywords =	 "lambda-Prolog, unification",
  urlps =	 "ftp://ftp.cis.upenn.edu/pub/papers/liang/thesis.ps.Z"
}

@InProceedings{Liang96,
  author = 	 "Chuck Liang",
  title = 	 "Substitutions for Proofs and Types as Logic Programming",
  editor =	 "Didier Galmiche",
  pages = 	 "61--68",
  booktitle =	 "Informal Proceedings of the Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1996,
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =     "LF"
}

@InProceedings{Lugiez94,
  author =	"D. Lugiez",
  title =	"Higher-Order Disunification: Some Decidable Cases",
  editor =	"J.-P. Jouannaud",
  booktitle =	"Proceedings of the First International Conference on
		  Constraints in Computational Logics",
  year =	1994,
  address =	"Munich, Germany",
  month =	sep,
  pages =       "121--135",
  publisher =   "Springer-Verlag LNCS 845",
  keywords = 	"unification, rewriting"
}

@TechReport{Luo92,
  author = 	"Zhaohui Luo and Robert Pollack",
  title = 	"The {LEGO} Proof Development System: A User's Manual",
  institution = 	"University of Edinburgh",
  month =	may,
  year = 	"1992",
  number = 	"ECS-LFCS-92-211",
  keywords =	"misc"
}

@inproceedings{Lysne95,
  author = 	 "Olav Lysne and Javier Piris",
  title = 	 "A Termination Ordering for Higher Order Rewrite Systems",
  editor =	 "Jieh Hsiang",
  booktitle =	 "Proceedings of the Sixth International Conference on
		  Rewriting Techniques and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 914",
  address =	 "Kaiserslautern, Germany",
  month =	 apr,
  pages =        "26--40",
  keywords =	 "rewriting"
}

@InProceedings{Magnusson93,
  author =	"Lena Magnusson",
  title =	"Refinement and local undo in the interactive proof editor
		  {ALF}",
  booktitle =	"Proceedings of the Workshop on Types for Proofs and Programs",
  address =	"Nijmegen, The Netherlands",
  year =	"1993",
  pages =	"191--208",
  keywords = 	"ALF"
}

@InCollection{Magnusson94,
  author =	"Lena Magnusson and Bengt Nordstr{\"o}m",
  title =	"The {ALF} Proof Editor and Its Proof Engine",
  booktitle =	"Types for Proofs and Programs",
  publisher =	"Springer-Verlag LNCS 806",
  year =	1994,
  editor =	"Henk Barendregt and Tobias Nipkow",
  pages =	"213--237",
  keywords = 	"ALF"
}

@PhdThesis{Magnusson95,
  author = 	 "Lena Magnusson",
  title = 	 "The Implementation of {ALF}---A Proof Editor Based on
		  {Martin-L{\"o}f's} Monomorphic Type Theory with Explicit
		  Substitution",
  school = 	 "Chalmers University of Technology and G{\"o}teborg
		  University",
  year = 	 1995,
  month =	 jan,
  keywords =	 "ALF"
}

@TechReport{MartiOliet93,
  author =	"Narciso Mart{\`\i}-Oliet and Jose Meseguer",
  title =	"Rewriting Logic as a Logical and Semantical Framework",
  institution =	"SRI International",
  year =	1993,
  number =	"SRI-CSL-93-05",
  month =	aug,
  keywords = 	"rewriting"
}

@InProceedings{MartinLof80,
  author =	"Martin-L{\"o}f, Per",
  title =	"Constructive Mathematics and Computer Programming",
  booktitle =	"Logic, Methodology and Philosophy of Science VI",
  publisher =	"North-Holland",
  year =	"1980",
  pages =	"153--175",
  keywords = 	"misc"
}

@TechReport{MartinLof85tr,
  author =	"Per Martin-L{\"o}f",
  title =	"On the Meanings of the Logical Constants and the
		  Justifications of the Logical Laws",
  institution =	"Scuola di Specializzazione in Logica Matematica,
		  Dipartimento di Matematica, Universit\`a di Siena",
  number =	"2",
  year =	"1985",
  keywords = 	"misc"
}

@Unpublished{MartinLof85un,
  author =	"Per Martin-L{\"o}f",
  title =	"Truth of a Proposition, Evidence of a Judgement,
		  Validity of a Proof",
  month =	jun,
  year =	"1985",
  note =	"Notes to a talk given at the workshop {\em Theory
		  of Meaning}, Centro Fiorentino di Storia e Filosofia della
		  Scienza",
  keywords = 	"misc"
}

@TechReport{Mason87,
  author =	"Ian A. Mason",
  title =	"Hoare's Logic in the {LF}",
  institution =	"Laboratory for Foundations of Computer Science, University of
		  Edinburgh ",
  number =	"ECS-LFCS-87-32",
  month =	jun,
  year =	"1987",
  keywords =	"LF"
}

@InCollection{Matthews93,
  author =	"Se{\'a}n Matthews and Alan Smaill and David Basin",
  title =	"Experience with {$FS_0$} as a Framework Theory",
  booktitle =	"Logical Environments",
  editor =	"G{\'e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"61--82",
  year =	1993,
  keywords =	"FS0"
}

@InCollection{Matthews94,
  author =	"Se{\'a}n Matthews",
  title =	"A Theory and its Metatheory in {$FS_0$}",
  editor =	"Dov Gabbay and Franz Guenthner",
  booktitle =	"What is a Logical System?",
  publisher =	"Oxford University Press",
  year =	1994,
  urldvi =      "http://www.mpi-sb.mpg.de/~sean/papers/metatheoryinFS0/metatheoryinFS0.dvi",
  urlps =	"http://www.mpi-sb.mpg.de/~sean/papers/metatheoryinFS0/metatheoryinFS0.ps",
  keywords = 	"FS0"
}

@InProceedings{McDowell96ll,
  author = 	 "Raymond McDowell and Dale Miller and Catuscia Palamidessi",
  title = 	 "Encoding Transition Systems in Sequent Calculus:
                  Preliminary Report",
  volume =	 3,
  series =	 "Electronic Notes in Theoretical Computer Science",
  booktitle =	 "Proceedings of the Workshop on Linear Logic",
  year =	 1996,
  publisher =	 "Elsevier",
  keywords =	 "misc",
  urlhtml =	 "http://pigeon.elsevier.nl/mcs/tcs/pc/volume3.htm#miller"
}

@InProceedings{McDowell97lics,
  author =       "Raymond McDowell and Dale Miller",
  title =        "A Logic for Reasoning with Higher-Order Abstract Syntax:
	          An Extended Abstract", 
  booktitle =    "Proceedings of the Twelfth Annual Symposium on
                  Logic in Computer Science",
  address =      "Warsaw, Poland",
  editor =       "Glynn Winskel",
  month =        jun,
  year =         1997,
  pages =        "434--445",
  keywords =     "Pi, misc",
  urlps =        "ftp://ftp.cis.upenn.edu/pub/papers/mcdowell/lrhoas.ps.gz"
}

@PhdThesis{McDowell97phd,
  author = 	 "Raymond McDowell",
  title = 	 "Reasoning in a Logic with Definitions and Induction",
  school = 	 "University of Pennsylvania",
  year = 	 1997
}

@InProceedings{McKinna93,
  author = 	"James McKinna and Robert Pollack",
  title = 	"{P}ure {T}ype {S}ytems Formalized",
  booktitle = 	"Proceedings of the International Conference on Typed
		 Lambda Calculi and Applications",
  year = 	"1993",
  editor = 	"M.Bezem and J.F.Groote",
  pages = 	"289--305",
  month = 	mar,
  publisher = 	"Springer-Verlag LNCS 664",
  keywords =	"misc"
}

@InProceedings{Mery91a,
  author =	"D. {M\'ery} and A. Mokkedem",
  title =	"A Proof Environment for a Subset of {SDL}",
  booktitle =	"Fifth {SDL} Forum Evolving Methods",
  year =	1991,
  editor =	"O. Faergemand and R. Reed",
  publisher =	"North-Holland",
  keywords = 	"Isabelle"
}

@InProceedings{Mery91b,
  author =	"D. {M\'ery} and A. Mokkedem",
  title =	"Demonstration of {Crocos}",
  booktitle =	"Fifth {SDL} Forum Evolving Methods",
  year =	1991,
  editor =	"O. Faergemand and R. Reed",
  publisher =	"North-Holland",
  keywords = 	"Isabelle"
}

@InProceedings{Mery92,
  author =	"D. {M\'ery} and A. Mokkedem",
  title =	"Crocos: an Integrated Environment for Interactive
		Verification of {SDL} Specifications",
  booktitle =	"Computer Aided Verification: Fourth International
		Workshop, {CAV} '92",
  year =	1993,
  editor =	"G. v. Bochmann and D. K. Probst",
  publisher =	"Springer-Verlag LNCS 663",
  keywords = 	"Isabelle"
}

@InProceedings{Meseguer87,
  author = 	 "Jos{\'e} Meseguer",
  title = 	 "General Logics",
  editor =	 "H.-D. Ebbinghaus",
  pages =	 "275--329",
  booktitle =	 "Logic Colloquium '87",
  year =	 1987,
  publisher =	 "North-Holland",
  address =	 "Granada, Spain",
  month =	 jul
}

@Book{Meseguer96,
  title = 	 "Proceedings of the First International Workshop on Rewriting
		  Logic and its Applications",
  publisher = 	 "Elsevier Science",
  year = 	 1998,
  editor =	 "Jos{\'e} Meseguer",
  volume =	 4,
  series =	 "Electronic Notes in Theoretical Computer Science",
  address =	 "Pacific Grove, California",
  month =	 sep,
  keywords =	 "rewriting",
  url =		 "http://www.elsevier.com/locate/entcs/volume4.html"
}

@InProceedings{Michaylov91,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"Natural Semantics and Some of its Meta-Theory in {Elf}",
  booktitle =	"Proceedings of the Second International Workshop on
		  Extensions of Logic Programming",
  editor =	"L.-H. Eriksson and L. Halln{\"a}s and P. Schroeder-Heister",
  publisher =	"Springer-Verlag LNAI 596",
  year =	"1991",
  address =	"Stockholm, Sweden",
  month =	jan,
  pages =	"299--344",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/elp91.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/elp91.ps.gz",
  keywords = 	"LF, Elf"
}

@InProceedings{Michaylov92,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"An Empirical Study of the Runtime Behavior of Higher-Order
		  Logic Programs",
  booktitle =	"Proceedings of the Workshop on the {$\lambda$Prolog}
		  Programming Language",
  editor =	"D. Miller",
  publisher =	"University of Pennsylvania",
  address =	"Philadelphia, Pennsylvania",
  month =	jul,
  year =	"1992",
  note =	"Available as Technical Report MS-CIS-92-86",
  pages =	"257--271",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/lpproc92.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/lpproc92.ps.gz",
  keywords = 	"LF, Elf"
}

@InProceedings{Michaylov93,
  author =	"Spiro Michaylov and Frank Pfenning",
  title =	"Higher-Order Logic Programming as Constraint Logic
		  Programming",
  booktitle =	"Position Papers for the First Workshop on Principles and
		  Practice of Constraint Programming",
  publisher =	"Brown University",
  address =	"Newport, Rhode Island",
  month =	apr,
  year =	"1993",
  pages =	"221--229",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/ppcp93.ps.gz",
  keywords = 	"LF, Elf"
}

@InCollection{Miculan94,
  author =	"Marino Miculan",
  title =	"The Expressive Power of Structural Operational Semantics
		  with Explicit Assumptions",
  booktitle =	"Types for Proofs and Programs",
  publisher =	"Springer-Verlag LNCS 806",
  year =	1994,
  editor =	"Henk Barendregt and Tobias Nipkow",
  pages =	"263--290",
  keywords = 	"LF, Elf"
}


@InProceedings{Miller86acl,
  author =	"Dale Miller and Gopalan Nadathur",
  title =	"Some Uses of Higher-Order Logic in Computational Linguistics",
  booktitle =	"Proceedings of the 24th Annual Meeting of the
		  Association for Computational Linguistics",
  pages =	"247--255",
  year =	1986,
  publisher =	"Association for Computational Linguistics, Morristown, New
		  Jersey",
  urldvi = 	"file://ftp.cis.upenn.edu/pub/papers/miller/acl86.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller86iclp,
  author =	"Dale Miller and Gopalan Nadathur",
  title =	"Higher-Order Logic Programming",
  booktitle =	"Proceedings of the Third International Logic
		  Programming Conference",
  pages =	"448--462",
  editor =	"Ehud Shapiro",
  address =	"London",
  month =	jun,
  year =	1986,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller86slp,
  author =	"Dale Miller",
  title =	"A Theory of Modules for Logic Programming",
  booktitle =	"Third Annual IEEE Symposium on Logic Programming",
  address =	"Salt Lake City, Utah",
  editor =	"Robert M. Keller",
  pages =	"106--114",
  month =	sep,
  year =	1986,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller87lics,
  author =	"Dale Miller and Gopalan Nadathur and Andre Scedrov",
  title =	"Hereditary {Harrop} Formulas and Uniform Proof Systems",
  booktitle =	"Symposium on Logic in Computer Science",
  pages =	"98-105",
  editor =	"David Gries",
  address =	"Ithaca, NY",
  month =	jun,
  year =	1987,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller87lmps,
  author =	"Dale Miller",
  title =	"Hereditary {Harrop} Formulas and Logic Programming",
  booktitle =	"Proceedings of the VIII International Congress of Logic,
		  Methodology, and Philosophy of Science",
  address =	"Moscow, Russia",
  pages =	"153--156",
  month =	aug,
  year =	"1987",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller87slp,
  author =	"Dale Miller and Gopalan Nadathur",
  title =	"A Logic Programming Approach to Manipulating Formulas
		  and Programs",
  booktitle =	"IEEE Symposium on Logic Programming",
  address =	"San Francisco",
  editor =	"Seif Haridi",
  pages =	"379-388",
  month =	sep,
  year =	1987,
  urlps =	"file://ftp.cis.upenn.edu/pub/papers/miller/slp87.ps.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller89iclp,
  author =	"Dale Miller",
  title =	"Lexical Scoping as Universal Quantification",
  editor =	"G. Levi and M. Martelli",
  booktitle =	"Proceedings of the Sixth International Conference on Logic
		  Programming",
  address =	"Lisbon, Portugal",
  publisher =	"MIT Press",
  pages =	"268--283",
  month =	jun,
  year =	1989,
  keywords = 	"lambda-Prolog"
}

@Article{Miller89jlp,
  author =	"Dale Miller",
  title =	"A Logical Analysis of Modules in Logic Programming",
  journal =	"Journal of Logic Programming",
  volume =	"6",
  number =	"1-2",
  month =	jan,
  year =	1989,
  pages =	"79--108",
  keywords = 	"lambda-Prolog"
}

@InCollection{Miller90,
  author =	"Dale Miller",
  title =	"Abstractions in Logic Programming",
  booktitle =	"Logic and Computer Science",
  editor =	"Piergiorgio Odifreddi",
  publisher =	"Academic Press",
  pages =	"329--359",
  year =	1990,
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/AbsInLP.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@Article{Miller91apal,
  author =	"Dale Miller and Gopalan Nadathur and Frank Pfenning and
		  Andre Scedrov",
  title =	"Uniform Proofs as a Foundation for Logic Programming",
  journal =	"Annals of Pure and Applied Logic",
  year =	"1991",
  volume =	"51",
  pages =	"125-157",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/apal91.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller91elp,
  author =	"Dale Miller",
  editor =	"Peter Schroeder-Heister",
  title =	"A Logic Programming Language with Lambda-Abstraction,
		  Function Variables, and Simple Unification",
  booktitle =	"Proceedings of the International Workshop on Extensions of
		  Logic Programming",
  address =	"T{\"u}bingen, Germany",
  publisher =	"Springer-Verlag LNAI 475",
  year =	"1989",
  pages =	"253--281",
  keywords = 	"lambda-Prolog, unification"
}

@InProceedings{Miller91iclp,
  author =	"Dale Miller",
  title =	"Unification of Simply Typed Lambda-Terms as Logic
		  Programming",
  editor =	"Koichi Furukawa",
  booktitle =	"Eighth International Logic Programming Conference",
  address =	"Paris, France",
  publisher =	"MIT Press",
  month =	jun,
  year =	"1991",
  pages =	"255--269",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/iclp91.dvi.Z",
  keywords = 	"lambda-Prolog, unification"
}

@Article{Miller91jlc,
  author =	"Dale Miller",
  title =	"A Logic Programming Language with Lambda-Abstraction,
		  Function Variables, and Simple Unification",
  journal =	"Journal of Logic and Computation",
  volume =	"1",
  number =	"4",
  pages =	"497--536",
  year =	"1991",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z",
  keywords = 	"lambda-Prolog, unification"
}

@Article{Miller92jsc,
  author =	"Dale Miller",
  title =	"Unification under a Mixed Prefix",
  year =	1992,
  journal =	"Journal of Symbolic Computation",
  pages =	"321--358",
  volume =	"14",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/jsc92.dvi.Z",
  keywords = 	"unification"
}

@Unpublished{Miller92lf,
  author = 	 "Dale Miller and Gordon Plotkin and David Pym",
  title = 	 "A Relevant Analysis of Natural Deduction",
  note = 	 "Talk given at the Workshop on Logical Frameworks,
		  B{\aa}stad, Sweden",
  year =	 1992,
  month =	 may,
  keywords =	 "LF, linear"
}

@Proceedings{Miller92lp,
  editor =	"Dale Miller",
  title =	"Proceedings of the Workshop on the $\lambda$Prolog
		  Programming Language",
  address =	"Philadelphia, Pennsylvania",
  month =	jul,
  year =	"1992",
  note =	"Available as University of Pennsylvania Technical Report
		  MS-CIS-92-86",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller92rclp,
  author =	"Dale Miller",
  title =	"Abstract Syntax and Logic Programming",
  booktitle =	"Proceedings of the First and Second Russian Conferences on
		  Logic Programming",
  address =	"Irkutsk and St.~Petersburg, Russia",
  year =	"1992",
  pages =	"322--337",
  publisher =	"Springer-Verlag LNAI 592",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/rclp91.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller93,
  author =	"Dale Miller",
  title =	"A Proposal for Modules in {$\lambda$Prolog}",
  booktitle =	"Proceedings of the 4th International Workshop on Extensions to
		  Logic Programming",
  editor =	"R. Dyckhoff",
  publisher =	"Springer-Verlag LNAI 798",
  year =	1993,
  urlps =	"file://ftp.cis.upenn.edu/pub/papers/miller/welp93.ps.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Miller94,
  author =	"Dale Miller",
  title =	"A Multiple-Conclusion Meta-Logic",
  booktitle =	"Ninth Annual {IEEE} Symposium on Logic in Computer Science",
  editor =	"S. Abramsky",
  address =	"Paris, France",
  month =	jul,
  year =	"1994",
  pages =	"272--281",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/lics94.dvi.Z",
  keywords = 	"linear"
}

@InProceedings{Muller95,
  author = 	 "Olaf M{\"u}ller and Tobias Nipkow",
  title = 	 "Combining Model Checking and Deduction of {I/O}-Automata",
  editor =	 "E. Brinksma",
  booktitle =	 "Proceedings of the First International Workshop on
                  Tools and Algorithms for the Construction and Analysis
                  of Systems",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 1019",
  address =	 "Aarhus, Denmark",
  month =	 may,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tacas.html"
}

@InProceedings{Muller97,
  author = 	 "Olaf M{\"u}ller and Tobias Nipkow",
  title = 	 "Traces of {I/O}-Automata in {Isabelle/HOLCF}",
  editor =	 "M. Bidoit and M. Dauchet",
  booktitle =	 "Proceedings of the Seventh International Joint
                  Conference on the Theory and Practice of Software
                  Development (TAPSOFT'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1214",
  address =	 "Lille, France",
  month =	 apr,
  keywords =	 "Isabelle",
  urlhtml =      "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tapsoft97.html"
}

@Article{Muller99jfp,
  author = 	 "Olaf M{\"u}ller and Tobias Nipkow and David von Oheimb and
		  Oscar Slotosch",
  title = 	 "HOLCF = {HOL} + {LCF}",
  journal =	 "Journal of Functional Programming",
  year =	 1999,
  volume =	 9,
  pages =	 "191--223",
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/jfp99.html"
}

@PhdThesis{Nadathur87,
  author =	"Gopalan Nadathur",
  title =	"A Higher-Order Logic as the Basis for Logic Programming",
  school =	"University of Pennsylvania",
  month =	may,
  year =	1987,
  note =	"Available as Technical Report MS-CIS-87-48",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Nadathur88,
  author =	"Gopalan Nadathur and Dale Miller",
  title =	"An Overview of {$\lambda$Prolog}",
  editor =	"Kenneth A. Bowen and Robert A. Kowalski",
  booktitle =	"Fifth International Logic Programming Conference",
  address =	"Seattle, Washington",
  publisher =	"MIT Press",
  pages =	"810--827",
  month =	aug,
  year =	1988,
  keywords = 	"lambda-Prolog"
}

@InProceedings{Nadathur89,
  author =	"Gopalan Nadathur and Bharat Jayaraman",
  title =	"Towards a {WAM} Model for {$\lambda$Prolog}",
  booktitle =	"Proceedings of the North American Conference on Logic
		  Programming",
  editor =	"Ewing Lusk and Ross Overbeek",
  pages =	"1180--1198",
  address =	"Cleveland, Ohio",
  month =	oct,
  year =	1989,
  keywords = 	"lambda-Prolog"
}

@Article{Nadathur90jacm,
  author =	"Gopalan Nadathur and Dale Miller",
  title =	"Higher-order {Horn} Clauses",
  journal =	"Journal of the ACM",
  volume =	"37",
  number =	"4",
  month =	oct,
  year =	1990,
  pages =	"777--814",
  urldvi = 	"file://ftp.cis.upenn.edu/pub/papers/miller/jacm90.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Nadathur90lfp,
  author =	"Gopalan Nadathur and Debra Sue Wilson",
  title =	"A Representation of Lambda Terms Suitable for Operations on
		  Their Intensions",
  booktitle =	"Proceedings of the 1990 ACM Conference on Lisp and Functional
		  Programming",
  editor =	"M. Wand",
  pages =	"341-348",
  year =	1990,
  keywords = 	"lambda-Prolog"
}

@InCollection{Nadathur92,
  author =	"Gopalan Nadathur and Frank Pfenning",
  title =	"The Type System of a Higher-Order Logic Programming Language",
  pages =	"245--283",
  booktitle =	"Types in Logic Programming",
  editor =	"Frank Pfenning",
  year =	1992,
  publisher =	"MIT Press",
  keywords = 	"lambda-Prolog"
}

@Article{Nadathur93jar,
  author =	"Gopalan Nadathur",
  title =	"A Proof Procedure for the Logic of Hereditary {Harrop}
		  Formulas",
  journal =	"Journal of Automated Reasoning",
  volume =	11,
  number =	1,
  year =	1993,
  month =	aug,
  pages =	"115--145",
  urldvi =      "http://cs-www.uchicago.edu/~gopalan/papers/proofproc.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@TechReport{Nadathur93trb,
  author =	"Gopalan Nadathur and Bharat Jayaraman and Debra Sue Wilson",
  title =	"Implementation Considerations for Higher-Order Features in
		  Logic Programming",
  month =	jun,
  year =	1993,
  institution =	"Department of Computer Science, Duke University",
  number =	"CS-1993-16",
  urldvi =      "http://cs-www.uchicago.edu/~gopalan/papers/hoimp.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@TechReport{Nadathur94trb,
  author =	"Gopalan Nadathur",
  title =	"A Notation for Lambda Terms {II}: Refinements and
		  Applications",
  month =	jan,
  year =	1994,
  institution =	"Department of Computer Science, Duke University",
  number =	"CS-1994-01",
  urldvi =      "http://cs-www.uchicago.edu/~gopalan/papers/lamnot1.dvi.Z",
  keywords = 	"lambda-Prolog"
}

@Article{Nadathur95jlp,
  author = 	 "Gopalan Nadathur and Bharat Jayaraman and Keehang Kwon",
  title = 	 "Scoping Constructs in Logic Programming: Implementation
		  Problems and their Solution",
  journal =	 "Journal of Logic Programming",
  year =	 1995,
  volume =	 25,
  number =	 2,
  pages =	 "119--161",
  month =	 nov,
  keywords =	 "lambda-Prolog"
}

@InProceedings{Nadathur95lics,
  author = 	 "Gopalan Nadathur and Donald W. Loveland",
  title = 	 "Uniform Proofs and Disjunctive Logic Programming",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 jun,
  pages =	 "148--155",
  note =	 "Available as Technical Report CS-1994-40,
		  Department of Computer Science, Duke University, December
		  1994",
  keywords =     "lambda-Prolog",
  urlps =	 "http://www.cs.duke.edu/~gopalan/ftp/updisj.ps.Z"
}

@Article{Nadathur97tcs,
  author = 	 "Gopalan Nadathur",
  title = 	 "Correspondences between Classical, Intuitionistic and
		  Uniform Provability",
  journal =	 "Theoretical Computer Science",
  year =	 1997,
  note =	 "To appear.  Available as Technical Report TR-97-12,
		  Department of Computer Science, University of Chicago",
  keywords =	 "lambda-Prolog",
  urlps =	 "http://www.cs.uchicago.edu/~gopalan/papers/classandint.ps.Z"
}

@Article{Nadathur98tcs,
  author = 	 "Gopalan Nadathur and Debra Sue Wilson",
  title = 	 "A Notation for Lambda Terms: A Generalization of
		  Environments",
  journal =	 "Theoretical Computer Science",
  year =	 1998,
  volume =	 198,
  number =	 "1--2",
  pages =	 "49--98",
  month =	 may,
  note =	 "Previous version available as Technical Report TR-97-01,
		  Department of Computer Science, University of Chicago",
  keywords =	 "lambda-Prolog",
  urlps =	 "http://www.cs.uchicago.edu/~gopalan/papers/lamnot1.ps.Z"
}

@InProceedings{Nadathur98westapp,
  author = 	 "Gopalan Nadathur",
  title = 	 "An Explicit Substitution Notation in a {lambdaProlog} Implementation",
  booktitle =	 "Proceedings of the First International Workshop on Explicit
		  Substitutions",
  year =	 1998,
  address =	 "Tsukuba, Japan",
  note =	 "Available as Technical Report TR-98-01, Department of
		  Computer Science, University of Chicago",
  keywords =	 "lambda-Prolog",
  urlps =	 "http://www.cs.uchicago.edu/~gopalan/papers/suspinhou.ps.Z"
}

@InCollection{Nadathur98handbook,
  author = 	 "Gopalan Nadathur and Dale Miller",
  title = 	 "Higher-Order Logic Programming",
  booktitle =	 "Handbook of Logic in Artificial Intelligence and Logic
		  Programming",
  publisher =	 "Oxford University Press",
  year =	 1998,
  editor =	 "D.M. Gabbay and C.J. Hogger and J.A. Robinson",
  volume =	 5,
  chapter =	 8,
  keywords =	 "lambda-Prolog"
}

@InProceedings{Nadathur99cade,
  author = 	 "Gopalan Nadathur and Dustin J. Mitchell",
  title = 	 "System Description: {Teyjus}---A Compiler and Abstract
		  Machine Based Implementation of Lambda Prolog",
  editor =	 "H. Ganzinger",
  pages =        "287--291",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "lambda-Prolog"
}

@Article{Nadathur99jflpa,
  author = 	 "Gopalan Nadathur",
  title = 	 "A Fine-Grained Notation for Lambda Terms and Its Use in
		  Intensional Operations",
  journal =	 "Journal of Functional and Logic Programming",
  year =	 1999,
  volume =       1999,
  number =	 2,
  month =	 mar,
  keywords =	 "lambda-Prolog",
  url =		 "http://www.cs.tu-berlin.de/journal/jflp/articles/1999/A99-02/A99-02.html"
}

@Article{Nadathur99jflpb,
  author = 	 "Gopalan Nadathur and Guanshan Tong",
  title = 	 "Realizing Modularity in {lambdaProlog}",
  journal =	 "Journal of Functional and Logic Programming",
  year =	 1999,
  volume =       1999,
  number =	 9,
  month =	 apr,
  keywords =	 "lambda-Prolog",
  url =		 "http://www.cs.tu-berlin.de/journal/jflp/articles/1999/S99-01/JFLP-A99-09.ps.gz"
}

@Unpublished{Naraschewski97,
  author = 	 "Wolfgang Naraschewski and Tobias Nipkow",
  title = 	 "Type Inference Verified: Algorithm {W} in {Isabelle/HOL}",
  note = 	 "Submitted",
  year =	 1997,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html"
}

@InProceedings{Nazareth96,
  author = 	 "Dieter Nazareth and Tobias Nipkow",
  title = 	 "Formal Verification of Algorithm {W}: The Monomorphic Case",
  editor =	 "J. Wright and J. Grundy and J. Harrison",
  booktitle =	 "Proceedings of the 9th International Conference on
                  Theorem Proving in Higher Order Logics (TPHOL'96)",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1125",
  address =	 "Turku, Finland",
  month =	 aug,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html"
}
		  
@InProceedings{Necula96osdi,
  author = 	 "George C. Necula and Peter Lee",
  title = 	 "Safe Kernel Extensions Without Run-Time Checking",
  booktitle =	 "Proceedings of the Second Symposium on Operating
		  System Design and Implementation (OSDI'96)",
  year =	 1996,
  address =	 "Seattle, Washington",
  month =	 oct,
  pages =	 "229--243"
}

@InProceedings{Necula97popl,
  author = 	 "George C. Necula",
  title = 	 "Proof-Carrying Code",
  booktitle =	 "Conference Record of the 24th Symposium on Principles
		  of Programming Languages (POPL'97)",
  year =	 1997,
  publisher =	 "ACM Press",
  address =	 "Paris, France",
  month =	 jan,
  editor =       "Neil D. Jones",
  pages =	 "106--119"
}

@InProceedings{Necula98lics,
  author = 	 "George C. Necula and Peter Lee",
  title = 	 "Efficient Representation and Validation of Logical Proofs",
  booktitle =	 "Proceedings of the 13th Annual Symposium on Logic in
		  Computer Science (LICS'98)",
  pages =	 "93--104",
  year =	 1998,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Indianapolis, Indiana",
  month =	 jun
}

@PhdThesis{Necula98phd,
  author = 	 "George C. Necula",
  title = 	 "Compiling with Proofs",
  school = 	 "Carnegie Mellon University",
  year = 	 1998,
  month =	 oct,
  note =         "Available as Technical Report CMU-CS-98-154"
}

@InProceedings{Necula98pldi,
  author = 	 "George C. Necula and Peter Lee",
  title = 	 "The Design and Implementation of a Certifying Compiler",
  editor =	 "Keith D. Cooper",
  pages =	 "333--344",
  booktitle =	 "Proceedings of the Conference on
		  Programming Language Design and Implementation (PLDI'98)",
  year =	 1998,
  publisher =	 "ACM Press",
  address =	 "Montreal, Canada",
  month =	 jun
}

@PhdThesis{Nederpelt73,
  author =	"R.P. Nederpelt",
  title =	"Strong Normalization in a Typed Lambda Calculus with Lambda
		  Structured Types",
  school =	"Eindhoven University of Technology",
  year =	1973,
  keywords = 	"Automath"
}

@Book{Nederpelt94,
  title = 	 "Selected Papers on {Automath}",
  publisher = 	 "North-Holland",
  year = 	 1994,
  editor =	 "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer",
  volume =	 133,
  series =	 "Studies in Logic and the Foundations of Mathematics",
  keywords =	 "Automath"
}

@Article{Nipkow89fac,
  author =	"Tobias Nipkow",
  title =	"Term Rewriting and Beyond --- Theorem Proving in {Isabelle}",
  journal =	"Formal Aspects of Computing",
  year =	1989,
  volume =	1,
  pages =	"320--338",
  urlhtml =     "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fac89.html",
  keywords = 	"Isabelle, rewriting"
}

@Article{Nipkow89scp,
  author =	"Tobias Nipkow",
  title =	"Equational Reasoning in {Isabelle}",
  journal =	"Science of Computer Programming",
  year =	1989,
  volume =	12,
  pages =	"123--149",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/~nipkow/pubs/scp89.html",
  keywords = 	"Isabelle"
}

@InProceedings{Nipkow90ctrs,
  author =	"Tobias Nipkow",
  title	=	"Higher-Order Unification, Polymorphism, and Subsorts",
  booktitle =	"Proceedings of the 2nd International Workshop on Conditional
		  and Typed Rewriting Systems",
  address =	"Montreal, Canada",
  month =	jun,
  editor =	"S. Kaplan and M. Okada",
  publisher =	"Springer-Verlag LNCS 516",
  pages =	"436--447",
  year =	"1990",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ctrs90.html",
  keywords =	"Isabelle, unification"
}

@InProceedings{Nipkow90srds,
  author =	"Tobias Nipkow",
  title =	"Formal Verification of Data Type Refinement ---
		  Theory and Practice",
  booktitle =	"Stepwise Refinement of Distributed Systems",
  editor =	"J.W. de Bakker and W.-P. de Roever and G. Rozenberg",
  year =	1990,
  publisher =	"Springer-Verlag LNCS 430",
  pages =	"561--591",
  urlhtml =	"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/rex.html",
  keywords = 	"Isabelle"
}

@Article{Nipkow91cj,
  author =	"Tobias Nipkow",
  title =	"Constructive Rewriting",
  journal =	"Computer Journal",
  year =	1991,
  volume =	34,
  pages =	"34--41",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cj91.html",
  keywords = 	"Isabelle, rewriting"
}

@InProceedings{Nipkow91lics,
  author =	"Tobias Nipkow",
  title =	"Higher-Order Critical Pairs",
  booktitle =	"Sixth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Amsterdam, The Netherlands",
  editor =	"G. Kahn",
  month =	jul,
  year =	"1991",
  pages =	"342--349",
  urlhtml =	"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics91.html",
  keywords = 	"rewriting"
}

@InProceedings{Nipkow92,
  author =	"Tobias Nipkow and Lawrence C. Paulson",
  title =	"{Isabelle}-91",
  editor =	"D. Kapur",
  booktitle =	"Proceedings of the 11th International Conference on Automated
		  Deduction",
  address =	"Saratoga Springs, NY",
  publisher =	"Springer-Verlag LNAI 607",
  pages =	"673--676",
  year =	1992,
  note =	"System abstract",
  urldvi =	"http://www.cl.cam.ac.uk/users/lcp/papers/CADE11.dvi.gz",
  keywords = 	"Isabelle"
}

@InProceedings{Nipkow93le,
  author =	"Tobias Nipkow",
  title =	"Order-Sorted Polymorphism in {Isabelle}",
  booktitle =	"Logical Environments",
  year =	1993,
  editor =	"G. Huet and G. Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"164--188",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lf91.html",
  keywords = 	"Isabelle"
}

@InProceedings{Nipkow93lics,
  title =	"Functional Unification of Higher-Order Patterns",
  author =	"Tobias Nipkow",
  pages =	"64--74",
  booktitle =	"Eighth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Montreal, Canada",
  editor =	"M. Vardi",
  month =	jun,
  year =	"1993",
  urlhtml =	"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html",
  keywords = 	"unification"
}

@InProceedings{Nipkow93tlca,
  author =	"Tobias Nipkow",
  title =	"Orthogonal Higher-Order Rewrite Systems are Confluent",
  booktitle =	"Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications",
  editor =	"M. Bezem and J.F. Groote",
  address =	"Utrecht, The Netherlands",
  month =	may,
  year =	"1993",
  pages =	"306--317",
  urlhtml =	"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tlca93.html",
  keywords =	"rewriting"
}

@InProceedings{Nipkow94,
  author = 	 "Tobias Nipkow and Konrad Slind",
  title = 	 "{I/O} Automata in {Isabelle/HOL}",
  editor = 	 "P. Dybjer and B. Nordstr{\"o}m and J. Smith",
  pages =	 "101--119",
  booktitle =	 "Proceedings of the International Workshop on Types for
		  Proofs and Programs",
  year =	 1994,
  publisher =	 "Springer-Verlag LNCS 996",
  address =	 "B{\aa}stad, Sweden",
  month =	 jun,
  keywords =	 "Isabelle",
  urlhtml =      "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html"
}

@InProceedings{Nipkow96cade,
  author = 	 "Tobias Nipkow",
  title = 	 "More {Church-Rosser} Proofs (in {Isabelle/HOL})",
  editor =	 "M.A. McRobbie and J.K. Slaney",
  pages =	 "733--747",
  booktitle =	 "Proceedings of the 13th International Conference on
		  Automated Deduction (CADE-13)",
  year =	 1996,
  publisher =	 "Springer-Verlag LNAI 1104",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "Isabelle",
  urlhtml =      "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.html"
}

@InProceedings{Nipkow96fsttcs,
  author = 	 "Tobias Nipkow",
  title = 	 "{Winskel} is (Almost) Right: Towards a Mechanized
                  Semantics Textbook",
  editor =	 "V. Chandru and V. Vinay",
  pages =	 "180--192",
  booktitle =	 "Proceedings of the Conference on Foundations of
                  Software Technology and Theoretical Computer Science",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1180",
  keywords =	 "Isabelle",
  urlhtml =      "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fsttcs96.html"
}

@InProceedings{Nipkow98popl,
  author = 	 "Tobias Nipkow and David von Oheimb",
  title = 	 "Java-light is Type-Safe --- Definitely",
  editor =	 "L. Cardelli",
  pages =	 "161--170",
  booktitle =	 "Conference Record of the 25th Symposium on Principles of
		  Programming Languages (POPL'98)",
  year =	 1998,
  publisher =	 "ACM Press",
  address =	 "San Diego, California",
  month =	 jan,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/bali.html"
}

@Article{Nipkow98fac,
  author = 	 "Tobias Nipkow",
  title = 	 "Winskel is (almost) Right: Towards a Mechanized Semantics
		  Textbook",
  journal =	 "Formal Aspects of Computing",
  year =         1998,
  volume =	 10,
  pages =	 "171--186",
  keywords =	 "Isabelle"
}

@InProceedings{Nipkow98tphols,
  author = 	 "Tobias Nipkow",
  title = 	 "Verified Lexical Analysis",
  editor =	 "J. Grundy and M. Newey",
  pages =	 "1--15",
  booktitle =	 "Proceedings of the 11th International Conference on Theorem
		  Proving in Higher Order Logics (TPHOLs'98)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1479",
  address =	 "Canberra, Australia",
  month =	 sep,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html"
}

@InProceedings{Nipkow99fase,
  author = 	 "Tobias Nipkow and Leonor Prensa Nieto",
  title = 	 "Owicki/{G}gries in {Isabelle/HOL}",
  editor =	 "J.-P. Finance",
  pages =	 "188--203",
  booktitle =	 "Proceedings of the Second International Conference on
		  Fundamental Approaches to Software Engineering (FASE'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1577",
  address =	 "Amsterdam, The Netherlands",
  month =	 mar,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/fase99.html"
}

@InProceedings{Nipkow99cade,
  author = 	 "Tobias Nipkow",
  title = 	 "Embedding Programming Language in Theorem Provers",
  editor =	 "Harald Ganzinger",
  pages =	 "398--399",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNAI 1632",
  address =	 "Trento, Italy",
  month =	 jul,
  note =	 "Abstract for Invited Talk",
  keywords =	 "Isabelle"
}

@TechReport{Noel91,
  author =	"Philippe No{\"e}l",
  title =	"A Set Theoretic Semantics for a first order Temporal Logic:
		  Definition and Application using {Isabelle}",
  number =	"UMCS-91-12-4",
  institution =	"Department of Computer Science, University of Manchester",
  year =	1991,
  keywords = 	"Isabelle"
}

@Article{Noel93,
  author =	"Philippe No{\"e}l",
  title =	"Experimenting with {Isabelle} in {ZF} Set Theory",
  journal =	"Journal of Automated Reasoning",
  volume =	10,
  number =	1,
  pages =	"15--58",
  year =	1993,
  keywords = 	"Isabelle"
}

@InProceedings{Nordstrom93,
  author =	"Bengt Nordstr{\"o}m",
  title =	"The {ALF} proof editor",
  booktitle =	"Proceedings of the Workshop on Types for Proofs and Programs",
  address =	"Nijmegen",
  year =	"1993",
  pages =	"253--266",
  keywords = 	"ALF"
}

@InProceedings{Oheimb97,
  author = 	 "David von Oheimb and Thomas F. Gritzner",
  title = 	 "{RALL}: Machine-Supported Proofs for Relational Algebra",
  editor =	 "W. McCune",
  pages =	 "380--394",
  booktitle =	 "Proceedings of the 14th International Conference on
		  Automated Deduction",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1249",
  address =	 "Townsville, Australia",
  month =	 jul,
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/papers/CADE-14_oheimb_1997_Conference.html"
}

@InCollection{Oheimb99,
  author = 	 "David von Oheimb and Tobias Nipkow",
  title = 	 "Machine-Checking the {Java} Specification: Proving
		  Type-Safety",
  booktitle =	 "Formal Syntax and Semantics of {Java}",
  publisher =	 "Springer-Verlag LNCS 1523",
  year =	 1999,
  editor =	 "J. Alves-Foss",
  pages =	 "119--156",
  keywords =	 "Isabelle",
  urlhtml =	 "http://www4.informatik.tu-muenchen.de/~isabelle/bali/doc/Springer98.html"
}

@InProceedings{Oostrom96,
  author = 	 "Vincent van Oostrom",
  title = 	 "Higher-Order Families",
  editor =	 "Harald Ganzinger",
  pages =	 "392--407",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "rewriting"
}

@InProceedings{Pareschi90,
  title =	"Extending Definite Clause Grammars with Scoping Constructs",
  author =	"Remo Pareschi and Dale Miller",
  year =	1990,
  booktitle =	"Proceedings of Seventh International Conference on Logic
		  Programming",
  address =	"Jerusalem, Israel",
  month =	jun,
  pages =	"373-389",
  publisher =	"MIT Press",
  editor =	"David H. D. Warren and Peter Szeredi",
  urldvi =	"file://ftp.cis.upenn.edu/pub/papers/miller/iclp90pareschi.dvi.Z",
  keywords =	"lambda-Prolog"
}

@Article{Paulson86,
  author =	"Lawrence C. Paulson",
  title =	"Natural Deduction as Higher-order Resolution",
  journal =	"Journal of Logic Programming",
  volume =	3,
  pages =	"237--258",
  year =	1986,
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR082-lcp-higher-order-resolution.dvi.gz",
  keywords =	"Isabelle"
}

@InProceedings{Paulson88cade,
  author =	"Lawrence C. Paulson",
  title =	"Isabelle: The Next Seven Hundred Theorem Provers",
  editor =	"E. Lusk and R. Overbeek",
  booktitle =	"Proceedings of the 9th International Conference on
		  Automated Deduction",
  address =	"Argonne, Illinois",
  publisher =	"Springer Verlag LNCS 310",
  year =	1988,
  pages =	"772--773",
  note =	"System abstract",
  urldvi =	"http://www.cl.cam.ac.uk/users/lcp/papers/CADE9.dvi.gz",
  keywords = 	"Isabelle"
}

@InProceedings{Paulson88colog,
  author =	"Lawrence C. Paulson",
  title =	"A Formulation of the Simple Theory of Types (for
		 {Isabelle})",
  year =	1988,
  editor =	"P. Martin-L{\"o}f and G. Mints",
  booktitle =	"Proceedings of the International Conference on Computer Logic
		  {COLOG'88}",
  address =	"Tallinn, Estonia",
  month =	dec,
  pages =	"246--274",
  publisher =	"Springer-Verlag LNCS 417",
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz",
  keywords = 	"Isabelle"
}

@Article{Paulson89,
  author =	"Lawrence C. Paulson",
  title =	"The Foundation of a Generic Theorem Prover",
  journal =	"Journal of Automated Reasoning",
  volume =	5,
  number =	3,
  pages =	"363--397",
  year =	1989,
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz",
  keywords = 	"Isabelle"
}

@InCollection{Paulson90lacs,
  author =	"Lawrence C. Paulson",
  title =	"{Isabelle}: The Next 700 Theorem Provers",
  booktitle =	"Logic and Computer Science",
  editor =	"P. Odifreddi",
  publisher =	"Academic Press",
  year =	1990,
  pages =	"361--386",
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz",
  keywords = 	"Isabelle"
}

@TechReport{Paulson90tr,
  author =	"Lawrence C. Paulson and Tobias Nipkow",
  title =	"{Isabelle} Tutorial and User's Manual",
  institution =	"University of Cambridge, Computer Laboratory",
  year =	1990,
  number =	189,
  month =	jan,
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR189-lcp-second-isabelle-manual.dvi.gz",
  keywords = 	"Isabelle"
}

@InCollection{Paulson92,
  author = 	"Lawrence C. Paulson",
  title = 	"Designing a Theorem Prover",
  booktitle =	"Handbook of Logic in Computer Science",
  publisher =	"Oxford University Press",
  year =	1992,
  editor =	"S. Abramsky and D. M. Gabbay and T. S. E. Maibaum",
  volume =	2,
  pages =	"415--475",
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR192-lcp-designing.dvi.gz",
  keywords =	"Isabelle"
}

@Article{Paulson93jar,
  author =	"Lawrence C. Paulson",
  title =	"Set Theory for Verification: {I}.  {From} Foundations to
		  Functions",
  journal =	"Journal of Automated Reasoning",
  volume =	11,
  number =	3,
  pages =	"353--389",
  year =	1993,
  urlps =	"ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz",
  keywords = 	"Isabelle"
}

@TechReport{Paulson93tra,
  author =	"Lawrence C. Paulson",
  title =	"Introduction to {Isabelle}",
  number =	280,
  institution =	"University of Cambridge, Computer Laboratory",
  year =	1993,
  urldvi =	"ftp://ftp.cl.cam.ac.uk/ml/intro.dvi.gz",
  keywords = 	"Isabelle"
}

@TechReport{Paulson93trb,
  author =	"Lawrence C. Paulson",
  title =	"{Isabelle}'s Object-Logics",
  number =	286,
  institution =	"University of Cambridge, Computer Laboratory",
  year =	1993,
  urldvi =	"ftp://ftp.cl.cam.ac.uk/ml/logics.dvi.gz",
  keywords = 	"Isabelle"
}

@TechReport{Paulson93trc,
  author =	"Lawrence C. Paulson",
  title =	"The {Isabelle} Reference Manual",
  number =	283,
  institution =	"University of Cambridge, Computer Laboratory",
  year =	1993,
  urldvi =	"ftp://ftp.cl.cam.ac.uk/ml/ref.dvi.gz",
  keywords = 	"Isabelle"
}

@TechReport{Paulson93tre,
  author =	"Lawrence C. Paulson",
  title =	"Co-induction and Co-recursion in Higher-Order Logic",
  institution =	"University of Cambridge, Computer Laboratory",
  year =	1993,
  number =	304,
  month =	jul,
  urlps =	"http://www.cl.cam.ac.uk/Research/Reports/TR304-lcp-coinduction.ps.gz",
  keywords =    "Isabelle"
}

@Book{Paulson94book,
  author =	"Lawrence C. Paulson",
  title =	"Isabelle: A Generic Theorem Prover",
  publisher =	"Springer-Verlag LNCS 828",
  year =	1994,
  keywords = 	"Isabelle"
}

@InProceedings{Paulson94cade,
  author =	"Lawrence C. Paulson",
  title =	"A Fixedpoint Approach to Implementing (Co)Inductive
		  Definitions",
  editor =	"Alan Bundy",
  booktitle =	"Proceedings of the 12th International Conference on Automated
		  Deduction",
  address =	"Nancy, France",
  month =	jun,
  year =	1994,
  publisher =	"Springer-Verlag LNAI 814",
  pages =	"148--161",
  urldvi =	"http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz",
  keywords = 	"Isabelle"
}

@Proceedings{Paulson95isabelle,
  title = 	 "Proceedings of the First {Isabelle} Users Workshop",
  year = 	 1995,
  editor =	 "Lawrence C. Paulson",
  note =	 "Available as University of Cambridge, Computer Laboratory,
                  Technical Report 379",
  keywords =     "Isabelle",
  url =		 "http://www.cl.cam.ac.uk/users/lcp/Workshop/index.html"
}

@Article{Paulson95jar,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Set Theory for Verification: {II}.  {Induction} and
                  Recursion",
  journal =	 "Journal of Automated Reasoning",
  year =	 1995,
  volume =	 15,
  number =	 2,
  pages =	 "167--215",
  keywords =     "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz"
}

@TechReport{Paulson95tr,
  author = 	 "Lawrence C. Paulson and Krzysztof Gr{\c{a}}bczewski",
  title = 	 "Mechanising Set Theory: Cardinal Arithmetic and the Axiom of
		  Choice",
  institution =  "University of Cambridge, Computer Laboratory",
  year = 	 1995,
  number =	 377,
  month =	 aug,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz"
}

@InCollection{Paulson96chap,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Generic Automatic Proof Tools",
  booktitle =	 "Automated Reasoning and Its Applications",
  publisher =	 "MIT Press",
  year =	 1997,
  editor =	 "Robert Veroff",
  chapter =	 3,
  note =	 "In press",
  keywords =	 "Isabelle"
}

@InCollection{Paulson96markt,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Tool Support for Logics of Programs",
  booktitle =	 "Mathematical Methods in Program Development",
  publisher =	 "Springer-Verlag",
  year =	 1996,
  editor =	 "Manfred Broy",
  series =	 "NATO ASI Series F",
  note =	 "Summer School Marktoberdorf.  In press",
  keywords =	 "Isabelle"
}

@TechReport{Paulson96tr,
  author = 	 "Lawrence C. Paulson",
  title = 	 "A Simple Formatization and Proof for the Mutilated
                  Chess Board",
  institution =  "University of Cambridge, Computer Laboratory",
  year = 	 1996,
  number =	 394,
  month =	 may,
  keywords =	 "Isabelle",
  urldvi =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz"
}

@Article{Paulson97jlc,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Mechanizing Coinduction and Corecursion in
                  Higher-Order Logic",
  journal =	 "Journal of Logic and Computation",
  year =	 1997,
  volume =	 7,
  number =	 2,
  pages =	 "175--204",
  month =	 mar,
  keywords =	 "Isabelle"
}

@TechReport{Paulson97tr,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Mechanized Proofs of Security Protocols:
                  {Needham-Schroeder} with Public Keys",
  institution =  "University of Cambridge, Computer Laboratory",
  year = 	 1997,
  number =	 413,
  month =	 jan,
  keywords =	 "Isabelle"
}

@InProceedings{Paulson97csfwa,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Proving Properties of Security Protocols by Induction",
  pages =	 "70--83",
  booktitle =	 "Proceedings of the 10th Computer Security Foundations Workshop",
  year =	 1997,
  publisher =	 "IEEE Computer Society Press",
  month =	 jun,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz"
}

@InProceedings{Paulson97csfwb,
  author = 	 "Lawrence C. Paulson",
  title = 	 "Mechanized Proofs for a Recursive Authentication Protocol",
  pages =	 "84--95",
  booktitle =	 "Proceedings of the 10th Computer Security Foundations Workshop",
  year =	 1997,
  publisher =	 "IEEE Computer Society Press",
  month =	 jun,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz"
}

@Article{Paulson98jcs,
  author = 	 "Lawrence C. Paulson",
  title = 	 "The Inductive Approach to Verifying Cryptographic Protocols",
  journal =	 "Journal of Computer Security",
  year =	 1998,
  volume =	 6,
  pages =	 "85--128",
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR443-lcp-Inductive-Approach-to-Verifying-Cryptographic-Protocols.ps.gz"
}

@InProceedings{Paulson98ids,
  author = 	 "Lawrence C. Paulson",
  title = 	 "A Generic Tableau Prover and Its Integration with {Isabelle}",
  pages =	 "51--60",
  booktitle =	 "Proceedings of the CADE-15 Workshop on Integration of
		  Deduction Systems",
  year =	 1998,
  month =	 jul,
  note =	 "Available as Technical Report 441, Computer Laboratory,
		  University of Cambridge",
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR441-lcp-Generic-Tableau-Prover.ps.gz"
}

@MastersThesis{Peratto91,
  author = 	 "Patricia Peratto",
  title = 	 "Course-of-Values Recursion  in {Martin-L{\"o}f's} Type
		  Theory",
  school = 	 "Instituto de Computaci{\'o}n, Facultad de Ingenieria,
		  Universidad de la Republica Oriental del Uruguay",
  year = 	 1991,
  address =	 "Montevideo, Uruguay",
  keywords =	 "misc"
}

@TechReport{Peratto95tra,
  author = 	 "Patricia Peratto",
  title = 	 "Course-of-Values Recursion on Lists and a Definition for
		  Quicksort",
  institution =  "Instituto de Computaci{\'o}n, Facultad de Ingenieria,
		  Universidad de la Republica Oriental del Uruguay",
  year = 	 1995,
  address =	 "Montevideo, Uruguay",
  keywords =     "misc"  
}
		  
@TechReport{Peratto95trb,
  author = 	 "Patricia Peratto",
  title = 	 "An {Alf} Implementation of Insertion Sort",
  institution =  "Instituto de Computaci{\'o}n, Facultad de Ingenieria,
		  Universidad de la Republica Oriental del Uruguay",
  year = 	 1995,
  address =	 "Montevideo, Uruguay",
  keywords =     "ALF"
}

@InProceedings{Pfenning88lfp,
  author =	"Frank Pfenning",
  title =	"Partial Polymorphic Type Inference and Higher-Order
		  Unification",
  booktitle =	"Proceedings of the 1988 {ACM} Conference on {Lisp} and
		  Functional Programming",
  publisher =	"ACM Press",
  month =	jul,
  year =	"1988",
  pages =	"153--163",
  address =	"Snowbird, Utah",
  keywords = 	"lambda-Prolog, unification"
}

@InProceedings{Pfenning88pldi,
  author =	"Frank Pfenning and Conal Elliott",
  title =	"Higher-Order Abstract Syntax",
  booktitle =	"Proceedings of the {ACM SIGPLAN '88} Symposium on Language
		  Design and Implementation",
  address =	"Atlanta, Georgia",
  month =	jun,
  year =	"1988",
  pages =	"199--208",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/pldi88.ps.gz",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Pfenning89lics,
  author =	"Frank Pfenning",
  title =	"{Elf}: A Language for Logic Definition and Verified
		  Meta-Programming",
  booktitle =	"Fourth Annual Symposium on Logic in Computer Science",
  address =	"Pacific Grove, California",
  publisher =	"IEEE Computer Society Press",
  month =	jun,
  year =	"1989",
  pages =	"313--322",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/lics89.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/lics89.ps.gz",
  keywords = 	"LF, Elf"
}

@InProceedings{Pfenning91lf,
  author =	"Frank Pfenning",
  title =	"Logic Programming in the {LF} Logical Framework",
  booktitle =	"Logical Frameworks",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  publisher =	"Cambridge University Press",
  pages =	"149--181",
  year =	"1991",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/lfproc91.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/lfproc91.ps.gz",
  keywords = 	"LF, Elf"
}

@InProceedings{Pfenning91lics,
  author =	"Frank Pfenning",
  title =	"Unification and Anti-Unification in the {Calculus} of
		  {Constructions}",
  booktitle =	"Sixth Annual {IEEE} Symposium on Logic in Computer Science",
  address =	"Amsterdam, The Netherlands",
  month =	jul,
  year =	"1991",
  pages =	"74--85",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/lics91.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/lics91.ps.gz",
  keywords = 	"LF, Elf, unification"
}

@InProceedings{Pfenning92cade,
  author =	"Frank Pfenning and Ekkehard Rohwedder",
  title =	"Implementing the Meta-Theory of Deductive Systems",
  booktitle =	"Proceedings of the 11th International Conference on Automated
		  Deduction",
  address =	"Saratoga Springs, New York",
  editor =	"D. Kapur",
  publisher =	"Springer-Verlag LNAI 607",
  month =	jun,
  year =	"1992",
  pages =	"537--551",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/cade92.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/cade92.ps.gz",
  keywords = 	"LF, Elf"
}

@InCollection{Pfenning92tilp,
  author =	"Frank Pfenning",
  title =	"Dependent Types in Logic Programming",
  booktitle =	"Types in Logic Programming",
  editor =	"Frank Pfenning",
  publisher =	"MIT Press",
  address =	"Cambridge, Massachusetts",
  chapter =	"10",
  pages =	"285--311",
  year =	"1992",
  keywords = 	"LF, Elf"
}

@Article{Pfenning93jar,
  author =	"Frank Pfenning",
  title =	"A Proof of the {Church-Rosser} Theorem and its Representation
		  in a Logical Framework",
  journal =	"Journal of Automated Reasoning",
  year =	"1993",
  note =	"To appear.  A preliminary version is available as
		  Carnegie Mellon Technical Report CMU-CS-92-186, September
		  1992",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/cr92.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/cr92.ps.gz",
  keywords = 	"LF, Elf"
}

@InProceedings{Pfenning93types,
  author =	"Frank Pfenning",
  title =	"Refinement Types for Logical Frameworks",
  booktitle =	"Informal Proceedings of the Workshop on Types for Proofs
		  and Programs",
  editor =	"Herman Geuvers",
  address =	"Nijmegen, The Netherlands",
  month =	may,
  year =	"1993",
  pages =	"285--299",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/rlf93.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/rlf93.ps.gz",
  keywords = 	"LF, Elf, lambda-Prolog"
}

@InProceedings{Pfenning94cade,
  author =	"Frank Pfenning",
  title =	"Elf: A Meta-Language for Deductive Systems",
  booktitle =	"Proceedings of the 12th International Conference on Automated
		  Deduction",
  editor =	"A. Bundy",
  publisher =	"Springer-Verlag LNAI 814",
  address =	"Nancy, France",
  month =	jun,
  year =	"1994",
  pages =	"811--815",
  note =	"System abstract",
  urldvi =	"http://www.cs.cmu.edu/~fp/papers/cade94.dvi.gz",
  urlps =	"http://www.cs.cmu.edu/~fp/papers/cade94.ps.gz",
  keywords = 	"LF, Elf"
}

@TechReport{Pfenning94tra,
  author = 	 "Frank Pfenning",
  title = 	 "A Structural Proof of Cut Elimination and Its Representation
		  in a Logical Framework",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1994,
  number =	 "CMU-CS-94-218",
  month =	 nov,
  keywords =	 "LF, Elf",
  urldvi =	 "http://www.cs.cmu.edu/~fp/papers/cutelim94.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/cutelim94.ps.gz"
}

@TechReport{Pfenning94trb,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination in Linear Logic",
  institution =  "Department of Computer Science, Carnegie Mellon University",
  year = 	 1994,
  number =	 "CMU-CS-94-222",
  month =	 dec,
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/cutlin94.ps.gz",
  keywords =	 "LF, Elf, linear"
}

@Unpublished{Pfenning94un,
  author =	"Frank Pfenning",
  title =	"Computation and Deduction",
  note =	"Unpublished lecture notes, 277 pp.
		 Revised May 1994, April 1996",
  year =	1992,
  month =	may,
  keywords = 	"LF, Elf"
}
		  
@InProceedings{Pfenning95lics,
  author = 	 "Frank Pfenning",
  title = 	 "Structural Cut Elimination",
  editor =	 "D. Kozen",
  booktitle =	 "Proceedings of the Tenth Annual Symposium on Logic in
		  Computer Science",
  year =	 1995,
  publisher =	 "IEEE Computer Society Press",
  address =	 "San Diego, California",
  month =	 "June",
  pages =	 "156--166",
  keywords =     "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/lics95.ps.gz"
}

@InProceedings{Pfenning95mfps,
  author = 	 "Frank Pfenning and Hao-Chi Wong",
  title = 	 "On a Modal $\lambda$-Calculus for {S4}",
  booktitle =	 "Proceedings of the Eleventh Conference on 
                  Mathematical Foundations of Programming Semantics",
  editor =       "S. Brookes and M. Main",
  year =	 1995,
  address =	 "New Orleans, Louisiana",
  month =	 mar,
  note =	 "{\em Electronic Notes in Theoretical Computer
		  Science}, Volume 1, Elsevier", 
  keywords =     "misc",
  urldvi =       "http://www.cs.cmu.edu/~fp/papers/mfps95.dvi.gz",
  urlps =        "http://www.cs.cmu.edu/~fp/papers/mfps95.ps.gz"
}

@InProceedings{Pfenning96caap,
  author = 	 "Frank Pfenning",
  title = 	 "The Practice of Logical Frameworks",
  booktitle = 	 "Proceedings of the Colloquium on Trees in Algebra and
		  Programming",
  editor =	 "H{\'e}l{\`e}ne Kirchner",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1059",
  address = 	 "Link{\"o}ping, Sweden",
  month =	 apr,
  pages =	 "119--134",
  note =	 "Invited talk",
  keywords =	 "ALF, Automath, Elf, FS0, Isabelle, lambda-Prolog,
		  LF, linear, misc, Pi, rewriting, unification",
  urldvi =	 "http://www.cs.cmu.edu/~fp/papers/caap96.dvi.gz",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/caap96.ps.gz"
}
		  
@Book{Pfenning00book,
  author = 	 "Frank Pfenning",
  title = 	 "Computation and Deduction",
  publisher = 	 "Cambridge University Press",
  year = 	 2000,
  note =	 "In preparation.  Draft from April 1997 available
		  electronically",
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~twelf/notes/cd.ps"
}

@InProceedings{Pfenning98cade,
  author = 	 "Frank Pfenning",
  title = 	 "Reasoning About Deductions in Linear Logic",
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =	 "1--2",
  booktitle =	 "Proceedings of the 15th International Conference on
		  Automated Deduction (CADE-15)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1421",
  address =	 "Lindau, Germany",
  month =	 jul,
  note =         "Abstract for invited talk",
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/cade98inv.ps.gz"
}
		  
@Manual{Pfenning98guide,
  title = 	 "Twelf User's Guide",
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  edition =	 "1.2",
  year =	 1998,
  month =	 sep,
  keywords =	 "LF, Elf",
  note =	 "Available as Technical Report CMU-CS-98-173, Carnegie
		  Mellon University",
  urlhtml =	 "http://www.cs.cmu.edu/~twelf/guide"
}
		  
@InProceedings{Pfenning98pstt,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "Algorithms for Equality and Unification in the
		  Presence of Notational Definitions",
  editor =	 "D. Galmiche",
  booktitle =	 "Proceedings of the CADE Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1998,
  publisher =	 "Electronic Notes in Theoretical Computer Science",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/strict98.ps.gz"
}

@InProceedings{Pfenning98types,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "Algorithms for Equality and Unification in the
		  Presence of Notational Definitions",
  editor =	 "T. Altenkirch and W. Naraschewski and B. Reus",
  booktitle =	 "Types for Proofs and Programs",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1657",
  note =	 "To appear",
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/types98.ps.gz"
}
		  
@InCollection{Pfenning99handbook,
  author = 	 "Frank Pfenning",
  title = 	 "Logical Frameworks",
  booktitle =	 "Handbook of Automated Reasoning",
  publisher =	 "Elsevier Science Publishers",
  year =	 1999,
  editor =	 "Alan Robinson and Andrei Voronkov",
  note =	 "In preparation",
  keywords =	 "LF, Elf, misc"
}

@InProceedings{Pfenning99cade,
  author = 	 "Frank Pfenning and Carsten Sch{\"u}rmann",
  title = 	 "System Description: Twelf --- A Meta-Logical Framework for
		  Deductive Systems",
  editor =	 "H. Ganzinger",
  pages =        "202--206",
  booktitle =	 "Proceedings of the 16th International Conference on
		  Automated Deduction (CADE-16)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNAI 1632",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/twelf98.ps.gz"
}

@InProceedings{Plesko99,
  author = 	 "Mark Plesko and Frank Pfenning",
  title = 	 "A Formalization of the Proof-Carrying Code Architecture in a
		  Linear Logical Framework",
  editor =	 "A. Pnueli and P. Traverso",
  booktitle =	 "Proceedings of the FLoC Workshop on Run-Time Result
		  Verification",
  year =	 1999,
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/pccllf99.ps.gz"
}

@InProceedings{Polakow99tlca,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Natural Deduction for Intuitionistic Non-Commutative
		  Linear Logic",
  editor =	 "J.-Y. Girard",
  booktitle =	 "Proceedings of the 4th International Conference on
		  Typed Lambda Calculi and Applications (TLCA'99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1581",
  address =	 "L'Aquila, Italy",
  month =	 apr,
  pages =        "295--309",
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/tlca99.ps.gz"
}

@InProceedings{Polakow99mfps,
  author = 	 "Jeff Polakow and Frank Pfenning",
  title = 	 "Relating Natural Deduction and Sequent Calculus for
		  Intuitionistic Non-Commutative Linear Logic",
  editor =	 "Andre Scedrov and Achim Jung",
  booktitle =	 "Proceedings of the 15th Conference on Mathematical
		  Foundations of Programming Semantics",
  year =	 1999,
  address =	 "New Orleans, Louisiana",
  month =	 apr,
  note =	 "Electronic Notes in Theoretical Computer Science, Volume 20",
  keywords =	 "LF, Elf, linear",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/mfps99.ps.gz"
}

@InProceedings{Pollack93types,
  author = 	 "Robert Pollack",
  title = 	 "Closure Under Alpha-Conversion",
  editor =	 "Henk Barendregt and Tobias Nipkow",
  pages =	 "313--332",
  booktitle =	 "Proceedings of the Workshop on Types for Proofs and Programs",
  year =	 1993,
  publisher =	 "Springer-Verlag LNCS 806",
  address =	 "Nijmegen, The Netherlands",
  month =	 may,
  keywords =	 "misc"
}

@PhdThesis{Pollack94phd,
  author = 	"Robert Pollack",
  title = 	"The Theory of {LEGO}: {A} Proof Checker for the Extended
		 Calculus of Constructions",
  school = 	"University of Edinburgh",
  year = 	"1994",
  keywords =	"misc",
  urlps =	"ftp://ftp.cs.chalmers.se/pub/users/pollack/thesis.ps.Z"
}

@InProceedings{Pollack94types,
  author = 	 "Robert Pollak",
  title = 	 "On Extensibility of Proof Checkers",
  editor = 	 "P. Dybjer and B. Nordstr{\"o}m and J. Smith",
  pages =	 "140--161",
  booktitle =	 "Proceedings of the International Workshop on Types for
		  Proofs and Programs",
  year =	 1994,
  publisher =	 "Springer-Verlag LNCS 996",
  address =	 "B{\aa}stad, Sweden",
  month =	 jun,
  keywords =	 "misc"
}

@InProceedings{Pollack95tlca,
  author = 	 "Robert Pollack",
  title = 	 "A Verified Typechecker",
  editor =	 "M. Dezani-Ciancaglini and G. Plotkin",
  booktitle =	 "Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 902",
  address =	 "Edinburgh, Scotland",
  month =	 apr,
  pages =	 "365--380",
  keywords =     "misc"
}

@Unpublished{Pollack95un,
  author = 	 "Robert Pollack",
  title = 	 "Polishing Up the {Tait-Martin-L{\"o}f} Proof of the
		  {Church-Rosser} Theorem",
  note = 	 "Unpublished note",
  year =	 1995,
  month =	 jan,
  keywords =	 "misc",
  urlps =	 "ftp://ftp.cs.chalmers.se/pub/users/pollack/churchrosser.dvi.gz"
}

@InCollection{Pollack98,
  author = 	 "Robert Pollack",
  title = 	 "How to Believe a Machine-Checked Proof",
  booktitle =	 "Twenty-Five Years of Constructive Type Theory",
  publisher =	 "Oxford University Press",
  year =	 1998,
  editor =	 "G. Sambin and J. Smith",
  month =	 aug,
  note =	 "Proceedings of a Congress held in Venice, Italy, October
		  1995",
  keywords =	 "misc",
  urlps =	 "http://www.brics.dk/~pollack/export/believing.ps.gz"
}

@InProceedings{Prehofer94cade,
  author =	"Christian Prehofer",
  title =	"Decidable Higher-order Unification Problems",
  booktitle =	"Proceedings of the 12th International Conference on Automated
		  Deduction", 
  address =	"Nancy, France",
  month =	jun,
  year =	1994,
  publisher =	"Springer LNAI 814",
  pages =	"635--649",
  keywords =	"unification",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/papers/Prehofer-CADE1994.html"
}

@InProceedings{Prehofer94lics,
  author =	"Christian Prehofer",
  title =	"Higher-order Narrowing",
  booktitle =	"Proceedings of the Ninth Annual IEEE Symposium on Logic in
		  Computer Science",
  address =	"Paris, France",
  month =	jul,
  year =	1994,
  publisher =	"IEEE Computer Society Press",
  pages =	"507--516",
  keywords =	"unification, rewriting",
  urlhtml =	"http://www4.informatik.tu-muenchen.de/papers/Prehofer-LICS1994.html"
}

@PhdThesis{Prehofer95,
  author = 	 "Christian Prehofer",
  title = 	 "Solving Higher-Order Equations: From Logic to Programming",
  school = 	 "Technische Universit{\"a}t M{\"u}nchen",
  year = 	 1995,
  month =	 mar,
  keywords =	 "rewriting, unification"
}

@PhdThesis{Puls90,
  author =	"Thomas Puls",
  title =	"Annotation Logic for {Standard ML}",
  school =	"Technical University of Denmark",
  address =	"Lyngby",
  note =	"Department of Computer Science Report ID-TR:1990-74",
  month =	Oct,
  year =	1990,
  keywords =	"Isabelle"
}

@InProceedings{Pusch96,
  author = 	 "Cornelia Pusch",
  title = 	 "Verification of Compiler Correctness for the {WAM}",
  editor =	 "J. Wright and J. Grundy and J. Harrison",
  booktitle =	 "Proceedings of the 9th International Conference on
                  Theorem Proving in Higher Order Logics (TPHOL'96)",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1125",
  address =	 "Turku, Finland",
  month =	 aug,
  keywords =	 "Isabelle",
  urldvi =	 "http://www4.informatik.tu-muenchen.de/~pusch/pubs/WAM.dvi.gz"
}

@InProceedings{Pym90cade,
  author =	"David Pym and Lincoln Wallen",
  title =	"Investigations into Proof-Search in a System of First-Order
		  Dependent Function Types",
  booktitle =	"Proceedings of the 10th International Conference on Automated
		  Deduction",
  address =	"Kaiserslautern, Germany",
  editor =	"M.E. Stickel",
  publisher =	"Springer-Verlag LNCS 449",
  month =	jul,
  year =	"1990",
  pages =	"236--250",
  keywords = 	"LF"
}

@PhdThesis{Pym90phd,
  author =	"David Pym",
  title =	"Proofs, Search and Computation in General Logic",
  school =	"University of Edinburgh",
  year =	"1990",
  note =	"Available as CST-69-90, also published as ECS-LFCS-90-125",
  keywords = 	"LF"
}

@InProceedings{Pym91,
  author =	"David Pym and Lincoln A. Wallen",
  title =	"Proof Search in the {$\lambda\Pi$}-Calculus",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  pages =	"309--340",
  booktitle =	"Logical Frameworks",
  year =	1991,
  publisher =	"Cambridge University Press",
  keywords = 	"LF"
}

@InProceedings{Pym92alpuk,
  author =	"David Pym and Lincoln A. Wallen",
  title =	"Logic Programming via Proof-Valued Computations",
  editor =	"K. Broda",
  booktitle =	"Proceedings of the 4th {UK} Annual Conference on Logic
		  Programming",
  year =	1992,
  publisher =	"Springer-Verlag",
  address =	"London",
  month =	mar,
  keywords = 	"LF"
}

@Article{Pym92fcs,
  author =	"David Pym",
  title =	"A Unification Algorithm for the {$\lambda\Pi$}-Calculus",
  journal =	"International Journal of Foundations of Computer Science",
  year =	1992,
  volume =	3,
  number =	3,
  pages =	"333--378",
  month =	sep,
  keywords = 	"LF"
}

@Article{Pym94jlc,
  author =	"David J. Pym and James A. Harland",
  title =	"The Uniform Proof-Theoretic Foundation of Linear Logic
		  Programming",
  journal =	"Journal of Logic and Computation",
  pages =	"175--207",
  volume =	"4",
  number =	"2",
  month =	apr,
  year =	"1994",
  keywords = 	"linear"
}

@Article{Pym95,
  author =      "David J. Pym",
  title =       "A Note on the Proof Theory of the {$\lambda\Pi$}-Calculus",
  journal =     "Studia Logica",
  pages =       "199--230",
  volume =      54,
  number =      2,
  year =        1995,
  keywords =    "LF"
}

@InProceedings{Pym96,
  author = 	 "D. J. Pym",
  title = 	 "A Note on Representation and Semantics in Logical
  	          Frameworks",
  editor =	 "Didier Galmiche",
  pages = 	 "101--108",
  booktitle =	 "Informal Proceedings of the Workshop on Proof Search in
		  Type-Theoretic Languages",
  year =	 1996,
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =     "LF, linear"
}

@InProceedings{Pym99lics,
  author = 	 "David J. Pym",
  title = 	 "On Bunched Predicate Logic",
  editor =	 "G. Longo",
  pages =	 "183--192",
  booktitle =	 "Proceedings of the 14th Annual Symposium on Logic in
		  Computer Science (LICS'99)",
  year =	 1999,
  publisher =	 "IEEE Computer Society Press",
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "linear"
}

@InProceedings{Qian93,
  author =	"Zhenyu Qian",
  title =	"Linear Unification of Higher-Order Patterns",
  booktitle =	"Proceedings of the Colloquium on Trees in Algebra and
		  Programming",
  address =	"Orsay, France",
  editor =	"M.-C. Gaudel and J.-P. Jouannaud",
  month =	apr,
  year =	1993,
  pages =	"391--405",
  publisher =	"Springer-Verlag LNCS 668",
  keywords = 	"unification"
}

@Article{Qian95,
  author = 	 "Zhenyu Qian",
  title = 	 "Unification of Higher-Order Patterns in Linear Time
                  and Space",
  journal =	 "Journal of Logic and Computation",
  year =	 1995,
  volume =	 6,
  number =	 3,
  pages =	 "315--341",
  keywords =	 "unification"
}

@InProceedings{Raamsdonk99rta,
  author = 	 "Femke van Raamsdonk",
  title = 	 "Higher-Order Rewriting",
  editor =	 "P. Narendran and M. Rusinowitch",
  pages =	 "45--59",
  booktitle =	 "Proceedings of the 10th International Conference on
		  Rewriting Techniques and Applications (RTA-99)",
  year =	 1999,
  publisher =	 "Springer-Verlag LNCS 1631",
  address =	 "Trento, Italy",
  month =	 jul,
  note =	 "Invited Tutorial",
  keywords =	 "rewriting"
}
		  
@TechReport{Rasmussen95,
  author = 	 "Ole Rasmussen",
  title = 	 "The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
		  Experiment",
  institution =  "University of Cambridge, Computer Laboratory",
  month =	 mar,
  year = 	 1995,
  number =	 364,
  keywords =	 "Isabelle",
  urlps =	 "http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz"
}

@InProceedings{Rasmussen96,
  author = 	 "Ole Rasmussen",
  title = 	 "An Embedding of {Ruby} in {Isabelle}",
  editor =	 "M.A. McRobbie and J.K. Slaney",
  pages =	 "186--200",
  booktitle =	 "Proceedings of the 13th International Conference on
		  Automated Deduction",
  year =	 1996,
  publisher =	 "Springer-Verlag LNAI 1104",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "Isabelle"
}

@PhdThesis{Regensburger94,
  author = 	 "Franz Regensburger",
  title = 	 "{HOLCF}: Eine konservative Erweiterung von {HOL} um {LCF}",
  school = 	 "Technische Universit{\"a}t M{\"u}nchen",
  year = 	 1994,
  keywords =	 "Isabelle"
}

@InProceedings{Regensburger95,
  author = 	 "Franz Regensburger",
  title = 	 "{HOLCF}: {Higher} {Order} {Logic} of {Computable} {Functions}",
  editor =	 "E.T. Schubert and P.J. Windley and J. Alves-Foss",
  booktitle =	 "Proceedings of the 8th International Workshop on
                  Higher Order Logic Theorem Proving and Its Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 971",
  address =	 "Aspen Grove, Utah",
  month =	 sep,
  keywords =	 "Isabelle"
}

@Unpublished{Rohwedder94,
  author =	"Ekkehard Rohwedder",
  title =	"Verifying the Meta-Theory of Deductive Systems",
  note =	"Thesis Proposal",
  year =	1994,
  month =	feb,
  keywords = 	"LF, Elf"
}

@InProceedings{Rohwedder96esop,
  author = 	 "Ekkehard Rohwedder and Frank Pfenning",
  title = 	 "Mode and Termination Checking for Higher-Order Logic
                  Programs",
  editor =	 "Hanne Riis Nielson",
  booktitle =	 "Proceedings of the European Symposium on Programming",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1058",
  address = 	 "Link{\"o}ping, Sweden",
  month =	 apr,
  pages =        "296--310",
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/esop96.ps.gz"
}

@PhdThesis{Rohwedder96phd,
  author = 	 "Ekkehard Rohwedder",
  title = 	 "Verifying the Meta-Theory of Deductive Systems",
  school = 	 "School of Computer Science, Carnegie Mellon University",
  year = 	 1996,
  note =	 "Forthcoming",
  keywords =     "LF, Elf"
}

@InProceedings{Rollins91,
  author =	"Eugene J. Rollins and Jeannette M. Wing",
  title =	"Specifications as Search Keys for Software Libraries",
  pages =	"173--187",
  booktitle =	"Proceedings of the 1991 International Conference on Logic
		  Programming",
  editor =	"Koichi Furukawa",
  publisher =	"MIT Press",
  year =	"1991",
  keywords = 	"lambda-Prolog"
}

@InCollection{Rossen90,
  author =	"Lars Rossen",
  booktitle =	"Formal Methods for {VLSI} Design",
  title =	"Formal {Ruby}",
  editor =	"J. Staunstrup",
  publisher =	"Elsevier",
  year =	1990,
  keywords = 	"Isabelle"
}

@InProceedings{Rossen91dcc,
  author =	"Lars Rossen",
  title =	"Ruby Algebra",
  booktitle =	"Designing Correct Circuits",
  address =	"Oxford, England",
  editor =	"G. Jones and M. Sheeran",
  publisher =	"Springer-Verlag Workshops in Computing",
  month =	sep,
  year =	1990,
  keywords = 	"Isabelle"
}

@InProceedings{Rossen91ho,
  author =	"Lars Rossen",
  title =	"Proving (facts about) {Ruby}",
  booktitle =	"IV Higher Order Workshop",
  address =	"Banff, Alberta",
  editor =	"G. Birtwistle",
  pages =	"265--283",
  publisher =	"Springer-Verlag Workshops in Computing",
  month =	sep,
  year =	1990,
  keywords = 	"Isabelle"
}

@PhdThesis{Rossen92,
  author = 	 "Lars Rossen",
  title = 	 "A Relational Approach to Sequential {VLSI} Design",
  school = 	 "Department of Computer Science, Technical University of
		  Denmark",
  year = 	 1992,
  keywords =	 "Isabelle"
}

@Unpublished{Rudnicki92,
  author = 	 "Piotr Rudnicki",
  title = 	 "An Overview of the {Mizar} Project",
  note = 	 "Notes to a talk at the workshop on {\em Types for Proofs and
		  Programs}",
  address =      "B{\aa}stad, Sweden",
  year =	 1992,
  month =	 jun,
  keywords =	 "misc",
  urlhtml =      "http://www.cs.ualberta.ca/~piotr/Mizar/index.html"
}

@InProceedings{Ruess96,
  author = 	 "Harald Rue{\ss}",
  title = 	 "Reflection of Formal Tactics in a Deductive Reflection
  		  Framework",
  editor =	 "M.A. McRobbie and J.K. Slaney",
  pages =	 "628--642",
  booktitle =	 "Proceedings of the 13th International Conference on
		  Automated Deduction",
  year =	 1996,
  publisher =	 "Springer-Verlag LNAI 1104",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "misc"
}

@InProceedings{Ruess97,
  author = 	 "Harald Ruess",
  title = 	 "Computational Reflection in the Calculus of
                  Constructions and Its Application to Theorem Proving",
  editor =	 "R. Hindley",
  booktitle =	 "Proceedings fo the Third International Conference on
                  Typed Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "misc"
}

@InProceedings{Saibi94,
  author = 	 "Amokrane Sa{\"\i}bi",
  title = 	 "Formalization of a {$\lambda$}-Calculus with Explicit
		  Substitutions in {Coq}",
  editor = 	 "P. Dybjer and B. Nordstr{\"o}m and J. Smith",
  pages =	 "183--202",
  booktitle =	 "Proceedings of the International Workshop on Types for
		  Proofs and Programs",
  year =	 1994,
  publisher =	 "Springer-Verlag LNCS 996",
  address =	 "B{\aa}stad, Sweden",
  month =	 jun,
  keywords =	 "misc"
}

@Unpublished{Salvesen90,
  author =	"Anne Salvesen",
  title =	"The {Church-Rosser} Theorem for {LF} with
		  {$\beta\eta$}-Reduction",
  month =	may,
  year =	"1990",
  note =	"Unpublished notes to a talk given at the First Workshop on
		  Logical Frameworks in Antibes, France ",
  keywords = 	"LF"
}

@InProceedings{Sandner97,
  author = 	 "Roberto Sandner and Olaf M{\"u}ller",
  title = 	 "Theorem Prover Support for the Refinement of Stream
		  Processing Functions",
  editor =	 "E. Brinksma",
  pages =	 "351--365",
  booktitle =	 "Proceedings of the Third International Workshop on Tools and
		  Algorithms for the Construction and Analysis of Systems
		  (TACAS'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS 1217",
  address =	 "Enschede, The Netherlands",
  month =	 apr,
  keywords =	 "Isabelle",
  urlhtml =	 "http://wwwbroy.informatik.tu-muenchen.de/~mueller/publications.html"
}

@InProceedings{SchroederHeister91,
  author =	"Peter Schroeder-Heister",
  title =	"Structural Frameworks, Substructural Logics, and the Role of
		  Elimination Inferences",
  editor =	"G\'{e}rard Huet and Gordon Plotkin",
  pages =	"385--403",
  booktitle =	"Logical Frameworks",
  year =	1991,
  publisher =	"Cambridge University Press",
  keywords = 	"linear"
}

@InProceedings{SchroederHeister93elp,
  author =	"Peter Schroeder-Heister",
  title =	"Definitional Reflection and the Completion",
  editor =	"R. Dyckhoff",
  booktitle =	"Proceedings of the 4th International Workshop on Extensions
		  of Logic Programming",
  year =	1993,
  publisher =	"Springer-Verlag LNAI 798",
  pages	=	"333--347",
  keywords = 	"Pi"
}

@InProceedings{SchroederHeister93lics,
  author =	"Peter Schroeder-Heister",
  title =	"Rules of Definitional Reflection",
  editor =	"M. Vardi",
  pages =	"222--232",
  booktitle =	"Proceedings of the Eighth Annual {IEEE} Symposium on Logic in
		  Computer Science",
  address =	"Montreal, Canada",
  month =	jun,
  year =	1993,
  keywords = 	"Pi"
}

@MastersThesis{Schurmann95,
  author = 	 "Carsten Sch{\"u}rmann",
  title = 	 "A Computational Meta Logic for the {Horn} Fragment of {LF}",
  school = 	 "Carnegie Mellon University",
  year = 	 1995,
  month =	 dec,
  note =	 "Available as Technical Report CMU-CS-95-218",
  keywords =	 "LF"
}

@InProceedings{Schurmann98cade,
  author = 	 "Carsten Sch{\"u}rmann and Frank Pfenning",
  title = 	 "Automated Theorem Proving in a Simple Meta-Logic for {LF}",
  editor =	 "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  pages =	 "286--300",
  booktitle =	 "Proceedings of the 15th International Conference on
		  Automated Deduction (CADE-15)",
  year =	 1998,
  publisher =	 "Springer-Verlag LNCS 1421",
  address =	 "Lindau, Germany",
  month =	 jul,
  keywords =	 "LF, Elf",
  urlps =	 "http://www.cs.cmu.edu/~fp/papers/cade98m2.ps.gz"
}

@Article{Shankar88,
  author =	"N. Shankar",
  title =	"A Mechanical Proof of the {Church-Rosser} Theorem",
  journal =	"Journal of the Association for Computing Machinery",
  volume =	"35",
  number =	"3",
  month =	jul,
  year =	"1988",
  pages =	"475--522",
  keywords = 	"misc"
}

@Book{Shankar94,
  author = 	 "N. Shankar",
  title = 	 "Metamathematics, Machines, and G{\"o}del's Proof",
  publisher = 	 "Cambridge University Press",
  year = 	 1994,
  volume =	 38,
  series =	 "Cambridge Tracts in Theoretical Computer Science",
  keywords =     "misc"
}

@InProceedings{Simons97,
  author = 	 "Martin Simons",
  title = 	 "Proof Presentation for {Isabelle}",
  editor =	 "E. Gunter and A. Felty",
  pages =        "259--274",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
                  Proving in Higher Order Logics (TPHOLs'97)",
  address =      "Murray Hill, New Jersey",
  year =	 1997,
  month =	 aug,
  keywords =	 "Isabelle"
}

@InProceedings{Slotosch97,
  author = 	 "Oscar Slotosch",
  title = 	 "Higher Order Quotients and their Implementation in
                  {Isabelle HOL}",
  editor =	 "E. Gunter and A. Felty",
  pages =        "291--306",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
                  Proving in Higher Order Logics",
  address =      "Murray Hill, New Jersey",
  year =	 1997,
  month =	 aug,
  keywords =	 "Isabelle"
}

@Article{Snyder89,
  author =	"Wayne Snyder and Jean H. Gallier",
  title =	"Higher Order Unification Revisited: Complete Sets of
		  Transformations",
  journal =	"Journal of Symbolic Computation",
  volume =	"8",
  number =	"1-2",
  pages =	"101--140",
  year =	"1989",
  keywords = 	"unification"
}

@InProceedings{Stark97,
  author = 	 "Ian Stark",
  title = 	 "Names, Equations, Relations: Practical Ways to Reason
                  about ``new''",
  editor =	 "R. Hindley",
  booktitle =	 "Proceedings of the Third International Conference on
                  Typed Lambda Calculus and Applications (TLCA'97)",
  year =	 1997,
  publisher =	 "Springer-Verlag LNCS",
  address =	 "Nancy, France",
  month =	 apr,
  keywords =	 "misc"
}

@InProceedings{Stump99,
  author = 	 "Aaron Stump and David L. Dill",
  title = 	 "Generating Proofs from a Decision Procedure",
  editor =	 "A. Pnueli and P. Traverso",
  booktitle =	 "Proceedings of the FLoC Workshop on Run-Time Result
		  Verification",
  year =	 1999,
  address =	 "Trento, Italy",
  month =	 jul,
  keywords =	 "LF, Elf"
}

@TechReport{Sydow92,
  author = 	 "Bj{\"o}rn von Sydow",
  title = 	 "A Machine-Assisted Proof of the Fundamental Theorem of
		  Arithmetic",
  institution =  "Chalmers University of Technology",
  year = 	 1992,
  type =	 "PMG Report",
  number =	 68,
  address =	 "Sweden",
  month =	 jun,
  keywords =	 "ALF"
}

@MastersThesis{Szasz91,
  author = 	 "Nora Szasz",
  title = 	 "A Machine Checked Proof that {Ackermann's} Function is not
		  Primitive Recursive", 
  school = 	 "Chalmers University of Technology and University of
		  G{\"o}teborg",
  year = 	 1991,
  address =	 "Sweden",
  month =	 jun,
  type =	 "Licentiate Thesis",
  keywords =	 "ALF"
}

@MastersThesis{Tasistro93,
  author = 	"A. Tasistro",
  title = 	"Formulation of {Martin-L\"of's} Theory of Types with
                 Explicit Substitutions",
  school = 	"Chalmers Tekniska {H\"ogskola} and {G\"oteborgs} Universitet",
  year = 	"1993",
  month = 	"May",
  keywords =	"ALF"
}

@InProceedings{Tej97,
  author = 	 "H. Tej and B. Wolff",
  title = 	 "A Corrected Failure-Divergence Model for {CSP} in {Isabelle/HOL}",
  editor =	 "C. Jones and J. Fitzgerald",
  booktitle =	 "Proceedings of the International Formal Methods Europe
                  Symposium (FME'97)",
  year =	 1997,
  address =	 "Graz, Austria",
  month =	 sep,
  keywords =	 "Isabelle",
  urlps =	 "http://www.informatik.uni-bremen.de/~bu/papers/CSP.ps.gz"
}

@InProceedings{Terrasse95amast,
  author = 	 "Delphine Terrasse",
  title = 	 "Encoding Natural Semantics in {Coq}",
  booktitle =	 "Proceedings of the Fourth International Conference on
		  Algebraic Methodology and Software Technology",
  editor =       "V.S. Alagar",
  publisher =    "Springer-Verlag LNCS 936",
  year =	 1995,
  address =	 "Montreal, Canada",
  month =	 jul,
  pages =        "230--244",
  keywords =	 "misc"
}

@MastersThesis{Terrasse95ms,
  author = 	 "Delphine Terrasse",
  title = 	 "Vers un environnement de d{\'e}veloppement de preuves 
                  en S{\'e}mantique Naturelle",
  school = 	 "ENPC",
  year = 	 1995,
  type =	 "Th{\`e}se de Doctorat",
  keywords =	 "misc",
  urlps =	 "file://babar.inria.fr/pub/croap/terrasse/these_DT.ps"
}

@InProceedings{Thery92,
  author =	"Laurent Thery and Yves Bertot and Gilles Kahn",
  title =	"Real Theorem Provers Deserve Real User-Interfaces",
  booktitle =	"Proceedings of the Fifth {ACM} {SIGSOFT} Symposium on
		  Software Development Environments ", 
  note =	"Published as {SIGSOFT} Software Engineering Notes, Vol.~17,
		  No.~5",
  pages =	"120--129",
  year =	1992,
  keywords = 	"misc"
}

@PhdThesis{VanDaalen80,
  author =	"D.T. van Daalen",
  title =	"The Language Theory of Automath",
  school =	"Eindhoven University of Technology",
  year =	1980,
  keywords = 	"Automath"
}

@InProceedings{VanDePol95,
  author = 	 "J. van de Pol and H. Schwichtenberg",
  title = 	 "Strict Functionals for Termination Proofs",
  editor =	 "M. Dezani-Ciancaglini and G. Plotkin",
  booktitle =	 "Proceedings of the International Conference on Typed Lambda
		  Calculi and Applications",
  year =	 1995,
  publisher =	 "Springer-Verlag LNCS 902",
  address =	 "Edinburgh, Scotland",
  month =	 apr,
  pages =	 "350--364",
  keywords =     "rewriting"
}

@PhdThesis{VanInwegen96,
  author = 	 "Myra VanInwegen",
  title = 	 "The Machine-Assisted Proof of Programming Language Properties",
  school = 	 "University of Pennsylvania",
  year = 	 1996,
  month =	 aug,
  keywords =	 "misc"
}

@PhdThesis{Vigano97,
  author = 	 "Luca Vigan{\`o}",
  title = 	 "A Framework for Non-Classical Logics",
  school = 	 "Universit{\"a}t des Saarlandes",
  year = 	 1997,
  OPTaddress = 	 "Saarbr{\"u}cken, Germany",
  month =	 sep,
  keywords =	 "misc"
}

@InProceedings{Virga96rta,
  author = 	 "Roberto Virga",
  title = 	 "Higher-Order Superposition for Dependent Types",
  editor =	 "Harald Ganzinger",
  pages =	 "123--137",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  note =         "Extended version available as Technical Report
		  CMU-CS-95-150, May 1995",
  urlps =	 "ftp://reports.adm.cs.cmu.edu/usr/anon/1995/CMU-CS-95-150.ps",
  keywords =	 "LF, rewriting"
}

@PhdThesis{Virga99phd,
  author = 	 "Roberto Virga",
  title = 	 "Higher-Order Rewriting with Dependent Types",
  school = 	 "Department of Mathematical Sciences, Carnegie Mellon
		  University",
  year = 	 1999,
  note =	 "Forthcoming",
  keywords =	 "LF, Elf, rewriting"
}

@InProceedings{Vittek96,
  author = 	 "Marian Vittek",
  title = 	 "A Compiler for Nondeterministic Term Rewriting Systems",
  editor =	 "Harald Ganzinger",
  pages =	 "154--168",
  booktitle =	 "Proceedings of the 7th International Conference on Rewriting
		  Techniques and Applications",
  year =	 1996,
  publisher =	 "Springer-Verlag LNCS 1103",
  address =	 "New Brunswick, New Jersey",
  month =	 jul,
  keywords =	 "rewriting"
}

@Book{Wallen90,
  author = 	 "Lincoln A. Wallen",
  title = 	 "Automated Deduction in Non-Classical Logics",
  publisher = 	 "MIT Press",
  year = 	 1990,
  keywords =     "misc"
}

@InProceedings{Wenzel97,
  author = 	 "Markus Wenzel",
  title = 	 "Type Classes and Overloading in Higher-Order Logic",
  editor =	 "E. Gunter and A. Felty",
  pages =        "307--322",
  booktitle =	 "Proceedings of the 10th International Conference on Theorem
                  Proving in Higher Order Logics (TPHOLs'97)",
  address =      "Murray Hill, New Jersey",
  year =	 1997,
  month =	 aug,
  keywords =	 "Isabelle"
}

@Article{Wolfram89,
  author = 	 "David A. Wolfram",
  title = 	 "Intractable Unifiability Problems and Backtracking",
  journal =	 "Journal of Automated Reasoning",
  year =	 1989,
  volume =	 5,
  pages =	 "37--47",
  keywords =	 "unification"
}

@InProceedings{Wolfram90cade,
  author = 	 "David A. Wolfram",
  title = 	 "{ACE}: The Abstract Clause Engine",
  editor =	 "Mark E. Stickel",
  pages =	 "679--680",
  booktitle =	 "Proceedings of the Tenth International Conference on
		  Automated Deduction",
  year =	 1990,
  publisher =	 "Springer-Verlag LNCS 449",
  address =	 "Kaiserslautern, Germany",
  month =	 jul,
  note =	 "System Abstract",
  keywords =	 "misc"
}

@PhdThesis{Wolfram90phd,
  author = 	 "David A. Wolfram",
  title = 	 "The Clausal Theory of Types",
  school = 	 "University of Cambridge",
  year = 	 1990,
  month =	 mar,
  keywords =	 "misc"
}

@InProceedings{Wolfram91,
  author = 	 "David A. Wolfram",
  title = 	 "Rewriting, and Equational Unification: The Higher-Order
		  Cases",
  editor =	 "Ronald V. Book",
  pages =	 "25--36",
  booktitle =	 "Proceedings of the Fourth International Conference on
		  Rewriting Techniques and Applications",
  year =	 1991,
  publisher =	 "Springer-Verlag LNCS 488",
  address =	 "Como, Italy",
  month =	 apr,
  keywords =	 "rewriting, unification"
}

@Book{Wolfram93book,
  author =	"David Wolfram",
  title =	"The Clausal Theory of Types",
  publisher =	"Cambridge University Press",
  year =	"1993",
  keywords = 	"misc"
}

@InProceedings{Wolfram93types,
  author = 	 "David A. Wolfram",
  title = 	 "Semantics for Abstract Clauses",
  editor =	 "Henk Barendregt and Tobias Nipkow",
  pages =	 "366--383",
  booktitle =	 "Proceedings of the Workshop on Types for Proofs and
		  Programs", 
  year =	 1993,
  publisher =	 "Springer-Verlag LNCS 806",
  address =	 "Nijmegen, The Netherlands",
  month =	 may,
  keywords =	 "misc"
}

@Article{Wolfram94,
  author =	"David A. Wolfram",
  title =	"A Semantics for {$\lambda$Prolog}",
  journal =	"Theoretical Computer Science",
  year =	"1994",
  volume =	"136",
  number =	"1",
  pages =       "277--289",
  keywords = 	"lambda-Prolog"
}

@InProceedings{Zucker75,
  author =	"J. Zucker",
  title =	"Formalisation of Classical Mathematics in {AUTOMATH}",
  volume =	249,
  pages =	"135--145",
  booktitle =	"Colloques Internationaux du Centre National de Recherche
		  Scientifique",
  year =	1975,
  month =	jul,
  keywords = 	"Automath"
}