...

[bitonic-mengthesis.git] / thesis.bib

diff --git a/thesis.bib b/thesis.bib
index f46fb3dc2c1dbdde13aec10ccd5cbbe963fe0786..60e575bc7a5b534e9d046b7121468809cedfb2d1 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -386,3 +386,36 @@ year = {2012}
   file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF},
   publisher = {Citeseer}
 }
+
+
+@inproceedings{Hofmann1994,
+  title={The groupoid model refutes uniqueness of identity proofs},
+  author={Hofmann, Martin and Streicher, Thomas},
+  booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on},
+  pages={208--212},
+  year={1994},
+  organization={IEEE}
+}
+
+@INPROCEEDINGS{Coquand1992,
+  author = {Coquand, Thierry},
+  title = {Pattern matching with dependent types},
+  booktitle = {Informal proceedings of Logical Frameworks},
+  year = {1992},
+  volume = {92},
+  pages = {66--79},
+  organization = {Citeseer},
+  file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript}
+}
+
+@INPROCEEDINGS{Abel2007,
+  author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter},
+  title = {Normalization by evaluation for Martin-Lof type theory with typed
+       equality judgements},
+  booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium
+       on},
+  year = {2007},
+  pages = {3--12},
+  organization = {IEEE},
+  file = {:/home/bitonic/docs/papers/nbe.pdf:PDF}
+}