From af8ab1498c9d137146cdcadd5d9ef8027785f94e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 31 Jan 2003 16:08:59 +0000
Subject: Ajout Streicher (axiom K)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8316 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/biblio.bib | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'doc')

diff --git a/doc/biblio.bib b/doc/biblio.bib
index 8a6380d5ed..87783c50ba 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},
-- 
cgit v1.2.3