% log.bib
% Aaron Stump, 5/4/99
%
% This file contains references to a number of works on
% formal systems.

@book{A65,
author="P. Andrews",
title="A Transfinite Type Theory with Type Variables",
publisher="North-Holland",
year=1965}

@book{A86,
author="P. Andrews",
title={{An Introduction to Mathematical Logic and Type Theory: to Truth through Proof}},
publisher="Academic Press",
year=1986}

@conference{Coq86,
author = "T. Coquand",
title = {{An analysis of Girard's paradox}},
booktitle = "1st Symposium on Logic in Computer Science",
year="1986",
pages="227-236"}

@article{L99,
author = "L. \L ukaszewicz",
title = {{Triple Dots in a Formal Language}},
journal = "Journal of Automated Reasoning",
volume="22",
year = 1999,
pages = "223-239"}

@conference{Coq94,
author = "T. Coquand",
title = {{A new paradox in type theory}},
booktitle = "9th International Conference on Logic, Methodology, and
                  Philosophy of Science",
year="1994",
pages="555-570"}

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

@article{H63,
author = "L. Henkin",
title = {{A theory of propositional types}},
journal = "Journal of Symbolic Logic",
volume="52",
year = 1963,
pages = "323-344"}

@article{A63,
author = "P. Andrews",
title = {{A reduction of the axioms for the theory of propositional types}},
journal = "Fundamenta Mathematicae",
volume="52",
year = 1963,
pages = "345-350"}

@Book{E72,
title = {{A Mathematical Introduction to Logic}},
author = "H. Enderton",
year = "1972",
publisher = "Academic Press"}

@Book{GLR95,
title = {{Advances in Linear Logic}},
author = "J.-Y. Girard and Y. Lafont and L. Regnier",
year = "1995",
publisher = "Cambridge University Press"}

@Book{H97,
title = {{A Shorter Model Theory}},
author = "W. Hodges",
year = "1997",
publisher = "Cambridge University Press"}

@Book{Mi00,
title = {{A Short Introduction to Intuitionistic Logic}},
author = "G. Mints",
year = "2000",
publisher = "Kluwer Academic / Plenum Publishes"}

@Book{Prawitz65,
title = {{Natural Deduction: a Proof-Theoretical Study}},
author = "D. Prawitz",
year = "1965",
publisher = "Almquist \& Wiksells"}

@Book{HA50,
title = {{Principles of Mathematical Logic}},
author = "D. Hilbert and W. Ackermann",
year = "1950",
publisher = "Chelsea Publishing Company",
note={{Translated from 2nd German edition of 1938}}}

@Book{CF50,
title = {{Combinatory Logic}},
volume = "1",
author = "H. Curry and R. Feys",
year = "1958",
publisher = "North-Holland Publishing Company"}

@Book{CHS72,
title = {{Combinatory Logic}},
volume = "2",
author = "H. Curry and J. Hindley and J. Seldin",
year = "1972",
publisher = "North-Holland Publishing Company"}

@Inbook{L80,
author = "J. Lambek",
crossref = "SH80",
pages = "375-402",
title = {{From $\lambda$-calculus to Cartesian closed categories}}}

@InCollection{H80,
author = "W. Howard",
crossref = "SH80",
pages = "479-490",
title = {{The formulae-as-types notion of construction}}}

@Book{SH80,
booktitle = {{To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus,
          and Formalism}},
editor = "J. Seldin and J. Hindley",
year = "1980",
publisher = "Academic Press"}

@Book{M96,
title = {{Foundations for Programming Languages}},
author = "J. Mitchell",
year = "1996",
publisher = "The MIT Press"}

@Book{C41,
title = {{The Calculi of Lambda-Conversion}},
author = "A. Church",
year = "1941",
publisher = "Princeton University Press"}

@book{gtl90,
author = "J.-Y. Girard and Y. Lafont and P. Taylor",
year = 1990,
publisher = "Cambridge University Press",
title={{Proofs and Types}}}

@conference{G71,
author = "J.Y. Girard",
title = {{Une extension de l'interpretation de G\"{o}del a l'analyse,
                  et son application a l'elimination des coupures dans
                  l'analyse et la theorie des types}},
booktitle = "2nd Scandinavian Logic Symposium",
year="1971",
pages="63-92"}

@book{T51,
author = "A. Tarski",
title = {{A decision method for elementary algebra and geometry}},
publisher = "University of California Press",
year = "1951"}

@Book{FBL73,
title = {{Foundations of Set Theory}},
author = "A. Fraenkel and Y. Bar-Hillel and A. Levy",
year = "1973",
publisher = "Elsevier Science Publishers B.V."}

@Book{F76,
title = {{Abstract Set Theory}},
author = "A. Fraenkel",
year = "1976",
publisher = "North-Holland Publishing Company",
note={{Revised by A. Levy}}}

@Book{BGG97,
title = {{The Classical Decision Problem}},
author = {{E. B\"{o}rger, E. Gr\"{a}del, and Y. Gurevich}},
year = "1997",
publisher = "Springer"}

@Misc{tata97,
author =       {H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez and S. Tison and M. Tommasi},
title =        {Tree Automata Techniques and Applications},
howpublished = {Available at {http://www.grappa.univ-lille3.fr/tata}},
year =         1997}

@book{K52,
author = "S. Kleene",
title = "Introduction to Metamathematics",
publisher = "Van Nostrand",
year = "1952"}

@book{TS00,
author = "A. Troelstra and H. Schwichtenberg",
publisher="Cambridge University Press",
year=2000,
edition="2nd",
title="Basic Proof Theory"}

@book{troelstra92,
author = "A. Troelstra",
publisher="Center for the Study of Language and Information",
year=1992,
title="Lectures on Linear Logic"}

@phdthesis{polakow_thesis,
author = "J. Polakow",
title = {{Ordered Linear Logic and Applications}},
year="2001",
school={Carnegie Mellon University}}

@incollection{feferman05,
title="Predicativity",
author="S. Feferman",
booktitle={{The Oxford Handbook of Philosophy of Mathematics and Logic}},
editor="S. Shapiro",
publisher="Oxford University Press",
year=2005,
pages="590-624"}

@InProceedings{pitts01,
  author =	 {A. M. Pitts},
  title =	 {Nominal Logic: A First Order Theory of Names and
                  Binding},
  booktitle =	 {Theoretical Aspects of Computer Software, 4th
                  International Symposium, TACS 2001, Sendai, Japan,
                  October 29-31, 2001. Proceedings},
  pages =	 {219--242},
  year =	 2001,
  editor =	 {N. Kobayashi and B. C. Pierce},
  volume =	 2215,
  series =	 {Lecture Notes in Computer Science},
  publisher =	 {Springer-Verlag, Berlin},
  isbn =	 {3-540-42736-8}
}

@book{boolos-provability-logic,
author = "George Boolos",
publisher="Cambridge University Press",
year=1993,
title="The logic of provability"}


@inbook{W80,
author="C. Wadsworth",
title={{Some Unusual $\lambda$-Calculus Numeral Systems}},
crossref="SH80",
pages="215-230"}

@book{halmos74,
author="P. Halmos",
title={{Naive Set Theory}},
year=1974,
publisher="Springer-Verlag"}

@inproceedings{leivant74,
author="D. Leivant",
title={{Strong Normalization for Arithmetic}},
editor="A. Dold and B. Eckmann",
booktitle={{Proof Theory Symposium}},
year=1974,
location=Kiel,
pages="182--197"}

@article{gabbaypitts02,
  author="Murdoch Gabbay and Andrew Pitts",
  title="A New Approach to Abstract Syntax with Variable Binding",
  journal="Formal Aspects of Computing",
  volume=13,
  year=2002,
  pages={341--363}
}

@InProceedings{urban+05,
  author =       {C.~Urban and C.~Tasson},
  title =        {{N}ominal {T}echniques in {I}sabelle/{HOL}},
  booktitle =    {Proc.~of the 20th International Conference on
                  Automated Deduction (CADE)},
  year =         2005,
  series =       {LNCS},
  pages =        {38--53},
  volume =       3632
}

@inproceedings{aydemir+07,
  Author = {Brian Aydemir and Aaron Bohannon and Stephanie Weirich},
  Booktitle = {Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice ({LFMTP} 2006)},
  Editor = {Alberto Momigliano and Brigitte Pientka},
  Publisher = {Elsevier},
  Year = 2007,
  Doi = {10.1016/j.entcs.2007.01.028},
  Pages = {69--77},
  Title = {Nominal Reasoning Techniques in {Coq} (Extended Abstract)}
}
