hott_references.bib

% This file was created with JabRef 2.8.
% Encoding: MacRoman

@incollection{deBruijn95,
	author = {N. G. de Bruijn},
	booktitle = {The Curry-Howard Isomorphism},
	title = {On the Roles of Types in Mathematics},
        series = {Cahiers du Centre de Logique},
        volume = {8},
        editor = {Philippe de Groote},
	publisher = {Academia},
	year = {1995}
}

@BOOK{HoTTBook2013,
  title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {The Univalent Foundations Program},
  year = {2013},
  author = {Institute for Advanced Study},
  note = {\url{http://homotopytypetheory.org/book/}},
  owner = {stephaniebalzer},
  timestamp = {2013.09.14}
}

@ELECTRONIC{Harper2013,
  author = {Robert Harper},
  month = {July},
  year = {2013},
  title = {Constructive Mathematics Is Not Metamathematics},
  howpublished = {\url{http://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/}},
  owner = {stephaniebalzer},
  timestamp = {2013.09.13}
}


@ELECTRONIC{Harper2013a,
  author = {Robert Harper},
  month = {June},
  year = {2013},
  title = {WhatÕs the big deal with {HoTT}?},
  howpublished = {\url{http://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-hott/}},
  owner = {stephaniebalzer},
  timestamp = {2013.09.13}
}

@ELECTRONIC{Harper2012,
  author = {Robert Harper},
  month = {August},
  year = {2012},
  title = {Extensionality, Intensionality, and {Brouwer}'s Dictum},
  howpublished = {\url{http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/}},
  owner = {stephaniebalzer},
  timestamp = {2013.09.13}
}

@Unpublished{Pfenning2009a,
  author =       {Frank Pfenning},
  title =        {Lecture Notes on Natural Deduction},
  note =         {\url{http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/02-natded.pdf}},
  month =     {August},
  year =      {2009} 
}

@Unpublished{Pfenning2009b,
  author =       {Frank Pfenning},
  title =        {Lecture Notes on Harmony},
  note =         {\url{http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf}},
  month =     {September},
  year =      {2009} 
}

@article{Lamport99,
  author    = {Leslie Lamport and
               Lawrence C. Paulson},
  title     = {Should your specification language be typed},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {21},
  number    = {3},
  year      = {1999},
  pages     = {502-526},
  ee        = {http://doi.acm.org/10.1145/319301.319317},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ELECTRONIC{MartinLof80,
  author = {Per Martin-L\"{o}f},
  title = {Intuitionistic Type Theory},
  howpublished = {\url{http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf}},
  year = {1980}
}

@ELECTRONIC{PMLTT,
  author = {Bengt Nodstr\"{o}m, Kent Petersson, Jan M. Smith},
  year = {1990},
  title = {Programming in Martin-L\"{o}f's Type theory},
  howpublished = {\url{http://www.cse.chalmers.se/research/group/logic/book/book.pdf}},
  owner = {nrfulton}
}

@article{Smith84,
  author    = {Jan M. Smith},
  title     = {An Interpretation of Martin-Lof's Type Theory in a Type-Free
               Theory of Propositions},
  journal   = {J. Symb. Log.},
  volume    = {49},
  number    = {3},
  year      = {1984},
  pages     = {730-753},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Whitehead63,
  author = {Whitehead, Alfred North and Russell, Bertrand},
  publisher = {Cambridge University Press},
  title = {Principia Mathematica},
  volume = {1},
  year = {1963},
  note = {Reprint of the 1927 second edition. Accessed at
          \url{https://archive.org/details/PrincipiaMathematicaVolumeI}}
}


@article{Hedberg98,
 author = {Hedberg, Michael},
 title = {A coherence theorem for Martin-L\"{o}f's type theory},
 journal = {J. Funct. Program.},
 issue_date = {July 1998},
 volume = {8},
 number = {4},
 month = jul,
 year = {1998},
 issn = {0956-7968},
 pages = {413--436},
 numpages = {24},
 url = {http://dx.doi.org/10.1017/S0956796898003153},
 doi = {10.1017/S0956796898003153},
 acmid = {969597},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 

@comment{jabref-meta: selector_review:}

@comment{jabref-meta: selector_publisher:}

@comment{jabref-meta: selector_author:}

@comment{jabref-meta: selector_journal:}

@comment{jabref-meta: selector_keywords:}

@ELECTRONIC{WikiFunctor,
  author = {Wikipedia},
  title = {Functor},
  howpublished = {\url{http://en.wikipedia.org/wiki/Functor}},
  year = {2013}
}