1 files changed, 21 insertions, 20 deletions
diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index d52cac0a67..77baf97998 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -1,30 +1,31 @@
-%%%%%%% F %%%%%%%
+%%%%%%% FAQ %%%%%%%
 
-@misc{fk:Practicals,
-  author = {Florent Kirchner},
-  title = "Programmation Tacticals",
-  year  = 2003,
-  note = "{\tt http://research.nianet.org/fm-at-nia/Practicals/}"
+@book{ProofsTypes,
+  Author="Girard, J.-Y. and Y. Lafont and P. Taylor",
+  Title="Proofs and Types",
+  Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press",
+  Year="1989"
 }
 
-@mastersthesis{fk:DEA,
-  author= {Florent Kirchner},
-  title= "{Towards a Common Tactical Language : The Case of Coq and PVS}",
-  school= {DEA Programmation : Sémantique, Preuves et Langages},
-  year= 2003
+@misc{Types:Dowek,
+  author = "Gilles Dowek",
+  title = "Th{\'e}orie des types",
+  year = 2002,
+  howpublished = "Lecture notes",
+  url= "http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz"
 }
 
-@inproceedings{fk:strata2003,
-  author= {Florent Kirchner},
-  editor= {Mila Archer et al.},
-  title= "{Coq Tacticals and PVS Strategies: A Small-Step Semantics}",
-  pages= {69-83},
-  booktitle= "{Design and Application of Strategies/Tactics in Higher Order Logics}",
-  publisher= {NASA},
-  month= "September",
-  year= 2003
+@PHDTHESIS{EGThese,
+  author = {E. Giménez},
+  title = {Un Calcul de Constructions Infinies et son application
+a la vérification de systèmes communicants},
+  type = {thèse d'Université},
+  school = {Ecole Normale Supérieure de Lyon},
+  month = {December},
+  year = {1996},
 }
 
+
 %%%%%%% Semantique %%%%%%%
 
 @misc{Sem:cours,