@string{itp = "International Conference on Interactive Theorem Proving"}
@string{tphols = "International Conference on Theorem Proving in Higher Order Logics"}
@string{proc = "Proceedings of the"}
@string{lncs = "Lecture Notes in Computer Science"}
@string{access = "Last access:"}
@string{avail = "Available at:"}

@Article{russell1908ajm,
  author = 	 {Bertrand Russell},
  title = 	 {Mathematical Logic as Based on the Theory of Types},
  journal = 	 {American Journal of Mathematics},
  year = 	 {1908},
  volume = 	 {30},
  number = 	 {3},
  pages = 	 {222-262},
  month = 	 {Jul.}
}

@Article{church1940jsl,
  author = 	 {Alonzo Church},
  title = 	 {A Formulation of the Simple Theory of Types},
  journal = 	 {The Journal of Symbolic Logic},
  year = 	 {1940},
  volume = 	 {5},
  number = 	 {2},
  pages = 	 {56--68},
  month = 	 {Jun.}
}

@InBook{howard1980,
  author = 	 {William A. Howard},
  title = 	 {To {H. B. Curry}: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  chapter = 	 {The formulae-as-types notion of construction},
  publisher = 	 {Academic Press Inc.},
  year = 	 {1980},
  month = 	 {Sep.},
  pages = 	 {479–-490},
  note = 	 {Original paper manuscript from 1969.}
}

@Book{graham1994,
  author = 	 {Ronald L. Graham and Donald E. Knuth and Oren Patashnik},
  title = 	 {Concrete Mathematics: A Foundation for Computer Science},
  publisher = 	 {Addison-Wesley},
  year = 	 {1994},
}

@Book{fregegodel,
  author = 	 {Jean van Heijenoort},
  title = 	 {From {Frege} to {G\"odel}---A Source Book in Mathematical Logic, 1879-1931},
  publisher = 	 {Harvard University Press},
  year = 	 {2002}
}

@InProceedings{reynolds2002lics,
  author = 	 {John C. Reynolds},
  title = 	 {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = proc # {17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark},
  pages = 	 {55--74},
  year = 	 {2002},
  publisher = {IEEE Computer Society}
}

@Article{romero2013ams,
  author = 	 {Ana Romero and Julio Rubio},
  title = 	 {Homotopy groups of suspended classifying spaces: An experimental approach},
  journal = 	 {Mathematics of Computation},
  year = 	 {2013},
  volume = 	 {82},
  pages = 	 {2237--2244}
}

@Article{pelayo2014bams,
  author = 	 {{\'A}lvaro Pelayo and Michael A. Warren},
  title = 	 {Homotopy type theory and {Voevodsky's} univalent foundations},
  journal = 	 {Bull. Americ. Math. Soc.},
  year = 	 {2014},
  volume = 	 {51},
  number = 	 {4},
  pages = 	 {597--648},
  month = 	 {Oct.},
  note = 	 {Article electronically published on May 9, 2014}
}