@misc{BN06:unpublished,
title="A Logical Account of Secure Declassification",
author="A. Banerjee and D. Naumann",
year="2006"}

@Misc{mobius:d11,
  author = 	 {Mobius project},
  title = 	 {Resource and information flow security requirements},
  year = 	 {2006},
  note = 	 {Available from \verb!http://mobius.inria.fr!},
}

@unpublished{BR06:cbt,
title="Constraint based termination",
author="F. Blanqui and C. Riba",
note="Manuscript",
year=2006}


@unpublished{santiago:gp,
author={S.~Zanella B\'eguelin},
title={{Formalisation and Verification of the GlobalPlatform Card Specification
Using the B Method}},
note={Manuscript},
year={2005}}


@inproceedings{floy67,
title="Assigning meanings to programs",
author="R.W. Floyd",
booktitle="Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics",
publisher="American Mathematical Society",
year=1967, 
pages={19-32}}

@unpublished{jive,
 author = {Meyer, J. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
 title = {The {\sc Jive} System---Implementation Description},
 note = {Available from \texttt{sct.inf.ethz.ch/publications}},
 year = {2000}
}
 


@InProceedings{DG02:wiess,
    author =    {D. Deville and G. Grimaud},
    title =     {{Building an ``impossible'' verifier on a Java Card}},
    booktitle = {{Proceedings of WIESS'02}},
    year =      {2002},
   publisher={Usenix Association}
}

@unpublished{DM05:ftfjp,
 author = {Darvas, A. and M\"uller, P.},
 title = {Reasoning {A}bout {M}ethod {C}alls in {JML} {S}pecifications},
 note = {Manuscript},
 year = {2005}
}

@unpublished{VDHP00:load-store,
title={Reducing loads and stores in stack architectures},
author={T. VanDrunen and A.L. Hosking and J. Palsberg},
note={Manuscript},
year={2000}}

@unpublished{rin99:credible,
title={Credible compilation},
author={M. Rinard},
note={Manuscript},
year={1999}}

@unpublished{JPW05:wits,
author={B. Jacobs and W. Pieters and M. Warnier},
title={Statically checking confidentiality via dynamic labels},
booktitle={Proceedings of {WITS}'05},
year={2005},
note={To appear}}


@inproceedings{PB06:sac,
title={Annotation Carrying Code},
author={L. Burdy and M. Pavlova},
booktitle={Proceedings of SAC'06},
year={2006},
publisher="ACM Press"}

@unpublished{ben04:logic,
title={A Typed Logic for Stacks and Jumps},
author={N. Benton},
note={Manuscript},
year={2004}}


@inproceedings{zwa04:plid,
author={S. Zwandewic},
title={Challenges in information flow security},
booktitle={Informal proceedings of {PLID}'04},
year={2004},
editor={R. Giacobazzi and I. Maestroni}}

@inproceedings{KM04:plid,
author={B. K\"opf and H. Mantel},
title={{Eliminating Timing leaks by Unification}},
booktitle={Informal proceedings of {PLID}'04},
year={2004},
editor={R. Giacobazzi and I. Maestroni}}

@article{ned89:mizar,
title={$\sigma$-Fields and Probability},
author={A. Nedzusiak},
journal={Journal of Formalized Mathematics},
volume=1,
year=1989}

@misc{bro:ecdsa,
author={D. Brown},
title={{Generic Groups, Collision Resistance, and ECDSA}},
year={2002},
note={Available from {\tt http://eprint.iacr.org/2002/026/}}}

@incollection{sma:ecies,
author={N. Smart}, 
title="{The Exact Security of ECIES in the Generic Group Model}",
year={2001},
pages={73--84},
booktitle={Cryptography and Coding},
publisher=springer,
editor={B. Honary}}

@inproceedings{DMT00:discex,
author = {Denker, G. and Meseguer, J. and Talcott, C.},
title = {Formal Specification and Analysis of Active Networks and
          Communication Protocols: The Maude Experience},
booktitle = {DARPA Information Survivability Conference and Exposition 
             (DISCEX 2000)},
year = 2000,
publisher = {{IEEE}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%     White Papers                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



@Misc{sc2010, 
  author={European Commission Information Society Directorate General},
  title = 	 {Research for the Smart Card of 2010},
  year = 	 {2001},
  note = 	 {Available from {\tt ftp://ftp.cordis.lu/pub/ist/docs/ka2/}}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%     JCWS                                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{key,
  author        = {W. Ahrendt and T. Baar and B.  Beckert and M.
                  Giese and E. Habermalz and R. Hähnle and W. Menzel and P. H.
              Schmitt},
  title         = {{The Key approach: integrating design and formal
                  verification of Java Card programs}},
 booktitle ={Proceedings of the Java Card Workshop, co-located with
                  the Java Card Forum, Cannes, France},
year={2000}}


@Inproceedings{raj,
author={R. Goré and  L. Nguyen},
title={{CardKt: Automated Logical Deduction on Java Cards}},
booktitle ={Proceedings of the Java Card Workshop, co-located with
                  the Java Card Forum, Cannes, France},
year={2000}} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%     FTFJP                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@InProceedings{bec00:ftfjp,
  author        = {B. Beckert},
  title         = {A Dynamic Logic for Java Card},
  booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {2000},
        publisher = {Fernuniversit{\"at} Hagen},
        editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs,
                  B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        organization = {Technical Report 269, 5/2000,
                  Fernuniversit{\"at} Hagen}}

@inproceedings{bri00:ftfjp,
        author = {Brisset, P.},
        title = {{A Case Study In Java Software Verification:
                  SecurityManager.checkConnect()}},   
        booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {2000},
        publisher = {Fernuniversit{\"at} Hagen},
        editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs,
                  B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        organization = {Technical Report 269, 5/2000,
                  Fernuniversit{\"at} Hagen}} 


@inproceedings{CL99:ftfjp,
        author = {L. Casset and J.-L. Lanet},
        title={{A Formal Specification of the Java Byte Code
Semantics using the B Method}},
        booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {1999},
       
        editor = {Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        publisher= {Technical Report 251,
                  Fernuniversit{\"at} Hagen}} 


@inproceedings{CGQ98:fuj,
title={{Towards a Provably-Correct Implementation of the JVM Bytecode
                  Verifier}},  
author={A. Coglio and A. Goldberg and Z. Qian},
booktitle={Formal Underpinnings of Java Workshop at OOPSLA},
year={1998}}

@inproceedings{cog02:ftfjp,
author={A. Coglio},
title={{Simple Verification Technique for Complex Java Bytecode Subroutines}},
booktitle={Proceedings of {FTFJP}'02},
year=2002}

@inproceedings{fre98:fuj,
title={{The Costs and Benefits of Java Bytecode Subroutines}},
author={S. N. Freund},
booktitle={Formal Underpinnings of Java Workshop at OOPSLA},
year={1998}}


@InProceedings{KN00:ftfjp,
  author        = {G. Klein and T. Nipkow},
  title         = {Lightweight ByteCode Verification},
  booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {2000},
        publisher = {Fernuniversit{\"at} Hagen},
        editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs,
                  B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        organization = {Technical Report 269, 5/2000,
                  Fernuniversit{\"at} Hagen}}

@inproceedings{LSS99:ftfjp,
        author = {K. R. M. Leino and J. B. Saxe and R. Stata},
        title={{Checking Java programs via guarded
       commands}},
        booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {1999},
        publisher = {Fernuniversit{\"at} Hagen},
        editor = {Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        organization = {Technical Report 251, 1999,
                  Fernuniversit{\"at} Hagen}} 


@InProceedings{MPH01:ftfjp,
  author =       {M\"{u}ller, P. and Poetzsch-Heffter, A.},
  title =        {A Type System for Checking Applet Isolation in
                  {J}ava {C}ard},  
  booktitle =    {Proceedings of Formal Techniques for {J}ava Programs},
  year =         2001,
editor={S. Drossopoulou}}


@inproceedings{vO00:ftfjp,
        author = {Oheimb, D. von},
        title = {Axiomatic Semantics for {J}ava$^{\ell{}ight}$ in
                  {Isabelle/HOL}},  
        booktitle = {Proceedings of Formal Techniques for {J}ava Programs},
        year = {2000},
        publisher = {Fernuniversit{\"at} Hagen},
        editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs,
                  B. and Leavens, G. T. and M{\"u}ller, P. and
                  Poetzsch-Heffter, A.}, 
        organization = {Technical Report 269, 5/2000,
                  Fernuniversit{\"at} Hagen}} 

@InProceedings{RR98:fuj,
  author =       "E. Rose and K. H. Rose",
  title =        "Lightweight Bytecode Verification",
  
  year =         "1998",
  booktitle =    "Workshop ``Formal Underpinnings of the Java
                 Paradigm'', {OOPSLA'98}",
  month =        oct}

@InProceedings{str+01:ftfjp,
title={{Formal Models of Java at the JVM Level
       A Survey from the ACL2 Perspective}},
author={J. Strother Moore and R. Krug and H. Liu and G. Porter},
 booktitle ={Proceedings of Formal Techniques for {J}ava Programs},
  year =         2001,
editor={S. Drossopoulou}}










%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%      LFM + DTP + TYPES                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@INPROCEEDINGS{AN00:lfm,
        AUTHOR = {C. Alvarado and Q-H. Nguyen},
        TITLE = {{\sc elan} for equational reasoning in {\sc coq}},
        BOOKTITLE= {Proceedings of LFM'00},
        YEAR = {2000},
        EDITOR = {Despeyroux,J.},                                 
        note = {Rapport Technique INRIA}}

@inproceedings{AC99:dtp,
  author = 	 {L. Augustsson and M. Carlsson},
  title = 	 {An exercise in dependent types: A well-typed interpreter},
  year = 	 {1999},
  booktitle=     {Informal Proceedings of DTP'99}
}

@inproceedings{ct99:lfm,
author={C. Coquand and T. Coquand},
title={{Structured Type Theory}},
year = 	 {1999},
booktitle={{Proceedings of LFM'99 (held in
                  conjunction with PLI'99)}},
url={http://www.cs.bell-labs.com/~felty/LFM99/index.html}}


@inproceedings{HP99:lfm,
  author=        {R. Harper and F. Pfenning},
  title = 	 {{On Equivalence and Canonical Forms in the LF Type Theory}},
  year = 	 {1999},
  booktitle=     {Proceedings of LFM'99 (held in
                  conjunction with PLI'99)},
url={http://www.cs.bell-labs.com/~felty/LFM99/index.html}
}

@inproceedings{nor00:dtp,
  author=        {J. Nordlander},
  title = 	 {{Polymorphic Subtyping in o'Haskell}},
  year = 	 {2000},
  booktitle=     {Proceedings of DTP'00},
note={Available from http://www-sop.inria.fr/oasis/DTP00/Proceedings}}

@unpublished{erik97:sub,
title={Subtyping and Inheritance for Inductive Types},
author={E. Poll},
note={Informal proceedings of the TYPES workshop on subtyping, inheritance
                  and modular development of proofs}, 
year={1997}} 


@inproceedings{randy90:types,
  author = 	 {R. Pollack},
  title = 	 {Implicit Syntax},
  booktitle = 	{{Informal proceedings of the Workshop on Logical Frameworks}},
  year = 	 {1990}}








%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%      JFLA         + GDR                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@inproceedings{DDCW97:gdr,
author={D. Delahaye and R. di Cosmo and B. Werner},
title = {Recherche dans une bibliothèque de
preuves {Coq} en utilisant le type et modulo isomorphismes},
booktitle = {{Proceedings of the PRC/GDR de programmation, P{\^o}le Preuves
                  et S{\'e}cifications Alg{\'e}briques}},  
  year = {1997},
  month = {November}}

@inproceedings{MB01:jfla,
author={N. Magaud and Y. Bertot},
title={Changements de repr{\'e}sentation des structures de donn{\'e}es dans
                  {Coq}: le cas des entiers naturels},
year = 	 {2001},
booktitle={Proceedings of JFLA'01},
editor={P. Casteran}}

@inproceedings{BB02:jfla,
author={A. Balaa and Y. Bertot},
title={Fonctions récursives générales par itération en théorie des types},
year = 	 {2002},
booktitle={Proceedings of JFLA'02},
editor={L. Rideau}}

@inproceedings{HS03:jfla,
author={L. Henrio and B. Serpette},
title={A Parameterized Polyvariant Bytecode Verifier},
year = 	 {2003},
booktitle={Proceedings of JFLA'03},
editor={J.-C. Filliatre}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%      TPHOLS B                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@inproceedings{loic01:tpholsb,
author={L. Pottier},
title={{Quotients in the CIC}},
booktitle={Supplementary proceedings of TPHOLS'01},
publisher={University of Edinburgh},
year={2001},
editor={R. Boulton and P. B. Jackson}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%      Workshops                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@inproceedings{MBC04:fcs,
author={A. Almeida Matos and G. Boudol and I. Castellani},
title={Typing noninterference for reactive programs},
editor={A. Sabelfeld},
booktitle={Proceedings of {FCS}'04},
year={2004}}

@inproceedings{BCGLL02:esmart,
author={G. Betarte and B. Chetali and E. Gim{\'e}nez and C. Loiseaux
and O. Ly},
title={{Formal Modeling and Verification of the Java Card Security Architecture: from Static Checkings to Embedded Applet Execution}},
booktitle={Proceedings of {ESMART}'02},
year={2002}}

@inproceedings{DHS03:wits,
author={A. Darvas and R. H{\"a}hnle and D. Sands},
title={A Theorem Proving Approach to Analysis of Secure Information Flow},
booktitle={Informal proceedings of WITS'03},
year={2003}}

@inproceedings{gem+:res,
title={Contr{\^o}le des ressources dans les cartes {\`a} microprocesseur},
booktitle={Proceedings of LTRE'02},
author={A. Galland and D. Deville and G. Grimaud and B. Folliot},
year={2002}}

@inproceedings{sal,
title={An Overview of {SAL}},
author={S. Bensalem and V. Ganesh and Y. Lakhnech and C.
       Muñoz and S. Owre and H. Rueß and J. Rushby and V. Rusu and
                  H. Saïdi and N. Shankar and E. Singerman and
                  A. Tiwari},
year={2000},
booktitle={Proceedings of NASA's Workshop on Formal Methods}}

@InProceedings{herman+01:calculemus,
  author =       {H.~Geuvers and R.~Pollack and F.~Wiedijk and
                  J.~Zwanenburg},
  title =        {{The Algebraic hierarchy of the FTA project}},
  institution =  {University of Nijmegen},
  booktitle =         {{Informal Proceedings of CALCULEMUS'01}},
  year={2001}}


@InProceedings{HR92:lprolog,
  author =      "R.W. Hasker and U.S. Reddy",
  title =       "Generalization at Higher Types",
  booktitle =   "Proceedings of the Workshop on the {$\lambda$Prolog}
                  Programming Language",
  editor =      "D.~Miller",
  publisher =   "University of Pennsylvania",
  month =       jul,
  year =        "1992",
  note =        "Available as Technical Report MS-CIS-92-86",
  pages =       "257--271"
}


@InProceedings{req00:fmics,
author={A. Requet},
title={{A B Model for Ensuring Soundness of a Large Subset of the Java
                  Card Virtual Machine}},  
booktitle={Proceedings of FMICS'00},
editor={S. Gnesi and I. Schieferdecker and A. Rennoch},
year={2000},
pages={29--46}}

@inproceedings{bernard92:wsa,
  author = 	 {B. Serpette},
  title = 	 {Approximations d'évaluateurs fonctionnels},
  year = 	 {1992},
  booktitle=     {Proceedings of WSA'92},
  pages={79--90}
}


@InProceedings{XS01:wollic,
title={CPS Transform and Type Derivations for Dependent ML},
author={H. Xi and C. Sch{\"u}rmann},
booktitle={Proceedings of WOLLIC'01},
year={2001}}
                      
 

@inproceedings{XX99:cascon,
author = "H. Xi and S. Xia",
title = {{Towards Array Bound Check Elimination in Java Virtual Machine Language}},
booktitle = "Proceedings of CASCOON'99",
month = "November",
pages = "110--125",
year={1999}}





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             DRAFTS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@article{AC:hbal,
title={Heap-Bound Assembly Language},
author={D. Aspinall and A. Compagnoni}, 
year={2003},
journal=jar,
volume=31, 
number={3-4}, 
pages={261-302}}


@unpublished{thierry98:agda,
author={T. Coquand},
title={Typechecking dependent types},
note={Privately circulated manuscript},
year={1998}}

@unpublished{CPT02:struc,
author={T. Coquand and R. Pollack and M. Takeyama},
title={Modules as dependently typed records},
note={To appear in the proceedings of TLCA'03},
year={2002}}

@unpublished{SA:tml,
title={Typed Machine Language and its Semantics},
author={K. N. Swadi and A. W. Appel}, 
year={2001},
note={Manuscript}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%             TALKS                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@misc{eduardo02:verificard,
author={E. Gim{\'e}nez and O. Ly},
title={Formal Modeling and Verification of the Java Card Security Architecture: from Static Checkings to Embedded Applet Execution},
note={Talk delivered at the Verificard'02 meeting, Marseille, 7-9 January 2002},
year={2002}}


@unpublished{ACR00:i3econc,
  author        = "I. Attali and D. Caromel and M. Russo",
  title         = "{Graphical Visualization of Java Objects, Threads, and
Locks}", 
year={2000},
 note     = "Submitted for publication"
}

@unpublished{BO97,
author={L. Barbosa and J.N. Oliveira},
title={Subtype Polymorphism as Natural Transformation in SETS},
year={1998},
note={Preliminary draft}}



@unpublished{alcino98:logcomp,
author={A. Cunha},
title={Formalizing multi-agent systems in {COQ}},
note={Talk at the LOGCOMP workshop, June 1998},
year={1998}}


@unpublished{DC96:gla,
author={R. Di Cosmo},
title={A brief history of rewriting with extensionality},
note={Presented at the International Summer School on Type
Theory and Term Rewriting, Glasgow},
month={September},
year={1996}}

@unpublished{dro00:dynlink,
title={{Towards an abstract model of Java dynamic linking and verification}},
author={S. Drossopoulou},
note={Manuscript},
year={2000}}

@unpublished{FS99:survey,
author={M. Felleisen and A. Sabry},
title={Continuations in Programming Practice: Introduction and Survey},
note={Manuscript},
year={1999}}

@unpublished{joa97:eta,
author={F. Joachimski},
title={$\eta$-expansion in {G}{\"o}del's {T}, {P}ure {T}ype {S}ystems and
                  calculi with permutative conversions},  
note={Manuscript},
year={1997}}

@unpublished{LW:choice,
author={S. Lacas and B. Werner},
title={Which choices imply the excluded middle?},
note={Manuscript},
year={1999}}

@unpublished{TK98,
author={P. Thiemann and H. Klaeren},
title={What security analysis can do for you or the correctness of a
                  multi-level binding-time analysis}, 
note={Manuscript},
month={June},
year={1998}}

@unpublished{herman:cl,
author={H. Geuvers},
title={Inconsistency of classical logic in type theory},
year={2001},
note={Unpublished note}}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        Manuscripts                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@unpublished{peter93:galois,
author={P. Aczel},
title={{GALOIS}: A theory development project},
year={1993},
note={Unpublished Mansucript}}


@Unpublished{car88:phase,
  author =      "L. Cardelli",
  title =       "Phase distinctions in type theory",
  month =       jan,
  year =        1988,
  note={Unpublished Mansucript}
}

@unpublished{LSZ96:tue,
author={T. Laan and P. Severi and J. Zwanenburg},
title={Pure Type Systems with Parameters},
year={1996},
note={Manuscript}}

@unpublished{ML71,
author={P. Martin-L{\"o}f},
title={A Theory of Types},
year={1971},
month=feb,
note={Technical Report, Stockholm University}}


@unpublished{ML72,
author={P. Martin-L{\"o}f},
title={An Intuitionistic Theory of Types},
note={Unpublished Manuscript},
year={1972}}

@unpublished{milad:exact,
title={{Exact Arithmetic on the Stern-Brocot Tree}},
author={M. Niqui},
note={Manuscript},
year={2003}}

@unpublished{syd96:wm,
author={B. van Sydow},
title={Dependently typed binomial queues},
year={1996},
note={Notes for a talk at the Winterm{\"o}te 1996}}

@unpublished{WZ:partial,
title={First order logic with domain conditions},
author={F. Wiedijk and J. Zwanenburg},
year={2001},
note={Manuscript}}

%%%%%%%%%%%%%% STOPPED HERE %%%%%%%%%%%%%
@unpublished{HNP:sdrc,
author={C. Hankin and H. Nielson and J. Palsberg},
title={Strategic directions for research on programming languages},
year={1996},
note={Position paper for the {ACM} Workshop on strategic directions in
	computing research}}

		  
@unpublished{henk96:glasgow,
author={H. Barendregt},
title={Efficient computations in proof-checking},
year={1996},
note={Talk at the International School on Type Theory and Term
		  Rewriting, Glasgow, September 1996}}


		  
@unpublished{bru96:sdcr,
		  author={K. Bruce},
		  title={Type systems and Programming Languages},
		  note={Position paper for the ACM working group on
		  strategic directions for computing research},
		  year={1996}}
		  
		  
		  
@unpublished{PJM97:tic,
		  author={S. {Peyton Jones} and E. Meijer},
		  title={{\sf Henk}: a typed intermediate language},
		  booktitle={Proceedings of TIC'97}, 
		  year={1997},
                 editor={R. Harper and R. Muller}, 
note={Appeared as Technical Report BCCS-97-03, Computer Science 
Department, Boston College} 
}
		  



@unpublished{con:web,
author={P. Chew and R.L. Constable and  K. Pingali and S. Vavasis and
		  R. Zippel},
title={Collaborative Mathematics Environments (Project Description)},
note={HTML document. Available from
{\tt http://www.cs.cornell.edu/Info/Projects/NuPrl/html/publication.html}},
year={1995}}

@unpublished{PT:web,
author={L. Pottier and L. Thery},
title={Algorithmes de calcul formel},
note={HTML document. Available from
{\tt http://www.inria.fr/safir/WHOSWHO/Loic/Coq/polynomials.html}},
year={1996}}



@unpublished{wer92:cpts,
author={B. Werner},
title={Continuations, Evaluation Styles and Type Systems},
year={1992},
note={Manuscript}}

@unpublished{sal:eta,
author={A. Salvesen},
title={The {Church-Rosser} property for $\beta\eta$-reduction},
year={1991},
note={Manuscript}}

@unpublished{ghe94:sn,
author={G. Ghelli},
title={Termination of system {F}-bounded},
year={1994},
note={Manuscript}}


@Unpublished{pfenning:www,
  author = 	"F.Pfenning",
  title = 	"Logical Frameworks",
  note = 	"World Wide Web, 
{\tt http://www.cs.cmu.edu:8001/afs/cs/user/fp/www/lfs.html}",
  year = 	"1994",
  month = 	"October"
}


@unpublished{peter:classes,
author={P. Aczel},
title={A notion of class for type theory},
year={1995},
note={Note}}

@unpublished{ter:gtss,
author={J. Terlouw},
title={Een nadere bewijstheoretische analyse van {GSTT's}},
note={Manuscript (in Dutch)},
year={1989}}



@unpublished{car90:fomsub,
author={L. Cardelli},
title={Notes about {$F_{\leq}^{\omega}$}},
note={Manuscript, D.E.C},
year={1990}}




@unpublished{samuel,
author={S. Boutin},
title={Implementation of quotient types},
year={1995},
note={Available from the Coq WWW page {\tt http://www.inria.fr/
		  Equipes/COQ-fra.html}}} 

@Misc{bac:rsa,
  author = 	 {J.C.B. Almeida},
  title = 	 {A formalization of {RSA} in {C}oq},
  month = jul,	 
  year = {1999},	
  note ={Available from http://logica.di.uminho.pt/CryptoCoq/index.html} 
}




@unpublished{sch00:entcs,
author={Schmidt, D.A.},
title={Binary relations for abstraction and refinement},
year={1999},
note={Available electronically}} 



@INPROCEEDINGS{PJetal93:haskell,
	BOOKTITLE = {Proceedings of the UK Joint Framework for
          Information Technology (JFIT) Technical Conference}, 
	AUTHOR = {S. {Peyton Jones} and C. Hall and K. Hammond and W. Partain
            and P. Wadler}, 
	TITLE = {The {Glasgow} {Haskell} Compiler: a Technical Overview},
	YEAR = 1993}

@unpublished{mark,
author={M. Ruys},
title={Formalizing algebra in Lego},
year={1996},
note={Lego files}}






@Unpublished{gemplus:certicartes,
  author = 	 {Gemplus Research Labs},
  title = 	 {{Java Card Common Criteria Certification Using Coq}},
  note = 	 {{Technical Report}},
  year = 	 {2001}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%      Strange                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@Booklet{SU:ch,
  AUTHOR       = {S{\o}rensen, M. H. and Urzyczyn, P.},
  YEAR         = {1998},
  TITLE        = {{Lectures on the Curry-Howard Isomorphism}},
  howpublished = {Available as DIKU Rapport 98/14}}

@unpublished{HC97:cofi,
title={The Role of Subsorts in Subsort Declarations and Datatype
                               Declarations},
author={A. Haxthausen and M. Cerioli},
year={1997},
note={Language design note for the Common Framework Initiative (COFI)}}


@incollection{henk96:smc,
author={H. Barendregt},
title={The quest for correctness},
year={1996},
booktitle={Images of SMC research},
pages={39--58},
note={Published by SMC for its 50th Birthday},
publisher={Stichting Mathematisch Centrum}}


@unpublished{coh97:djvm,
  author =       "R. M. Cohen",
  title =        "{Defensive Java Virtual Machine Specification Version
0.5}",
  pages =        "397",
  year =         "1997",
  url =          "http://www.cli.com/software/djvm/index.html",
note={Manuscript}}