Ajout Streicher (axiom K)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8316 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/doc/biblio.bib b/doc/biblio.bib
index 8a6380d5e..87783c50b 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -563,6 +563,14 @@ s},
         YEAR               = {1994}
 }
 
+@INPROCEEDINGS{HofStr98,
+        AUTHOR        = {Martin Hofmann and Thomas Streicher},
+        TITLE         = {The groupoid interpretation of type theory},
+        BOOKTITLE     = {Proceedings of the meeting Twenty-five years of constructive type theory},
+        PUBLISHER     = {Oxford University Press},
+        YEAR          = {1998}
+} 
+
 @INCOLLECTION{How80,
         AUTHOR             = {W.A. Howard},
         BOOKTITLE          = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
@@ -990,6 +998,12 @@ Decomposition}},
         YEAR               = {1994}
 }
 
+@misc{streicher93semantical,
+  author = "T. Streicher",
+  title = "Semantical Investigations into Intensional Type Theory",
+  note = "Habilitationsschrift, LMU Munchen.",
+  year = "1993" }
+
 @INCOLLECTION{wadler87,
         AUTHOR             = {P. Wadler},
         TITLE              = {Efficient  Compilation of Pattern Matching},