@Phdthesis{abel:thesis,
author={A. Abel},
title={A Polymorphic Lambda-Calculus with Sized Higher-Order Types},
school={Ludwig-Maximilians-Universit\"at M\"unchen},
year={2006}}
  

@phdthesis{ach:thesis,
author={P. Achten},
title={Interactive Functional Programs: models, methods and implementation},
school={University of Nijmegen}, 
year={1996}}

@phdthesis{Matos:phd,
author={A. {Almeida Matos}},
title={Typing secure information flow:  declassification and mobility},
year={2006},
school={Ecole Nationale Sup\'erieure des Mines de Paris}}


@Phdthesis{thorsten:thesis,
author={T. Altenkirch},
title={Constructions, inductive types and strong normalisation},
school={Laboratory for the Foundations of Computer Science, University
		  of Edinburgh},
year={1994}}

@Phdthesis{aspinall:thesis,
author={D. Aspinall},
title={Type Systems for Modular Programs and Specifications},
school={Laboratory for the Foundations of Computer Science, University
		  of Edinburgh},
year={1997}} 

@PHDTHESIS{aud:thesis,
 AUTHOR       = {P. Audebaud},
 TITLE        ={Extensions du {C}alcul des {C}onstructions par points fixes}, 
 SCHOOL       = {Universit{\'e} Bordeaux I},
 YEAR         = 1992
}

@MastersThesis{bac:dea,
author={Bac, A.},
title="Un algorithme d'inf{\'e}rence de types pour les types
coinductifs",
school="{\'E}cole Normale Sup{\'e}rieure de Lyon",
year={1998}}

@MastersThesis{anthony:msc,
  author = 	"A. Bailey",
  title = 	"{Representing Algebra in LEGO}",
  school = 	"University of Edinburgh",
  year = 	"1993"
}

@phdthesis{anthony:thesis,
  author = 	"A. Bailey",
  title = 	"{The Machine-Checked Literate Formalisation of Algebra in
                 Type Theory}",
  school = 	"University of Manchester",
  year = 	"1998"
}

@phdthesis{barras:thesis,
author={B. Barras},
title={{Auto-validation d'un syst\`eme de preuves avec familles inductives}},
school={Universit{\'e} Paris 7},
year={1999}}

@phdthesis{ben:thesis,
author={N. Benton},
title={Strictness Analysis of Lazy Functional Programs},
year={1992},
school={University of Cambridge}}

@phdthesis{stefano:thesis,
author={S. Berardi},
title={Type dependence and Constructive Mathematics},
school={University of Torino},
year={1990}}

@MastersThesis{ber:msc,
author={P. Bertelsen},
title={{Semantics of Java Byte Code}},
school={Department of Computer Science, Royal Veterinary and
                  Agricultural University of Copenhagen},
year={1997}}

@phdthesis{gustavo:thesis,
author={G. Betarte},
title={Dependent Record Types and Algebraic Structures in Type Theory},
school={Department of Computer Science, Chalmers  Tekniska H{\"o}gskola},
year={1998}}


@PhdThesis{blanqui:thesis,
  author = 	 {F. Blanqui},
  title = 	 {Th\'eorie des Types et {R}\'ecriture},
  school = 	 {Universit\'e Paris XI, Orsay, France},
  year = 	 2001,
  note =	 {Available in english as "Type theory and Rewriting"}
}
@PhdThesis{boh:thesis,
  author =       "H. Boehm",
  title =        "A Logic for the Russell Programming Language",
  school =       "Cornell University",
  year =         "1983"}

@phdthesis{bor:thesis,
author={T. Borghuis},
title={Coming to terms with modal logic: on the interpretation of
		  modalities in typed $\lambda$-calculi},
school={Technische Universiteit Eindhoven},
year={1994}}

@PHDTHESIS{samuel:thesis,
  author = {S. Boutin},
  title = {R{\'e}flexions sur les quotients},
  school = {Paris 7},
  year = {1997}}

@phdthesis{venanzio:thesis,
  author   = "V. Capretta",
  title    = "{Abstraction and Computation}",
  school   = "University of Nijmegen, Computing Science Institute",
  year     = 2002
}

@phdthesis{ced:thesis,
author={J. Cederquist},
title={A point-free approach to constructive analysis in type theory},
year={1997},
school={Chalmers Tekniska H{\"o}gskola}}

@Phdthesis{adriana:thesis,
author={A. Compagnoni},
title={Higher-order subtyping with intersection types},
school={Department of Computer Science, University of Nijmegen},
year={1995}}

@PhdThesis{catarina:thesis,
  author =       "C. Coquand",
  title =        "Computation in Type Theory",
  school =       "Department of Computing Science, Chalmers University of
                 Technology",
  year =         "1996"}

@phdthesis{cristina:thesis,
author={C. Cornes},
title="Conception d'un langage de haut niveau de representation de preuves:
       R{\'e}currence par filtrage de motifs; Unification en pr{\'e}sence de 
        types inductifs primitifs; Synth{\`e}se de lemmes d'inversion",
school={Universit{\'e} de Paris 7},
year={1997}} 

@phdthesis{judicael:thesis,
author={J. Courant},
title = {Un calcul de modules pour les syst{\`e}mes de types purs},
school = {Ecole Normale Sup{\'e}rieure de Lyon},
year = {1998},
}

@PHDTHESIS{pierre:thesis,
  author = {P. Courtieu},
  title = {{Repr{\'e}sentation d'Alg{\`e}bres Non Libres en Th{\'e}orie des Types}},  
  school = {Universit{\'e} Paris 11},
  year = {2001}}


@phdthesis{cur:thesis,
author={R. Curien},
title = {Outils pour la preuve par analogie},
school = {Universit{\'e} de Nancy},
year = {1995},
}

@PhdThesis{daa:thesis,
author={Daalen, D. van},
title={The language theory of {A}utomath},
school={Technical University of Eindhoven},
year={1980}}


@mastersthesis{guillaume:dea,
author={G. Dufay},
school = {Universit{\'e} de Paris 7},
title={Certification d'abstractions pour la s{\'e}curisation de programmes Java},
year = {2000},
}

@phdthesis{guillaume:thesis,
author={G. Dufay},
title={V\'erification formelle de la plateforme JavaCard},
school={Universit\'e de Nice Sophia-Antipolis},
year={2003}}

@phdthesis{hugo:thesis,
author={H. Elbers},
title={Connecting formal and informal mathematics},
school={Technische Universiteit Eindhoven},
year={1998}}


@phdthesis{maribel:thesis,
author={M. Fern{\'a}ndez},
title={Mod{\`e}les de calcul multiparadigmes fond{\'e}s sur la
		  r{\'e\'e}criture}, 
school={{Universit\'e Paris-Sud Orsay}},
year={1993}}

@phdthesis{mariajoao:thesis,
author={M. J. Frade},
title={Constructor Subtyping}, 
school={{Universidade do Minho}},
year={200x},
note={Forthcoming}}


@Phdthesis{geser:thesis,
author={A. Geser},
title={Relative termination},
school={Universiteit Passau},
YEAR = 1990,
NOTE = {Appeared as technical report 91-03, Ulmer Informatik-Berichte,
                  Universit{\ä}t Ulm}}

 
@phdthesis{herman:thesis,
author={H. Geuvers},
title={Logics and type systems},
school={University of Nijmegen}, 
year={1993}}


@Phdthesis{gha:thesis,
author={N. Ghani},
title={Adjoint rewriting},
school={Laboratory for the Foundations of Computer Science, University
		  of Edinburgh},
year={1995}}

@phdthesis{ghe:thesis,
author={G. Ghelli},
title={Proof theoretic studies about a minimal type system integrating
		  inclusion and parametric polymorphism},
school={Universit{\`a} di {P}isa},
year={1990},
note={Appeared as technical report TD-6/90, {D}ipartimento di
		  {I}nformatica, Universit{\`a} di {P}isa}}

@PHDTHESIS{eduardo:thesis
, AUTHOR       = {Gim{\'e}nez, E.}
, TITLE        = {Un calcul de constructions infinies et son application 
    \`a la v\'erification de syst\`emes communicants}
, SCHOOL       = {Ecole Normale Superieure de Lyon}
, YEAR         = {1996}
}

@Misc{gir:thesis,
  author = 	 {J-Y. Girard},
  title = 	 {\emph{Interpr\'etation fonctionnelle et \'elimination
                des  coupures dans l'arithm\'etique d'ordre sup\'erieur}}, 
  howpublished = {Th\`ese d'Etat, Universit{\'e} Paris 7},
  year = 	 {1972}
}

@Phdthesis{healf:thesis,
author={H. Goguen},
title={A typed operational semantics for UTT},
school={Laboratory for the Foundations of Computer Science, University
		  of Edinburgh},
year={1994}}

@Book{gor:thesis,
  author = 	 "A. D. Gordon",
  title = 	 "Functional Programming and Input/Output",
  publisher = 	 "Cambridge University Press",
  year = 	 1994}



@PhdThesis{gro:thesis,
  author = 	 {D. P. Grove},
  title = 	 {Effective Interprocedural Optimization of
                  Object-Oriented Languages},  
  school = 	 {University of Wahsington},
  year = 	 {1998}
}

@Misc{thomas:lic,
author={T. Hallgren},
title={\emph{Subtypes in Polymorphic Functional Languages}}, 
 howpublished ={{Licenciate Thesis, Department of Computer Science, Chalmers
  Tekniska H{\"o}gskola}}, 
year={1993}}

@book{har:thesis,
  author =       {J. Harrison},
  title =        {{Theorem Proving with the Real Numbers}},
  publisher =    springer,
  year =         {1998},
  series =       {Distinguished Dissertations}
}


@mastersthesis{ludovic:dea,
author={L. Henrio},
school = {Universit{\'e} de Paris 7},
title={Analyse de partage pour applications JavaCard},
year = {2000},
}


@phdthesis{her:thesis,
author={H. Herbelin},
title={S{\'e}quents qu'on calcule},
school={Universit{\'e} Paris 7},
year={1995}}


@Phdthesis{martin:thesis,
author={M. Hofmann},
title={{Extensional Concepts in Intensional Type Theory}},
school={Laboratory for the Foundations of Computer Science, University
		  of Edinburgh},
year={1995}}


@phdthesis{howe:thesis,
 Author={D. Howe},
title={ Automating reasoning in an implementation
of constructive type theory},
School={Department of Computer Science, Cornell University},
year={1988}}

@PHDTHESIS{hurd:thesis,
  AUTHOR = {J. Hurd},
  TITLE = {Formal Verification of Probabilistic Algorithms},
  SCHOOL = {University of Cambridge},
  YEAR = 2002}

@phdthesis{jackson:thesis
, Author={P. Jackson}
, Title={Enhancing the {Nuprl} proof development system and applying
		  it to computational abstract algebra}
, School={Department of Computer Science, Cornell University}
, year={1995}
, month={January}
}

@PHDTHESIS{bart:thesis, 
AUTHOR       = "B. Jacobs", 
TITLE        = "Categorical Type Theory", 
SCHOOL       = "University of Nijmegen", 
YEAR         = 1991}


@phdthesis{jon:thesis,
author={M. Jones},
title={Qualified types: theory and practice},
school={Oxford University},
year={1992}}

@phdthesis{jasper:thesis,
author={J. Kamperman},
title={Efficient compilation of term-rewriting systems},
year={1996},
school={University of Amsterdam}}



@PhdThesis{kesner:thesis,
  author        = "D. Kesner",
  title         = "La d\'efinition de fonctions par cas \`a l'aide de
                 motifs dans des langages applicatifs",
  school        = "Universit\'e Paris-Sud",
  year          = 1993}

@PhdThesis{gerwin:thesis,
  author        = "G. Klein",
  title         = "Verified Java Bytecode Verification",
  school        = "Technical University Munich",
  year          = 2003}

@phdthesis{koh:thesis,
   author = {M. Kohlhase},
   school = {Universit{\"a}t des Saarlandes},
   title = {A Mechanization of Sorted Higher-Order Logic Based on the
		  Resolution Principle}, 
   year = {1994}}

@phdthesis{twan:thesis,
author={T. Laan},
title={The evolution of type theory in logic and mathematics},
school={Technische Universiteit Eindhoven},
year={1997}}

@phdthesis{lac:thesis,
author={S. Lack},
title={The algebra of distributive and extensive categories},
school={University of Cambridge},
year={1995}}

@phdthesis{leino:thesis,
 author = {K.R.M. Leino},
 title = {Toward reliable modular programs},
 year = {1995},
 school = {California Institute of Technology},
 }

@phdthesis{lil:thesis,
		  author={M. Lillibridge},
		  title={Translucent Sums: A Foundation for
		  Higher-Order Module Systems}, 
		  school={ School of Computer Science, Carnegie Mellon
                  University},
		  year={1997}} 
		  

@phdThesis{lena:thesis,
Author={L. Magnusson},
title={The implementation of {ALF}: a proof editor based on
		  {Martin-L\"of's} monomorphic type theory with
		  explicit substitution},
school={Department of Computer Science, Chalmers University},
year={1994}}



@mastersthesis{MS:msc,
Author={M. Marquard and B. Steensgaard},
title={Partial evaluation of an object-oriented language},
school={Department of Computer Science, Copenhagen University (DIKU)},
year={1992}}

@PhdThesis{conor:thesis,
  author = 	"C. McBride",
  title = 	"Dependently typed functional programs and their proofs",
  school = 	"University of Edinburgh",
  year = 	"2000"
}

@phdthesis{aart:thesis,
author={A. Middeldorp},
title={Modular properties of term-rewriting systems},
school={Department of Computer Science, Vrije Universiteit,
		  Amsterdam},
year={1990}}

@phdthesis{miq:thesis,
author={A. Miquel},
title={Le Calcul des Constructions implicite: syntaxe et s{\'e}mantique},
school={Universit{\'e} Paris 11},
year={2001}}


@MASTERSTHESIS{mon:msc,
  author = "Monniaux, D.",
  title = "R{\'e}alisation m{\'e}canis{\'e}e d'interpr{\'e}teurs
abstraits",
  school = "Universit{\'e} Paris VII",
  year = "1998",
  type = "Rapport de {DEA}"}


@book{mul:phd,
 author = {M{\"u}ller, P.},
 title = {Modular Specification and Verification of Object-Oriented Programs},
 publisher = {Springer-Verlag},
 series = lncs,
 volume = {2262},
 year = {2002}
}
 

@PHDTHESIS{chet:thesis
, AUTHOR       = {Murthy, C.}
, TITLE        = {Extracting Constructive Contents from Classical Proofs}
, SCHOOL       = {Cornell University}
, YEAR         = 1990
}
@PhdThesis{nec:thesis,
  author =	"G.C. Necula",
  title =	"Compiling with Proofs",
  school =	"Carnegie Mellon University",
  year = 	"1998",
  month =	oct,
  note = 	"Available as Technical Report CMU-CS-98-154",
}

@PhdThesis{ned:thesis,
author={R. Nederpelt},
title={Strong normalisation in a typed lambda calculus with lambda
		  structured types},
school={Technical University of Eindhoven},
year={1973}}

@PHDTHESIS{nor:thesis,
  AUTHOR  = "J. Nordlander",
  TITLE   = "Reactive Objects and Functional Programming",
  SCHOOL  = "Chalmers Tekniska H{\"o}gskola",
  YEAR    = 1999}

@phdthesis{ohe:thesis,
  author = {Oheimb, D. von},
  title = {Analyzing {J}ava in {Isabelle/HOL}:
    \textit{Formalization, Type Safety and {H}oare Logic}},
  school = {Technische Universit\"{a}t M\"{u}nchen},
  year = 2001,
  note = {\url{http://www4.in.tum.de/~oheimb/diss/}}}

@mastersthesis{oos96:msc,
author={M. Oostdijk},
title={Proofs by calculation},
school={University of Nijmegen},
year={1996}}

@PHDTHESIS{vincent:thesis,
  AUTHOR  = "Oostrom, V. van",
  TITLE   = "Confluence for Abstract and
             Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit Amsterdam",
  YEAR    = 1994}

@PHDTHESIS{christine:thesis
, AUTHOR       = {C. Paulin-Mohring}
, SCHOOL       = {Universit\'{e} Paris VII}
, TITLE        = {Extraction des Programmes dans le Calcul des Constructions}
, YEAR         = 1989
}

@MISC{christine:hdr,
 AUTHOR       = {C. Paulin-Mohring},
 TITLE        = {\emph{D\'efinitions Inductives en Theorie des Types d'Ordre
 Superieur}}, 
 howpublished={Habilitation \`a diriger les recherches,
                     Universit\'e Claude Bernard Lyon I}, 
 YEAR         = 1996
}


@mastersthesis{mariela:dea,
author={M. Pavlova},
title={{Annotation automatique d'applications JavaCard}},
school={Universit\'e Paris 7},
month=jul,
year={2003}}

@PHDTHESIS{henrik:thesis,
  AUTHOR  = "H. Persson",
  TITLE   = "Type Theory and the Integrated Logic of Programs",
  SCHOOL  = "Chalmers Tekniska H{\"o}gskola",
  YEAR    = 1999}

@PHDTHESIS{pet:thesis,
  AUTHOR  = "M. Petersson",
  TITLE   = "Compiling Natural Semantics",
  SCHOOL  = "Link{\"o}ping University",
  YEAR    = 1995}

@phdthesis{pic:thesis,
        author       = "D. Pichardie",
        month        = "December",
        school       = "Universit\'e de Rennes 1",
        title        = "Interpr\'etation abstraite en logique  intuitioniste :
         extraction d'analyseurs Java certifi\'es",
        year         = "2005",
       note =       {\url{http://www-sop.inria.fr/everest/personnel/David.Pichardie/ thesis}}
}

@phdthesis{ple:thesis,
author={Pleyvak, J. },
title={Optimization of Object-Oriented and Concurrent Programs},
year={1996},
school={University of Illinois at Urbana-Champaign}}


@phdthesis{jaco:thesis,
author={Pol, J. van de},
title={Termination of higher-order rewrite systems},
year={1996},
school={University of Utrecht}}

@PhdThesis{randy:thesis,
  author = 	"R. Pollack",
  title = 	"The Theory of {LEGO}: {A} Proof Checker for the Extended
		 Calculus of Constructions",
  school = 	"University of Edinburgh",
  year = 	"1994"
}

@PhDThesis{olivier:thesis,
author={O. Pons},
title="Conception et r{\'e}alisation d'outils d'aide au d{\'e}veloppement de
                  grosses th{\'e}ories dans les syst{\`e}mes de preuves
                  interactifs", 
school={Conservatoire National des Arts et M{\'e}tiers}, 
year=1999}

@PhDThesis{pot:thesis,
author          =       "F. Pottier",
title           =       "Synth{\`e}se de types en pr{\'e}sence de sous-typage:
                  de la th{\'e}orie ā la pratique",  
school          =       "Universit{\'e} Paris VII",
year            =       1998}

@PHDTHESIS{femke:thesis,
  AUTHOR  = "Raamsdonk, F. van",
  TITLE   = "Confluence and Normalisation for 
            Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit Amsterdam",
  YEAR    = 1996}

@PHDTHESIS{rus:thesis,
author={C. Russo},
title={Types For Modules},
school={University of Edinburgh},
year={1998}}

@mastersthesis{mark:msc,
author={M. Ruys},
title={{$\lambda P\omega$ is not conservative over $\lambda P2$}},
school={University of Nijmegen},
year={1991}}


@PhdThesis{schurmann:thesis,
  title =        "{Automating the Meta Theory of Deductive Systems}",
  author =       "C. Sch{\"u}rmann",
 year =         "2000",
  school =       "School of Computer Science, Carnegie Mellon University",
}

@PHDTHESIS{amok:thesis,
  author = {A. Sa{\"\i}bi},
  title = {{Alg{\`e}bre Constructive en Th{\'e}orie des Types,
                  Outils g{\'e}n{\'e}riques pour la mod{\'e}lisation et 
                  la d{\'e}monstration,
                  Application ā la th{\'e}orie des Cat{\'e}gories}},
  school = {Universit{\'e} Paris VI},
  year = {1998}
}


@book{SS:thesis,
author={M. Schmidt-Schau{\ss}},
title={Computational Aspects of Order-Sorted Logic with Term
Declarations},
series=lnai,
publisher=springer,
volume={395}, 
year={1989}}

@phdthesis{see:thesis,
author={R. Seely},
title={Hyperdoctrines and natural deduction},
year={1977},
school={University of Cambridge}}


@MastersThesis{seg:msc,
author={G. S{\'e}gouat},
title={{Preuve en Coq d'une mise en oeuvre de Java Card}},
school={University of Rennes 1},
year={1999}}

@PhdThesis{alex:thesis,
author={A. Sellinx},
title={Computer-aided verification of protocols},
school={University of Utrecht},
year={1996}}


@PhdThesis{paula:thesis,
author={P. Severi},
title={Normalisation in lambda calculus and its relation to type inference},
school={Technical University of Eindhoven},
year={1996}}


@PHDTHESIS{shi:thesis,
	AUTHOR = {O. Shivers},
	TITLE = {Control-Flow Analysis of Higher-Order Languages},
	SCHOOL = {School of Computer Science, Carnegie Mellon University},
	YEAR = 1991,
        MONTH = may,
	NOTE = {Also appears as Technical Report CMU-CS-91-145}
}


@PhDThesis{sim:thesis,
  author =       "M. Simons",
  title =        "The Presentation of Formal Proofs",
  school =       "Technische Universität Berlin",
  year =         1996
                 }


@PhDThesis{slind:thesis,
author={K. Slind},
title={Reasoning about Terminating Functional Programs},
school={TU M{\"u}nich},
year={1999}}

@phdthesis{simao:thesis,
author={Sousa, S. Melo de},
title={Outils et techniques pour la v\'erification formelle de la
plateforme JavaCard},
school={Universit\'e de Nice Sophia-Antipolis},
month=feb,
year={2003}}


@Phdthesis{steffen:thesis,
author={M. Steffen},
title={Polarized Higher-order Subtyping},
school={Department of Computer Science, University of Erlangen},
year={1997}}

@PHDTHESIS{thomas:thesis, 
AUTHOR       = "Th. Streicher", 
TITLE        = "Correctness and Completeness of a Categorical Semantics of the
                Calculus of Constructions", 
SCHOOL       = "University of Passau", 
YEAR         = 1989}

@phdthesis{swa:thesis,
author={M. D. G. Swaen},
title={Weak and strong sum elimination in intuitionistic type theory},
school={Faculty of Mathematics and Computer Science, University of Amsterdam},
year={1989}}


@mastersthesis{sabrina:dea,
author={S. Tarento},
title={Certifying Cryptographic Algoirthms Using the Coq System},
school={Universit\'e de Nice Sophia-Antipolis},
month=jul,
year={2003}}

@phdthesis{tato:thesis,
author={A. Tasistro},
title={Substitution, Record Types and Subtyping in Type Theory,
        with applications to the theory of programming},
school={Department of Computer Science, Chalmers  Tekniska H{\"o}gskola},
year={1997}}




@PhdThesis{delphine:thesis,
  author = 	 {D. Terrasse},
  title = 	 {Vers un environnement d'aide au d{\'e}veloppement de
                  preuves en S{\'e}mantique Naturelle}, 
  school = 	 {Ecole Nationale des Ponts et Chauss{\'e}es},
  year = 	 {1995}}

@PhdThesis{judith:thesis,
  author = 	 {Underwood, J.L.},
  title = 	 {Aspects of the Computational Content of Proofs},
  school = 	 {Department of Computer Science, Cornell University},
  year = 	 1994
}

@phdthesis{werner:thesis,
author={B. Werner},
title={{M\'eta-th\'eorie du Calcul des Constructions Inductives}},
school={Universit{\'e} Paris 7},
year={1994}}

@mastersthesis{wil:msc,
title={Subroutines and Java Bytecode Verification},
author={M. Wildmoser},
year={2002},
school={Technical Univeristy M{\"u}nich}}


@PhDThesis{xi:thesis,
author          =       "H. Xi",
title           =       "Dependent types in practical programming",  
school          =       "Department of Computer Science,
                  Carnegie-Mellon University",  
year            =       1998}


@PhDThesis{yu:thesis,
author          =       "S.-W. Yu",
title           =       "Verification of Concurrent Programs Based on
                  Type Theory",    
school          =       "Department of Computer Science,
                 Durham University",  
year            =       1999}

@PhdThesis{zan:phd,
author ={D. Zanardini},
title = {Certified Abstract Non-Interference: Object-Oriented Code Validation for Information Flow Security},
school = {Universit\`a di Verona},
year = 2006,
month = apr,
}

%%%%%%%%%%%%%%%%%%%%%% STAGES %%%%%%%%%%%%%%%%%%%%%%%%

@Misc{bon97:mag,
Author={D. Bonniot},
title={Rapport de stage de magist{\`e}re},
year={1997}} 



@Misc{let98:stage,
Author={P. Letouzey},
title={A certified of {S}t{\aa}lmarck's algorithm},
year={1998},
howpublished = {Rapport de Stage effectu{\'e} {\`a} l'INRIA Sophia-Antipolis}}




%%%%%%%%%%%%%%%%%%% OUTDATED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@MastersThesis{gustavo:msc,
Author={G. Betarte},
title={A machine-assisted proof that the integers form an integral
		  domain},
school={Department of Computer Science, Chalmers University},
year={1993}}