@STRING{igpl 	= "Logic Journal of the Interest Group in Pure and Applied Logics"}
@string{lncs = "LNCS"} 


@unpublished{CPT02:struc,
Author =	"Coquand, T. and Pollack, R. and Takeyama, M.",
Title =		"Modules as dependently typed records",
note =		"Manuscript",
Year =		"2002"
} 

@Book{PJ:book,
  author =       "S. {Peyton Jones}",
  title =        "The Implementation of Functional Programming Languages",
  publisher =    "Prentice Hall",
  year =         "1987"
 }

@INPROCEEDINGS{zwa99:tlca,
	AUTHOR = {Zwanenburg, J.},
	TITLE = {Pure Type Systems with Subtyping},
	BOOKTITLE = {Proc. of TLCA},
	YEAR = {1999},
	VOLUME = {1581},
	PUBLISHER = {Springer-Verlag},
	SERIES = lncs,
	OPTEDITOR = {Girard, J.-Y.},
	OPTADDRESS = {L'Aquila (Italy)},
	OPTMONTH = apr
}

@INPROCEEDINGS{FaureKirchner-RTA2002,
	AUTHOR = {Faure, G. and Kirchner, C.},
	TITLE = {Exceptions in the rewriting calculus},
	PAGES = {66--82},
	VOLUME = {2378},
	BOOKTITLE = {Proc. of RTA},
	YEAR = {2002},
	PUBLISHER = {Springer-Verlag},
	SERIES = lncs,
	OPTEDITOR = {Tison, Sophie},
	OPTADDRESS = {Copenhagen},
	OPTMONTH = jul
}


@Techreport {vincent-90,
Author =	"V. van Oostrom",
Title =		"Lambda {C}alculus with {P}atterns",
Type =		"Technical Report",
Number =	"IR-228",
Institution =	"Faculteit der Wiskunde en Informatica, Vrije Universiteit
		Amsterdam",
Year =		"1990"
} 


@INPROCEEDINGS{CirsteaKirchnerLiquoriMATCHING,
   author = {Cirstea, H. and Kirchner, C. and Liquori, L.},
   title  = {{M}atching {P}ower},
   booktitle = {Proc. of RTA},
   OPTeditor = {van Oostrom, Vincent},
   year =   {2001},
   PUBLISHER = "Springer-Verlag",
   series = lncs,
   volume = 2051,
   OPTOPTmonth = {May},
   OPTaddress = {Utrecht, The Netherlands},
   OPTsupport={protheo}
}

@INPROCEEDINGS{CirsteaKirchnerLiquoriCUBE,
	AUTHOR = {Cirstea, H. and Kirchner, C. and Liquori, L.},
	TITLE = {The {R}ho {C}ube},
  	PAGES = {166-180},
	VOLUME = {2030},
	BOOKTITLE = {Proc. of FOSSACS},
	OPTADDRESS = {Genova, Italy},
	OPTEDITOR = {Honsell, Furio},
	OPTOPTMONTH = apr,
        SERIES = lncs,
	YEAR = {2001}
}

@ARTICLE{multisetIST-I-2001,
	AUTHOR = {Cirstea, H. and Kirchner, C.},
	TITLE = {{R}ewriting and {M}ultisets in {R}ho-calculus 
                  and {{\sf ELAN}}},
	JOURNAL = "Romanian Journal of Information, 
                   Science and Technology",
	YEAR = {2001},
	VOLUME = {4},
	NUMBER = {1-2},
	PAGES = {33--48},
	OPTNOTE = {ISSN: 1453-8245}
}

@ARTICLE{AitKaciPodelskiSmolkaTCS94,
	AUTHOR = {Ait-Kaci, H. and Podelski, A. and Smolka, G.},
	TITLE = {A feature constraint system for logic 
                 programming with entailment},
	JOURNAL = {Theoretical Computer Science},
	NUMBER = {1-2},
	PAGES = {263--283},
	VOLUME = {122},
	YEAR = {1994}
}



@BOOK{ASF-BOOK,
	AUTHOR = {van Deursen, A. and Heering, J. and Klint, P.},
	TITLE = {{Language Prototyping}},
	PUBLISHER = {World Scientific},
	YEAR = {1996},
	OPTNOTE = {ISBN 981-02-2732-9}
}



@INCOLLECTION{Bar-92,
	AUTHOR = {Barendregt, H.},
	TITLE = {Lambda {C}alculi with {T}ypes},
	BOOKTITLE = {Handbook of Logic in Computer Science},
	OPTEDITOR = {Abramsky, S. and Gabbai, Dov.M. and 
                     Maibaum, T.S.E.},
	PAGES = {118--310},
	PUBLISHER = {Oxford University Press},
	VOLUME = {II},
	YEAR = {1992}
}


@BOOK{Bar-book,
	AUTHOR = {Barendregt, H.},
	TITLE = {Lambda Calculus: its Syntax and Semantics},
	PUBLISHER = {North Holland},
	YEAR = {1984},
	NOTE = {}
}


@BOOK{Barendregt84,
	AUTHOR = "Barendregt, H. P.",
	TITLE = "The {L}ambda-{C}alculus, its syntax and semantics",
	SERIES = "Studies in Logic and the Foundation of Mathematics",
	PUBLISHER = {North Holland},
	OPTADDRESS = "Amsterdam",
	YEAR = 1984,
	NOTE = "Second edition"
}

@TECHREPORT{Berardi-88,
	AUTHOR = {Berardi, S.},
	TITLE = {Towards a {M}athematical {A}nalysis of {T}ype 
                 {D}ependence in {C}oquand--{H}uet {C}alculus of 
                 {C}onstructions and the {O}ther {S}ystems in 
                 {B}arendregt's {C}ube},
	INSTITUTION = {Dept. of Computer Science, 
                       Carnegie Mellon University, and
                       Dip. di Matematica, Universit\'a di Torino},
	OPTMONTH = {},
	YEAR = {1988},
	NOTE = {}
}



@PHDTHESIS{Berardi-phd,
	AUTHOR = {Berardi, S.},
	TITLE = {Type {D}ependence and {C}onstructive {C}athematics},
	SCHOOL = {Dipartimento di Matematica, Universit\'a di Torino},
	YEAR = {1990}
}



@INPROCEEDINGS{Breazu-TannenLICS88,
	AUTHOR = {Breazu-Tannen, V.},
	TITLE = {Combining algebra and higher-order types},
	BOOKTITLE = {Proc. of LICS},
	PAGES = {82--90},
	YEAR = {1988}
}
 


@ARTICLE{Burckert-JSC-88,
	AUTHOR = {B{\"u}rckert, H.-J.},
	TITLE = {Matching--{A} {S}pecial {C}ase of {U}nification?},
	JOURNAL = {Journal of Symbolic Computation},
	NUMBER = {5},
	PAGES = {523--536},
	VOLUME = {8},
	YEAR = {1989}
}
 

@ARTICLE{Church-41,
	AUTHOR = {Church, A.},
	TITLE = {A {F}ormulation of the {S}imple {T}heory of {T}ypes},
	JOURNAL = {Journal of Symbolic Logic},
	OPTOPTMONTH = {},
	NUMBER = {},
	PAGES = {56--68},
	VOLUME = {5},
	YEAR = {1941},
	NOTE = {}
}



@ARTICLE{CH-88,
	AUTHOR = {T. Coquand and G. Huet},
	TITLE = {The {C}alculus of {C}onstructions},
	JOURNAL = {Information and Computation},
	OPTMONTH = {},
	NUMBER = {2/3},
	PAGES = {95--120},
	VOLUME = {76},
	YEAR = {1988}
}



@MISC{Colson88,
	AUTHOR = {Colson, L.},
	TITLE = {Une structure de donn�s pour le 
                 $\lambda$-calcul typ{\'e}},
	HOWPUBLISHED = {Private Communication},
	YEAR = {1988}
}


@INCOLLECTION{Coquand-90,
	AUTHOR = {Coquand, T.},
	TITLE = {Metamathematical {I}nvestigations of a 
                {C}alculus of {C}onstructions},
	BOOKTITLE = {Logic and Computer Science},
	OPTEDITOR = {P. Odifreddi},
	PAGES = {91--122},
	PUBLISHER = {Academic Press},
	YEAR = {1991}
}  

@INPROCEEDINGS{CirsteaKirchnerWRLA2000,
	AUTHOR = {Cirstea, H. and Kirchner, C.},
	TITLE = {The {T}yped {R}ewriting {C}alculus},
	BOOKTITLE = {Third International Workshop on 
                     Rewriting Logic and Application},
	OPTADDRESS = {Kanazawa (Japan)},
	OPTOPTMONTH = {September},
	YEAR = {2000}
}

@TECHREPORT{CirsteaKirchnerINRIA99,
	AUTHOR = {Cirstea, H. and Kirchner, C.},
	TITLE = {{A}n {I}ntroduction to the {R}ewriting {C}alculus},
	INSTITUTION = {INRIA},
	NUMBER = {RR-3818},
	TYPE = {Research Report},
	YEAR = {1999}
}

@INCOLLECTION{CirsteaKirchner-LivreFroCoS99,
	AUTHOR = {Cirstea, H. and Kirchner, C.},
	TITLE = {{C}ombining {H}igher-{O}rder and {F}irst-{O}rder 
                 {C}omputation {U}sing $\rho$-calculus: 
                 {T}owards a {S}emantics of {{\sf ELAN}}},
	BOOKTITLE = {Frontiers of Combining Systems 2},
	PAGES = {95--120},
	PUBLISHER = {Wiley},
	YEAR = {1999}
}


 
 


@ARTICLE{rhoCalIGLP-I+II-2001, AUTHOR = {Cirstea, H. and Kirchner,
C.}, TITLE = {The rewriting calculus --- {Part~I {\em and} II}},
JOURNAL = {Logic Journal of the Interest Group in Pure and Applied
Logics}, OPTOPTMONTH = {May}, NUMBER = {3}, PAGES = {427--498}, VOLUME =
{9}, YEAR = {2001} }

 
 

@PHDTHESIS{CirsteaThese2000,
	AUTHOR = {Cirstea, H.},
	TITLE = {Calcul de {R}\'e\'ecriture~: 
                 {F}ondements et {A}pplications},
	SCHOOL = {Universit\'e Henri Poincar\'e - Nancy I},
	TYPE = {{T}h\`ese de {D}octorat d'{U}niversit\'e},
	YEAR = {2000}
}
 

@ARTICLE{CurienHardinLevy-JACM96,
	AUTHOR = {Curien, P.-L. and Hardin, Th. and L{\'e}vy, J.-J.},
	TITLE = {Confluence properties of weak and 
                 strong calculi of explicit substitutions},
	JOURNAL = jacm,
	VOLUME = 43,
	NUMBER = 2,
        PAGES = {362--397},
	YEAR = 1996
}

@INCOLLECTION{db-80,
	AUTHOR = {N. G. de Bruijn},
	TITLE = {{A} {S}urvey of the {P}roject {AUTOMATH}},
	BOOKTITLE = {To H. B. Curry: Essays in Combinatory Logic, 
                     Lambda Calculus, and Formalism},
	EDITOR = {J. P. Seldin and J. R. Hindley},
	PAGES = {589--606},
	PUBLISHER = {Academic Press},
	YEAR = {1980}
}

 

@ARTICLE{DowekFiltrage,
	AUTHOR = {Dowek, G.},
	TITLE = {Third Order Matching is Decidable},
	JOURNAL = {Annals of Pure and Applied Logic},
	PAGES = {135--155},
	VOLUME = {69},
	YEAR = {1994}
}


@TECHREPORT{DHK-ENAR-98,
	AUTHOR = {Dowek, G. and Hardin, T. and Kirchner,
                  C.},
	TITLE = {Theorem Proving Modulo},
	INSTITUTION = {INRIA},
	OPTMONTH = {April},
	NUMBER = {3400},
	TYPE = {Rapport de Recherche},
	YEAR = {1998},
	note = {\verb|ftp://ftp.inria.fr/INRIA/publication/RR/RR-3400.ps.gz|}
}

@INPROCEEDINGS{ELAN-wrla98,
	AUTHOR = {Borovansk\'y, P. and Kirchner, C. and Kirchner,
        H. and Moreau, P.-E.  and Ringeissen, C.},
	TITLE = {An Overview of \mbox{{\sf {ELAN}}}},
	BOOKTITLE = {Proc. of WRLA},
	PUBLISHER = {Electronic Notes in Theoretical Computer Science},
	VOLUME = {15},
	YEAR = {1998}
}



@MISC{elan,
	AUTHOR = {\'Equipe {P}rotheo},
	TITLE = {The {E}lan {H}ome {P}age},
	INSTITUTION = {LORIA \& INRIA},
	YEAR = {2001},
	OPTNOTE = {\url{http://elan.loria.fr}}
}





@INPROCEEDINGS{FutatsugiN-IEEE97,
	AUTHOR = {Futatsugi, K. and Nakagawa, A.},
	TITLE = {An overview of {CAFE} specification environment -- 
                 An algebraic approach for creating, verifying, and 
                 maintaining formal specifications over networks},
	BOOKTITLE = {Proc. of FEM},
	YEAR = {1997}
}





@INPROCEEDINGS{GallierBreazu,
	AUTHOR = {Gallier, J. and Breazu-Tannen, V.},
	TITLE = {Polymorphic Rewriting Conserves Algebraic 
                 Strong Normalization and Confluence},
	BOOKTITLE = {Proc. of ICALP},
	PAGES = {137--150},
	PUBLISHER = {Springer-Verlag},
	SERIES = {LNCS},
	VOLUME = {372},
	YEAR = {1989}
}


@ARTICLE{Girard-86,
	AUTHOR = {Girard, J.Y.},
	TITLE = {The {S}ystem {F} of {V}ariable {T}ypes, 
                 {F}ifteen {Y}ears {L}ater},
	JOURNAL = {Theoretical Computer Science},
	OPTMONTH = {},
	NUMBER = {},
	PAGES = {159--192},
	VOLUME = {45},
	YEAR = {1986},
	NOTE = {}
}



@PHDTHESIS{Girard-72,
	AUTHOR = {Girard, J.Y.},
	TITLE = {Interpretation {F}onctionnelle et 
                 \'{E}limination des {C}oupures dans
                 l'{A}rithm\'etique d'{O}rdre {S}up\'erieur},
	SCHOOL = {Universit\'e Paris VII},
	YEAR = {1972}
}


@ARTICLE{GN-91,
	AUTHOR = {H. Geuvers and M.J. Nederhof},
	TITLE = {A {M}odular {P}roof of {S}trong {N}ormalization 
                 for the {C}alculus of {C}onstructions},
	JOURNAL = {Journal of Functional Programming},
	OPTOPTMONTH = {April},
	NUMBER = {2},
	PAGES = {155--189},
	VOLUME = {1},
	YEAR = {1991}
}  

@MISC{KirchnerKirchner-RSP-99,
	AUTHOR = {Kirchner, C. and Kirchner, H.},
	TITLE = {Rewriting, {S}olving, {P}roving},
	HOWPUBLISHED = {A preliminary version of a book available at
                        \verb|www.loria.fr/~ckirchne/rsp.ps.gz|},
	YEAR = {1999}
}



     

@INCOLLECTION{KirchnerKV-MIT95,
	AUTHOR = {Kirchner, C. and Kirchner, H. and Vittek, M.},
	TITLE = {Designing Constraint Logic Programming Languages 
                 using Computational Systems},
	BOOKTITLE = {Principles and Practice of Constraint 
                     Programming. The Newport Papers.},
	CHAPTER = {8},
	PAGES = {131--158},
	PUBLISHER = {The MIT press},
	YEAR = {1995}
}

@ARTICLE{HoffmannOD-82b,
	AUTHOR = {Hoffmann, C. M. and O'Donnell, M. J.},
	TITLE = {Pattern Matching in Trees},
	JOURNAL = {Journal of the {ACM}},
	NUMBER = {1},
	PAGES = {68--95},
	VOLUME = {29},
	YEAR = {1982}
}


@ARTICLE{KN-96,
	AUTHOR = {F. Kamareddine and R. Nederpelt},
	TITLE = {Canonical {T}yping and $\Pi$-conversion 
                 in the $\lambda$-cube},
	JOURNAL = {Journal of  Functional Programming},
	OPTMONTH = {},
	NUMBER = {2},
	PAGES = {85--109},
	VOLUME = {6},
	YEAR = {1996}
}

@ARTICLE{KBN-00,
	AUTHOR = {F. Kamareddine and R. Bloo and R. Nederpelt},
	TITLE = {On $\Pi$-conversion on the $\lambda$-cube and the 
                {C}ombination with {A}bbreviations},
	JOURNAL = {Annals of Pure and Applied Logics},
	OPTMONTH = {},
	NUMBER = {1-3},
	PAGES = {27--45},
	VOLUME = {97},
	YEAR = {1999}
}

@ARTICLE{KL-01,
	AUTHOR = {F. Kamareddine and T. Laan},
	TITLE = {A {C}orrespondence between {Martin-L\"of} 
                {T}ype {T}heory, the {R}amified {T}heory of  
                {T}ypes and {P}ure {T}ype {S}ystems},
	JOURNAL = {Journal of  Logic, Language and Information},
	OPTMONTH = {},
	NUMBER = {},
	PAGES = {},
	VOLUME = {},
	YEAR = {2001},
	NOTE = {To appear}
}
 


@ARTICLE{KlopOostromRaamsdonk,
	AUTHOR = {Klop, J.W. and van Oostrom, V. and 
                  van Raamsdonk, F.},
	TITLE = {Combinatory reduction systems: 
                 introduction and survey},
	JOURNAL = {Theoretical Computer Science},
	PAGES = {279--308},
	VOLUME = {121},
	YEAR = {1993}
}




@ARTICLE{KMP77,
	AUTHOR = {Knuth, Donald E. and Morris, J. and Pratt, V.},
	TITLE = {Fast Pattern Matching in Strings},
	JOURNAL = {{SIAM} Journal of Computing},
	NUMBER = {2},
	PAGES = {323--350},
	VOLUME = {6},
	YEAR = {1977}
}

 
@PHDTHESIS{Liquori-Phd,
  AUTHOR = {Liquori, L.},
  TITLE = {Type {A}ssigment {S}ystems for {L}ambda {C}alculi
               and for the {L}ambda {C}alculus of {O}bjects},
  SCHOOL = {University of Turin},
  TYPE = {Ph.D. Thesis, 193 pp.},
  YEAR = {1996},
  OPTMONTH = {October},
  NOTE = {\url{http://www.loria.fr/~lliquori/PAPERS/phd.ps.gz}}
}


@ARTICLE{BLRU-97,
  AUTHOR = {van Bakel, S. and  Liquori, L. and
            {Ronchi della Rocca}, S. and  Urzyczyn, P.},
  TITLE = {Comparing {C}ubes of {T}yped and
            {T}ype {A}ssignment {S}ystem},
  JOURNAL = {Annals of Pure and Applied Logics},
  YEAR = {1997},
  PUBLISHER = {North-Holland},
  VOLUME = {86},
  NUMBER = {3},
  PAGES = {267--303},
  OPTMONTH = {},
  OPTNOTE = {\url{http://www.loria.fr/~lliquori/PAPERS/apal-97.ps.gz}}
}


@INPROCEEDINGS{Luo-89,
	AUTHOR = {Z. Luo},
	TITLE = {{ECC:} {A}n {E}xtended {C}alculus of 
                 {C}onstructions},
	BOOKTITLE = {Proc. of LICS},
	PAGES = {385-395},
	OPTPUBLISHER = {IEEE},
	YEAR = {1990}
}
 


@INPROCEEDINGS{Laville-87,
	AUTHOR = {Laville, A.},
	TITLE = {Lazy Pattern Matching in the {ML} Language},
	BOOKTITLE = {Proc. of FCT \& TCS},
	PAGES = {400--419},
	PUBLISHER = {Springer-Verlag},
	SERIES = {LNCS},
	VOLUME = {287},
	YEAR = {1987}
}


@BOOK{Lof-84,
	AUTHOR = {P. {Martin-L\"of}},
	TITLE = {Intuitionistic {T}ype {T}heory},
	OPTADDRESS = {Naples},
	PUBLISHER = {Bibliopolis},
	SERIES = {Studies in Proof Theory},
	VOLUME = {1},
	YEAR = {1984}
}

@INCOLLECTION{JouannaudKirchner-rob91,
	AUTHOR = {Jouannaud, J.-P. and Kirchner, C.},
	TITLE = {Solving {E}quations in {A}bstract {A}lgebras: 
                 {A} {R}ule-based {S}urvey of {U}nification},
	BOOKTITLE = {Computational {L}ogic. {E}ssays in {H}onor 
                     of {A}lan {R}obinson},
	CHAPTER = {8},
	PAGES = {257--321},
	PUBLISHER = {The MIT press},
	YEAR = {1991}
}
 
@ARTICLE{JouannaudKirchnerSIAM86,
	AUTHOR = {Jouannaud, J.-P. and Kirchner, H.},
	TITLE = {Completion of a {S}et of {R}ules {M}odulo a 
                 {S}et of {E}quations},
	JOURNAL = {{SIAM} Journal of Computing},
	NUMBER = {4},
	PAGES = {1155--1194},
	VOLUME = {15},
	YEAR = {1986},
	OPTNOTE = {Preliminary version in Proc. of POPL'84}
}


@Inproceedings {Jouannaud-Okada'91,
Author =	"J.P. Jouannaud and M. Okada",
Title =		"Executable higher-order algebraic specification languages",
Booktitle =	"Proc. of LICS",
Year =		"1991",
Pages =		"350-361"
}

 
@ARTICLE{TCSJouannaudO1997,
	AUTHOR = {Jouannaud, J.P. and Okada, M.},
	TITLE = {Abstract data type systems},
	JOURNAL = {Theoretical Computer Science},
	OPTOPTMONTH = {28~February},
	NUMBER = {2},
	PAGES = {349--391},
	VOLUME = {173},
	YEAR = {1997}
}



@INPROCEEDINGS{Hullot79,
	AUTHOR = {Hullot, J.-M.},
	TITLE = {{A}ssociative-{C}ommutative {P}attern {M}atching},
	BOOKTITLE = {Proc. of IJCAI},
	YEAR = {1979}
}
 
 
@ARTICLE{HHP-92,
	AUTHOR = {R. Harper and F. Honsell and G. Plotkin},
	TITLE = {A {F}ramework for {D}efining {L}ogics},
	JOURNAL = {Journal of the ACM},
	NUMBER = {1},
	PAGES = {143--184},
	VOLUME = {40},
	YEAR = {1992},
	OPTNOTE = {Preliminary version in proc. of {LICS'87}}
}



@ARTICLE{HuetLang-78,
	AUTHOR = {Huet, G. and Lang, B.},
	TITLE = {Proving And Applying Program Transformations 
                 Expressed With Second-Order Patterns},
	JOURNAL = {Acta Informatica},
	PAGES = {31--55},
	VOLUME = {11},
	YEAR = {1978}
}

@ARTICLE{Masako-92,
	AUTHOR = {M. Takahashi},
	TITLE = {Parallel {R}eductions in $\lambda$-calculus},
	JOURNAL = {Journal of Symbolic Computation},
	PAGES = {113-123},
	VOLUME = {7},
	YEAR = {1989}
}
   
 

@INPROCEEDINGS{Maude-RwLg1996,
	AUTHOR = {Clavel, M. and Eker, S. and Lincoln, P. 
                  and Meseguer, J.},
	TITLE = {Principles of {Maude}},
	BOOKTITLE = {Proc. of WRLA},
	PUBLISHER = {Electronic Notes in Theoretical 
                     Computer Science},
	VOLUME = {4},
	YEAR = {1996}
}
 

@INPROCEEDINGS{MillerLProlog-89-91,
	AUTHOR = {Miller, D.},
	TITLE = {A Logic Programming Language with 
                 Lambda-Abstraction, Function
                 Variables, and Simple Unification},
	BOOKTITLE = {{Proc. of ELP}},
	OPTEDITOR = {Schroeder-Heister, Peter},
	PAGES = {253--281},
	PUBLISHER = {Springer-Verlag},
	SERIES = {LNCS},
	VOLUME = {475},
	YEAR = {1991}
}



@INCOLLECTION{Nipkow-Prehofer-98,
	AUTHOR = {T. Nipkow and C. Prehofer},
	TITLE = {Higher-Order Rewriting and Equational Reasoning},
	BOOKTITLE = {Automated Deduction --- 
                     A Basis for Applications. Volume I: Foundations},
	EDITOR = {W. Bibel and P. Schmitt},
	PUBLISHER = {Kluwer},
	YEAR = {1998}
}

 

@INPROCEEDINGS{obj3-88,
	AUTHOR = {Goguen, J. A. and Kirchner, C. and Kirchner, H. and
        M{\'e}grelis, A. and Meseguer, J. and Winkler, T.},
	TITLE = {An Introduction to {OBJ}-3},
	BOOKTITLE = {Proc. of CTRS},
	PAGES = {258--263},
	PUBLISHER = {Springer-Verlag},
	SERIES = {LNCS},
	VOLUME = {308},
	YEAR = {1987}
}




@INPROCEEDINGS{Okada1989SNC,
	AUTHOR = {Okada, M.},
	TITLE = {Strong normalizability for the combined system 
                 of the typed $\lambda$ calculus and an 
                 arbitrary convergent term rewrite system},
	BOOKTITLE = {Proc. of ISSAC},
	PAGES = {357--363},
	PUBLISHER = {ACM Press},
	YEAR = {1989}
}
 
 

@ARTICLE{Padovani-mscs2000,
	AUTHOR = {Padovani, V.},
	TITLE = {Decidability of fourth-order matching},
	JOURNAL = {Mathematical Structures in Computer Science},
	OPTOPTMONTH = {June},
	NUMBER = {10},
	PAGES = {361--372},
	VOLUME = {3},
	YEAR = {2000}
}


@BOOK{Peyton87,
	AUTHOR = {Peyton-Jones, S.},
	TITLE = {The implementation of functional programming 
                 languages},
	PUBLISHER = {Prentice Hall, Inc.},
	YEAR = {1987}
}




@INPROCEEDINGS{PJM-97,
	AUTHOR = {S.L. {Peyton Jones} and E. Meijer},
	TITLE = {Henk: a {T}yped {I}ntermediate {L}anguage},
	BOOKTITLE = {Types in Compilation Workshop},
	PAGES = {},
	OPTPUBLISHER = {},
	YEAR = {1997}
}

 

@ARTICLE{PS81,
	AUTHOR = {Peterson, G. and Stickel, M. E.},
	TITLE = {Complete Sets of Reductions for Some 
                 Equational Theories},
	JOURNAL = {Journal of the {ACM}},
	PAGES = {233--264},
	VOLUME = {28},
	YEAR = {1981}
}



@article{Plo-75,
        author = "G. Plotkin",
        title ="Call by name, call by value and the $\lambda$-calculus",               journal = "Theoretical {C}omputer {S}cience ",
        year = "1975 ",
        volume= "1",
        pages = " 125--159" 
}                




@UNPUBLISHED{Terlouw-89,
	AUTHOR = {J. Terlouw},
	TITLE = {Een nadere bewijstheoretische analyse van {GSTT}s},
	YEAR = {1989},
	NOTE = {Manuscript, University of Nijmegen, Toernooiveld I, 
                Nijmegen, The Netherlands}
}

  
@INPROCEEDINGS{VB98,
	AUTHOR = {Visser, E. and Benaissa, Z.e.A.},
	TITLE = {A Core Language for Rewriting},
	BOOKTITLE = {Proc. of WRLA},
	PUBLISHER = {Electronic Notes in Theoretical Computer Science},
	VOLUME = {15},
	YEAR = {1998}
}


@INPROCEEDINGS{Viry-RwLg1996,
	AUTHOR	= {Viry, P.},
	TITLE	= {{Input/Output for {{\sf ELAN}}}},
	BOOKTITLE = {Proc. of WRLA},
        PUBLISHER = {Electronic Notes in Theoretical Computer Science},
	VOLUME = {4},
	YEAR	= {1996}
}


@BOOK{WolframLivre,
	AUTHOR = {Wolfram, D. A.},
	TITLE = {The Clausal Theory of Types},
	PUBLISHER = {Cambridge University Press},
	SERIES = {Cambridge Tracts in Theoretical Computer Science},
	VOLUME = {21},
	YEAR = {1993}
}
 

@ARTICLE{YokouchiHikita90,
        AUTHOR = {Yokouchi, H. and Hikita, T.},
	TITLE = {A rewriting system for categorical combinators 
                 with multiple arguments},
	JOURNAL = {{SIAM} Journal of Computing},
	VOLUME = {19},
	NUMBER = {1},
	YEAR = {1990},
	OPTMONTH = feb
}


@BOOK{AC-book,
	AUTHOR = {Abadi, M. and Cardelli, L.},
	TITLE = {A {T}heory of {O}bjects},
	PUBLISHER = {Springer Verlag},
	YEAR = {1996}
}

@ARTICLE{FHM-94,
	AUTHOR = {Fisher, K. and Honsell, F. and Mitchell, J. C.},
	TITLE = {A {L}ambda {C}alculus of {O}bjects and {M}ethod 
                 {S}pecialization},
	JOURNAL = {Nordic Journal of Computing},
	NUMBER = {1},
	PAGES = {3--37},
	VOLUME = {1},
	YEAR = {1994}
}
 
 
@INPROCEEDINGS{DHL-98,
	AUTHOR = {P. Di~Gianantonio and F. Honsell and L. Liquori},
	TITLE = {A {L}ambda {C}alculus of {O}bjects with 
                 {S}elf-inflicted {E}xtension},
	BOOKTITLE = {Proc. of OOPSLA},
	PAGES = {166--178},
	PUBLISHER = {The ACM Press},
	YEAR = {1998}
}


@MISC{duboiskirchner-tcs,
	AUTHOR = {Dubois, H. and Kirchner, H.},
	TITLE = {{Objects, rules and strategies in {\tt ELAN}}},
	HOWPUBLISHED = {Manuscript},
        YEAR = {2001}
}
 

%%%% GILLES

@unpublished{PJM97:tic,
                  author={S. {Peyton Jones} and E. Meijer},
                  title={{\sf Henk}: a typed intermediate language},
                  note={Proceedings of the ACM Workshop on Types in
                  Compilation},
                  year={1997}}


@UNPUBLISHED{Acz:78,
  AUTHOR = "Aczel, Peter",
  TITLE  = "A General {C}hurch-{R}osser Theorem",
  OPTMONTH  = jul,
  YEAR   = "1978",
  NOTE   = "University of Manchester",
}

@INPROCEEDINGS{Aka:93,
  AUTHOR    = "Akama, Y.",
  TITLE     = "On {M}ints' Reduction  for ccc-Calculus",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications 
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "1--12",
  OPTADDRESS   = "Utrecht, The Netherlands",
  OPTMONTH     = mar,
  NOTE      = "Volume 664 of Lecture Notes in Computer Science"
}


@INPROCEEDINGS{Ant:Mid:94,
  AUTHOR    = "Antoy, S. and Middeldorp, A.",
  TITLE     = "A sequential Reduction Strategy",
  BOOKTITLE = "Proceedings of the 4th International
               Conference on Algebraic and Logic Programming
              (ALP '94)",
  YEAR      = 1994,
  PAGES     ="168--185",
  SERIES    = lncs,
  NUMBER    = 850,
  OPTADDRESS   = "Madrid"
}

@ARTICLE{Asp:91,
  AUTHOR   = "Asperti, A.",
  TITLE    = "Linear Logic, Comonads and Optimal Reductions",
  JOURNAL  = "Fundamenta Informaticae",
  YEAR     = 1994,
  VOLUME   = 22,
  PAGES    = "3--22",
  NOTE     = "Special Issue devoted to Categories in 
             Computer Science"
}

@INPROCEEDINGS{Asp:95,
  AUTHOR    = "Asperti, A.",
  TITLE     = "$\delta \ \circ \ ! \epsilon = 1$",
  BOOKTITLE = "Proceedings of the 6th International Conference
              on Rewriting Techniques and Applications
              (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "102--116",
  OPTADDRESS   = "Kaiserslautern, Germany",
  OPTMONTH     = apr,
  SERIES    = lncs,
  NUMBER    = 914
}

@ARTICLE{Asp:Lan:94,
  AUTHOR  = "Asperti, A. and Laneve, C.",
  TITLE   = "Interaction Systems {I}:
            The theory of optimal reductions",
  JOURNAL = mscs,
  YEAR    = 1994,
  VOLUME  = 4,
  PAGES   = "457--504"
}

@ARTICLE{Asp:Lan:96,
  AUTHOR  = "Asperti, A. and Laneve, C.", 
  TITLE   ="Interaction Systems {II}:
            The practice of optimal reductions",
  JOURNAL = tcs,
  YEAR    = 1996,
  OPTMONTH   = jul,
  NOTE    = "To appear."
}

@PHDTHESIS{Bar:71,
  AUTHOR  = "Barendregt, H.P.",
  TITLE   = "Some Extensional Term Models for Combinatory Logics
            and $\lambda$-calculi",
  SCHOOL  = "Rijksuniversiteit Utrecht",
  YEAR    = 1971
}

@ARTICLE{Bar:74,
  AUTHOR  = "Barendregt, H.P.",
  TITLE   = "Pairing without conventional constraints",
  JOURNAL = "Zeitschrift f{\"u}r mathematischen Logik
            und Grundlagen der Mathematik",
  YEAR    = 1974,
  VOLUME  = 20,
  PAGES   = "289--306"
}


@BOOK{Bar:84,
  AUTHOR    = "Barendregt, H.P.",
  TITLE     = "The Lambda Calculus, its Syntax and Semantics",
  PUBLISHER = nh,
  YEAR      = 1984,
  VOLUME    = 103,
  SERIES    = slfm,
  EDITION   = "Revised",
}

@INCOLLECTION{Bar:92,
  AUTHOR    = "Barendregt, H.P.",
  TITLE     = "Lambda calculi with types",
  BOOKTITLE = "Handbook of Logic in Computer Science",
  PUBLISHER = oup,
  YEAR      = 1992,
  EDITOR    = "Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E",
  PAGES     = "117--310",
  OPTADDRESS   = "New  York",
  VOLUME    = 2
}

@TECHREPORT{Bar:Ber:Klo:Vol:76,
  AUTHOR      = "Barendregt, H. and
                Bergstra, J. and
                Klop, J. W. and
                Volken, H.",
  TITLE       = "Degrees, Reductions and Representability in the
                Lambda Calculus",
  INSTITUTION = "University Utrecht",
  NUMBER      = 22,
  YEAR        = 1976,
  OPTMONTH       = feb
}

@ARTICLE{Ber:Klo:86,
  AUTHOR  = "Bergstra, J.A. and Klop, J.W.",
  TITLE   = "Conditional Rewrite Rules: Confluence and Termination",
  JOURNAL = jcss,
  YEAR    = 1986,
  VOLUME  = 32,
  PAGES   = "323--362",
}

@INCOLLECTION{Bou:85,
  AUTHOR    = "Boudol, G.",
  TITLE     = "Computational semantics of term rewriting systems",
  BOOKTITLE = "Algebraic methods in semantics",
  PUBLISHER = cup,
  YEAR      = 1985,
  EDITOR    = "Nivat, Maurice and Reynolds, John C.",
  CHAPTER   = "5",
  PAGES     = "169--236",
}



@ARTICLE{Bre:Gal:90,
  AUTHOR  = "Breazu-Tannen, V. and Gallier, J.",
  TITLE   = "Polymorphic rewriting conserves 
            algebraic strong normalization",
  JOURNAL = tcs,
  YEAR    = 1990,
  VOLUME  = 83,
  PAGES   = "3--28"
}

@ARTICLE{Bre:Gal:94,
  AUTHOR  = "Breazu-Tannen, V. and Gallier, J.",
  TITLE   = "Polymorphic rewriting conserves 
            algebraic confluence",
  JOURNAL = ic,
  VOLUME  = 14,
  NUMBER  = 1,
  PAGES   = "1--29",
  YEAR    = 1994
}

@BOOK{Chu:41,
  AUTHOR     = "Church, A.",
  TITLE      = "The Calculi of Lambda Conversion",
  PUBLISHER  = pup,
  YEAR       = 1941
}

@ARTICLE{Chu:Ros:36,
  AUTHOR  = "Church, A. and Rosser, J.B.",
  TITLE   = "Some properties of conversion",
  JOURNAL = tams,
  YEAR    = 1936,
  VOLUME  = 39,
  PAGES   = "472--482"
}

@ARTICLE{Coq:Hue:88,
  AUTHOR  = "Coquand, Th. and Huet, G.",
  TITLE   = "The calculus of constructions",
  JOURNAL = ic,
  YEAR    = 1988,
  VOLUME  = 76,
  PAGES   = "95--120"
}



@UNPUBLISHED{Cub:93,
  AUTHOR = "{\v C}ubri{\v c}, D.",
  TITLE  = "Embedding of a free cartesian closed category
           into the category of sets",
  YEAR   = 1993,
  NOTE   = "McGill University"
}

@BOOK{Cur:93,
  AUTHOR    = "Curien, P.-L.",
  TITLE     = "Categorical Combinators, Sequential Algorithms,  
              and Functional Programming",
  PUBLISHER = "Birkh{\"a}user",
  YEAR      = 1993,
  OPTADDRESS   = "Boston, USA",
  NOTE      = "Second edition"
}

@TECHREPORT{Cur:95,
  AUTHOR      = "Curien, P.-L.",
  TITLE       = "Alg{\`e}bre Universelle,
                Introduction au $\lambda$-calcul et aux Logiques
                Combinatoires (Notes de Cours)",
  INSTITUTION = "Ecole Normale Sup{\'e}riere",
   NUMBER      = "LIENS-95-30",
  OPTMONTH       = nov,
  YEAR        = 1995
}



@BOOK{Cur:Fey:Cra:58,
  AUTHOR    = "Curry, Haskell B. and Feys, R. and Craig, W.",
  TITLE     = "Combinatory Logic, volume I",
  PUBLISHER = nh,
  YEAR      = 1958,
  SERIES    = slfm,
  OPTADDRESS   = "Amsterdam",
}

@PHDTHESIS{Dan:90,
  AUTHOR  = "Danos, V.",
  TITLE   = "La Logique Lin{\'e}aire appliqu{\'e}e {\`a}
            l'{\'e}tude de divers processus de normalisation
            (principalement du $\lambda$-calcul)",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1990
}

@ARTICLE{Dan:Reg:89,
  AUTHOR  = "Danos, V. and R{\'e}gnier, L.",
  TITLE   = "The structure of multiplicatives",
  JOURNAL = aml,
  YEAR    = 1989,
  VOLUME  = 28,
  PAGES   = "181--203"
}



@article{Miller-Annals,
author   = "D. Miller and G. Nadathur and F. Pfenning and A. Shedrov",
title    = "{U}niform {P}roofs as a {F}oundation for {L}ogic {P}rogramming",
journal  = "Annals of Pure and Applied Logics",
volume   = "51",
year     = 1991,
pages    = "125--157"
}


@INCOLLECTION{Der:Jou:90,
  AUTHOR    = "Dershowitz, N. and Jouannaud, J.-P.",
  TITLE     = "Rewrite Systems",
  BOOKTITLE = "Handbook of Theoretical Computer Science",
  PUBLISHER = esp,
  YEAR      = 1990,
  EDITOR    = "Leeuwen, Jan van",
  CHAPTER   = 6,
  VOLUME    = "B: Formal Models and Semantics",
  PAGES     = "243--320",
  OPTADDRESS   = "Amsterdam",
}

@ARTICLE{DiC:Kes:94,
  AUTHOR  = "Di Cosmo, R. and Kesner, D.",
  TITLE   = "Simulating Expansions Without Expansions",
  JOURNAL = mscs,
  YEAR    = 1994,
  VOLUME  = 4,
  PAGES   = "315--362"
}

@TECHREPORT{Fer:Sev:93,
  AUTHOR      = "Ferrer, Walter and Severi, Paula",
  TITLE       = "Abstract Reduction and Topology",
  INSTITUTION = "Eindhoven University of Technology",
  NUMBER      = "93/35",
  OPTMONTH       = oct,
  YEAR        = 1993
}


@PHDTHESIS{Fie:91,
  AUTHOR  = "Field, John Henry",
  TITLE   = "Incremental Reduction in the Lambda Calculus and
            Related Reduction Systems",
  SCHOOL  = "Cornell University",
  YEAR    = 1991,
  OPTADDRESS = "Ithaca, New York, USA"
}

@INPROCEEDINGS{Fie:93,
  AUTHOR    = "Field, John",
  TITLE     = "A graph reduction approach to 
              incremental term rewriting",
  BOOKTITLE = "Proceedings of the Fifth International Conference
              on Rewriting Techniques and Application (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "259--273",
  OPTADDRESS   = "Montreal, Canada",
  OPTMONTH     = jun,
  SERIES    = lncs,
  NUMBER    = 690
}

@INCOLLECTION{Gan:80,
  AUTHOR    = "Gandy, R.O.",
  TITLE     = "Proofs of Strong Normalization",
  BOOKTITLE = "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus
              and Formalism",
  PUBLISHER = ap,
  YEAR      = 1980,
  EDITOR    = "Seldin, J.P. and Hindley, J.R.",
  PAGES     = "457--477"
}


@INPROCEEDINGS{Gar:94,
  AUTHOR    = "Gardner, Phillipa",
  TITLE     = "Discovering Needed Reductions 
              Using Type Theory",
  BOOKTITLE = "Proceedings of the Second International Symposium
              on Theoretical Aspects of Computer Software (TACS '94)",
  YEAR      = 1994,
  EDITOR    = "Hagiya, Masami and Mitchell, John C.",
  PAGES     = "555--574",
  OPTADDRESS   = "Sendai, Japan",
  OPTMONTH     = apr,
  SERIES    = lncs,
  NUMBER    = 789
}

@INPROCEEDINGS{Ghi:94,
  AUTHOR    = "Ghilezan, Sylvia",
  TITLE     = "Application of Typed Lambda Calculi in the
              Untyped Lambda Calculus",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "129--139",
  OPTADDRESS   = "St. Petersburg, Russia",
  OPTMONTH     = jul,
  SERIES    = lncs,
  VOLUME    = 813
}


@PHDTHESIS{Gir:72,
  AUTHOR  = "Girard, Jean-Yves",
  TITLE   = "Interpr{\'e}tation fonctionelle et {\'e}limination 
            des coupures dans l'arithm{\'e}tique d'ordre sup{\'e}rieur",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1972
}


@ARTICLE{Gir:87,
  AUTHOR  = "Girard, Jean-Yves",
  TITLE   = "Linear Logic",
  JOURNAL = tcs,
  YEAR    = 1987,
  VOLUME  = 50,
  PAGES   = "1--102"
}

@BOOK{Gir:Laf:Tay:89,
  AUTHOR    = "Girard, Jean-Yves and Lafont, Yves and Taylor, Paul",
  TITLE     = "Proofs and Types",
  PUBLISHER = cup,
  YEAR      = 1989,
  VOLUME    = 7,
  SERIES    = cttcs
}

@INPROCEEDINGS{Gla:Kha:94,
  AUTHOR    = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE     = "Relative Normalization in Orthogonal Expression Reduction Systems",
  BOOKTITLE = "Proceedings of the 4th International Workshop on Conditional and
              Typed Term Rewriting Systems (CTRS '94)",
  YEAR      = 1994,
  EDITOR    = "Dershowitz, N.",
  PAGES     = "144-165",
  OPTADDRESS   = "Jerusalem, Israel",
  SERIES    = lncs,
  VOLUME    = 968
}

@INPROCEEDINGS{Gla:Kha:96a,
  AUTHOR    = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE     = "Relative Normalization in Deterministic Residual Structures",
  BOOKTITLE = "Proceedings of the 19th International Colloquium on
              Trees in Algebras and Programming (CAAP '96)",
  OPTMONTH     = apr,
  YEAR      = 1996,
  ADDRES    = "Link{\"o}ping, Sweden",
  NOTE      = "To appear"
}

@UNPUBLISHED{Gla:Kha:96b,
  AUTHOR = "Glauert, J.R.W. and Khasidashvili, Z.",
  TITLE  = "Minimal and Optimal Relative Normalization in 
           Orthogonal Expression Reduction Systems",
  YEAR   = 1996,
  NOTE   = "University of East Anglia"
}

@INPROCEEDINGS{Gon:Aba:Lev:92,
  AUTHOR    = "Gonthier, Georges and Abadi, Mart{\'\i}n and
              L{\'e}vy, Jean-Jacques ",
  TITLE     = "The geometry of optimal lambda reduction",
  BOOKTITLE = "Proceedings  of the 19th ACM
               Conference on Principles of
               Programming Languages (POPL '92)",
  YEAR      = 1992,
  PAGES     = "15--26"
}

@INPROCEEDINGS{Gon:Lev:Mel:92,
  AUTHOR    = "Gonthier, Georges and L{\'e}vy, Jean-Jacques and
              Melli{\`e}s, Paul-Andr{\'e}",
  TITLE     = "An abstract standardisation theorem",
  BOOKTITLE = "Proceedings of the seventh Annual IEEE Symposium on
              Logic in Computer Science (LICS '92)",
  PAGES     = "72--81",
  YEAR      = 1992,
  OPTADDRESS   = "Los Alamitos, California"
}

@INPROCEEDINGS{Gro:93,
  AUTHOR    = "Groote, Philippe de",
  TITLE     = "The Conservation Theorem revisited",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "163--178",
  OPTADDRESS   = "Utrecht, The Netherlands",
  OPTMONTH     = mar,
  NOTE      = "Volume 664 of Lecture Notes in Computer Science"
}

@INPROCEEDINGS{Han:Pre:96,
  AUTHOR     ="Hanus, Michael and Prehofer, Christian",
  TITLE     = "Higher-Order Narrowing with Definitional Trees",
  BOOKTITLE = "Proceedings of the 7th International Conference on
              Rewriting Techniques and Applications (RTA '96)",
  YEAR      = 1996,
  EDITOR    = "Ganzinger, Harald",
  SERIES    = lncs,
  VOLUME    = 1103,
  PAGES     = "138--152",
  OPTADDRESS   = "New Brunswick, USA"
}
@ARTICLE{Hin:78,
  AUTHOR  = "Hindley, R.",
  TITLE   = "Reductions of Residuals are Finite",
  JOURNAL = tams,
  YEAR    = 1978,
  VOLUME  = 240,
  PAGES   = "345--361",
  OPTMONTH   = jun
}


@BOOK{Hin:Sel:86,
  AUTHOR    = "Hindley, J. Roger and Seldin, Jonathan P.",
  TITLE     = "Introduction to Combinators and $\lambda$-Calculus",
  PUBLISHER = cup,
  YEAR      = 1986,
  VOLUME    = 1,
  SERIES    = lmsst
}

@ARTICLE{Hue:75,
  AUTHOR  = "Huet, G.P.",
  TITLE   = "A unification algorithm for typed 
            ${\overline \lambda}$-calculus",
  JOURNAL = tcs,
  YEAR    = 1975,
  VOLUME  = 1,
  PAGES   = "27--57"
}

@ARTICLE{Hue:80,
  AUTHOR  = "Huet, G{\'e}rard",
  TITLE   = "Confluent Reductions:
            Abstract Properties and Applications to Term Rewriting Systems",
  JOURNAL = jacm,
  YEAR    = 1980,
  VOLUME  = 27,
  NUMBER  = 4,
  PAGES   = "797--821",
  OPTMONTH   = oct,
}

@ARTICLE{Hue:94,
  AUTHOR  = "Huet, G{\'e}rard",
  TITLE   = "Residual Theory in $\lambda$-calculus:
            a formal development",
  JOURNAL = jfp,
  YEAR    = 1994,
  VOLUME  = 4,
  NUMBER  = 3,
  PAGES   = "371--394"
}


@INCOLLECTION{Hue:Lev:91,
  AUTHOR    = "Huet, G{\'e}rard and L{\'e}vy, Jean-Jacques",
  TITLE     = "Computations in Orthogonal Rewriting Systems, {I} and {II}",
  BOOKTITLE = "Computational Logic:
              Essays in honor of Alan Robinson",
  PUBLISHER = mitp,
  YEAR      = 1991,
  EDITOR    = "Lassez, Jean-Louis and Plotkin, Gordon",
  PAGES     = "395--443",
  OPTADDRESS   = "Cambridge, Massachusetts"
}

@INCOLLECTION{Hue:Opp:80,
  AUTHOR    = "Huet, G{\'e}rard and Oppen, Derek C.",
  TITLE     = "Equations and Rewrite rules, a survey",
  BOOKTITLE = "Formal Language Theory,
              Perspectives and Open Problems",
  PUBLISHER = ap,
  YEAR      = 1980,
  EDITOR    = "Book, R.V.",
  PAGES     = "349--405"
}


@TECHREPORT{Hyl:73,
  AUTHOR      = "Hyland, J.M.E.",
  TITLE       = "A simple proof of the {C}hurch-{R}osser theorem",
  INSTITUTION = "Oxford University",
  YEAR        = 1973
}


@PHDTHESIS{Joi:93,
  AUTHOR  = "Joinet, J.-B.",
  TITLE   = "Etude de la normalisation du calcul des
            s{\'e}quents classique {\`a} travers la
            logique lin{\'e}aire",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1993
}

@INPROCEEDINGS{Jou:Oka:91,
  AUTHOR    = "Jouannaud, Jean-Pierre and Okada, Mitsuhiro",
  TITLE     = "A Computational Model for Executable Higher-Order
              Algebraic Specification Languages",
  BOOKTITLE = "Proceedings of the sixth annual IEEE Symposium on
              Logic in Computer Science (LICS '91)",
  YEAR      = 1991,
  PAGES     = "350--361",
  OPTADDRESS   = "Amsterdam",
  OPTMONTH     = jul,
}

@INPROCEEDINGS{Kah:93,
  AUTHOR    = "Kahrs, Stefan",
  TITLE     = "Compilation of Combinatory Reduction Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  PAGES     = "169--188",
  OPTADDRESS   = "Amsterdam, The Netherlands"
}

@INPROCEEDINGS{Kah:95,
  AUTHOR    = "Kahrs, Stefan",
  TITLE     = "Towards a domain theory for termination proofs",
  BOOKTITLE = "Proceedings of the 6th International Conference on
              Rewriting Techniques and Applications (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "241--255",
  OPTADDRESS   = "Kaiserslautern, Germany",
  OPTMONTH     = apr,
  VOLUME    = 941,
  SERIES    = lncs
}

@TECHREPORT{Ken:92,
  AUTHOR      = "Kennaway, J.R.",
  TITLE       = "On transfinite abstract reduction systems",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9205",
  OPTMONTH       = jan,
  YEAR        = 1992
}

@INPROCEEDINGS{Kha:90,
  AUTHOR    = "Khasidashvili, Z.O.",
  TITLE     = "Expression {R}eduction {S}ystems",
  BOOKTITLE = "Proceedings of I. Vekua Institute of Applied
              Mathematics",
  YEAR      = 1990,
  VOLUME    = 36,
  PAGES     = "200--220",
  OPTADDRESS   = "Tblisi"
}

@TECHREPORT{Kha:92,
  AUTHOR      = "Khasidashvili, Z.O.",
  TITLE       = "The {C}hurch-{R}osser theorem in orthogonal
                Combinatory Reduction Systems",
  INSTITUTION = "INRIA Rocqencourt",
  NUMBER      = 1825,
  YEAR        = 1992,
  OPTADDRESS     = "France"
}


@INPROCEEDINGS{Kha:93,
  AUTHOR    = "Khasidashvili, Zurab",
  TITLE     = "Optimal Normalization in Orthogonal
              Term Rewriting Systems",
  BOOKTITLE = "Proceedings of the Fifth International Conference
              on Rewriting Techniques and Applications (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "243--258",
  OPTADDRESS   = "Montreal, Canada",
  OPTMONTH     = jun,
  SERIES    = lncs,
  NUMBER    = 690
}

@INPROCEEDINGS{Kha:94,
  AUTHOR    = "Khasidashvili, Zurab",
  TITLE     = "The longest perpetual reductions in
              orthogonal Expression Reduction Systems",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "191--203",
  OPTADDRESS   = "St. Petersburg, Russia",
  OPTMONTH     = jul,
  SERIES    = lncs,
  NUMBER    = 813
}

@ARTICLE{Kha:Oos:95,
  AUTHOR  = "Khasidashvili, Z. and Oostrom, V. van",
  TITLE   = "Context-sensitive Conditional Expression Reduction
            Systems",
  JOURNAL = "Elsevier, Electronic Notes in Theoretical Computer Science",
  YEAR    = 1995,
  VOLUME  = 2,
  NOTE    = "Available at http://www.elsevier/nl/mcs/tcs/pc/volume2.htm"
}

@BOOK{Klo:80,
  AUTHOR    = "Klop, J.W.",
  TITLE     = "Combinatory Reduction Systems",
  PUBLISHER = "CWI",
  YEAR      = 1980,
  VOLUME    = 127,
  SERIES    = mct,
  OPTADDRESS   = "Amsterdam", 
  NOTE      = "PhD Thesis"
}

@INCOLLECTION{Klo:92,
  AUTHOR    = "Klop, J.W.",
  TITLE     = "Term rewriting systems",
  BOOKTITLE = "Handbook of Logic in Computer Science",
  PUBLISHER = oup,
  YEAR      = 1992,
  EDITOR    = "Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E.",
  PAGES     = "1--116",
  OPTADDRESS   = "New York",
  VOLUME    = 2,
}

@ARTICLE{Klo:Oos:Raa:93,
  AUTHOR  = "Klop, J.W. and Oostrom, V. van and Raamsdonk, F. van ",
  TITLE   = "Combinatory Reduction Systems: introduction and survey",
  JOURNAL = tcs,
  YEAR    = 1993,
  VOLUME  = 121,
  PAGES   = "279--308",
  NOTE    = "Special issue in honour of {C}orrado {B}{\"o}hm"
}


@ARTICLE{Klo:Vrij:89,
  AUTHOR  = "Klop, J.W. and Vrijer, R.C. de",
  TITLE   = "Unique Normal Forms for Lambda Calculus
            with Surjective Pairing",
  JOURNAL = ic,
  YEAR    = 1989,
  VOLUME  = 80,
  PAGES   = "97--113",
}

@BOOK{Kri:93,
  AUTHOR    = "Krivine, J.L.",
  TITLE     = "Lambda-Calculus, Types and Models",
  PUBLISHER = m,
  YEAR      = 1993,
  OPTADDRESS   = "Paris, France"
}


@INPROCEEDINGS{Laf:90,
  AUTHOR    = "Lafont, Yves",
  TITLE     = "Interaction Nets",
  BOOKTITLE = "Proceedings of the 17th ACM Symposium on
              Principles of Programming Languages (POPL '90)",
  YEAR      = 1990,
  PAGES     = "95--108",
  OPTADDRESS   = "San Francisco, USA",
  OPTMONTH     = jan
}

@INPROCEEDINGS{Lam:90,
  AUTHOR     = "Lamping, John",
  TITLE      = "An Algorithm for Optimal Lambda Calculus Reduction",
  BOOKTITLE  = "Proceedings of the 17th ACM
               Conference on Principles of 
               Programming Languages (POPL '90)",
  YEAR       = 1990,
  PAGES      = "16--30",
 OPTADDRESS     = "San Francisco, USA",
  OPTMONTH      = jan
}



@PHDTHESIS{Lan:93,
  AUTHOR  = "Laneve, Cosimo",
  TITLE   = "Optimality and Concurrency in
            Interaction Systems",
  SCHOOL  = "Universit{\`a} di Pisa",
  YEAR    = 1993,
  OPTADDRESS = "Pisa, Italy",
  OPTMONTH   = mar
}


@PHDTHESIS{Lev:78,
  AUTHOR  = "L{\'e}vy, Jean-Jacques",
  TITLE   = "R{\'e}ductions correctes et optimales
            dans le lambda-calcul",
  SCHOOL  = "Universit{\'e} de Paris VII",
  YEAR    = 1978
}

@UNPUBLISHED{Loa:95,
  AUTHOR  = "Loader, R.",
  TITLE   = "Normalisation by Translation",
  YEAR    = "1995",
  OPTMONTH   = "April",
  NOTE    = "Note distributed on the `types' mailing list"
}

@INPROCEEDINGS{Lys:Pir:95,
  AUTHOR    = "Lysne, Olav and Piris, Javier",
  TITLE     = "A Termination Ordering for Higher-Order 
               Rewrite Systems",
  BOOKTITLE = "Proceedings of the 6th International Conference on
              Rewriting Techniques and Applications (RTA '95)",
  YEAR      = 1995,
  EDITOR    = "Hsiang, Jieh",
  PAGES     = "26--40",
  SERIES    = lncs,
  VOLUME    = "914",
  OPTADDRESS   = "Kaiserslautern, Germany",
  OPTMONTH     = apr

}


@TECHREPORT{May:Nip:94,
  AUTHOR      = "Mayr, Richard and Nipkow, Tobias",
  TITLE       = "Higher-Order Rewrite Systems and their Confluence",
  INSTITUTION = "Technische Universit{\"a}t M{\"u}nchen",
  NUMBER      = "TUM-I9433",
  OPTMONTH       = aug,
  YEAR        = 1994
}

@PHDTHESIS{Mel:96,
  AUTHOR  = "Melli{\`e}s, Paul-Andr{\'e}",
  TITLE   = "Description Abstraite des Syst{\`e}mes de R{\'e}{\'e}criture",
  SCHOOL  = "Universit{\'e} de Paris VII",
  YEAR    = "1996",
  NOTE    = "To appear"
}

@PHDTHESIS{Meu:94,
  AUTHOR  = "Meulen, Emma A. van der",
  TITLE   = "Incremental Rewriting",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1994,
  OPTMONTH   = jan, 
}

@ARTICLE{Mil:91,
  AUTHOR  = "Miller, Dale",
  TITLE   = "A logic programming language with lambda-abstraction,
            function variables, and simple unification",
  JOURNAL = jlc,
  YEAR    = 1991,
  VOLUME  = 1,
  NUMBER  = 4,
  PAGES   = "497--536"
}

@PHDTHESIS{Ned:73,
  AUTHOR  = "Nederpelt, R.P.",
  TITLE   = "Strong Normalization in a Typed Lambda Calculus
            with Lambda Structured Types",
  SCHOOL  = "Technische Hogeschool Eindhoven",
  YEAR    = 1973,
  OPTMONTH   = jun
}

@BOOK{Ned:Geu:Vri:94,
  EDITOR    = "Nederpelt, R.P. and Geuvers, J.H. and 
              Vrijer, R.C. de",
  TITLE     = "Selected Papers on Automath",
  PUBLISHER = es,
  YEAR      = 1994,
  VOLUME    = 133,
  SERIES    = slfm
}



@ARTICLE{New:42,
  AUTHOR  = "Newman, M.H.A",
  TITLE   = "On theories with a combinatorial definition
            of ``equivalence''",
  JOURNAL = am,
  YEAR    = 1942,
  VOLUME  = 43,
  NUMBER  = 2,
  PAGES   = "223--243",
  OPTMONTH   = apr
}

@INPROCEEDINGS{Nip:91,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Higher-order Critical Pairs",
  BOOKTITLE = "Proceedings of the sixth annual IEEE Symposium on
              Logic in Computer Science (LICS '91)",
  YEAR      = 1991,
  PAGES     = "342--349",
  OPTADDRESS   = "Amsterdam, The Netherlands",
  OPTMONTH     = jul,
}

@INPROCEEDINGS{Nip:93,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Orthogonal Higher-order Rewrite Systems 
              are confluent",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "306--317",
  OPTADDRESS   = "Utrecht, The Netherlands",
  OPTMONTH     = mar,
  SERIES    = lncs,
  VOLUME    = 664
}

@INPROCEEDINGS{Nip:93:b,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "Functional Unification of Higher-Order Patterns",
  BOOKTITLE = "Proceedings of the eigth annual IEEE Symposium on
              Logic in Computer Science (LICS '93)",
  YEAR      = 1993,
  PAGES     = "64--74",
  OPTADDRESS   = "Montreal, Canada",
  OPTMONTH     = jun,
}

@INPROCEEDINGS{Nip:96,
  AUTHOR    = "Nipkow, Tobias",
  TITLE     = "More {Church-Rosser} Proofs
                (in {Isabelle/HOL})",
  BOOKTITLE = "Proceedings of the 13th International Conference on
              Automated Deduction (CADE '96)",
  YEAR      = 1996,
  ADDRES    = "New Jersey",
  NOTE      = "To appear"
}

@BOOK{OD:77,
  AUTHOR    = "O'Donnell, Michael J.",
  TITLE     = "Computing in Systems Described by Equations",
  PUBLISHER = sv,
  YEAR      = 1977,
  VOLUME    = 58,
  SERIES    = lncs,
}


@PHDTHESIS{Oos:94,
  AUTHOR  = "Oostrom, Vincent van",
  TITLE   = "Confluence for Abstract and
             Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit",
  YEAR    = 1994,
  OPTADDRESS = "Amsterdam",
  OPTMONTH   = mar,
  NOTE    = "Available at \verb+http://www.cs.vu.nl/~oostrom+"
}

@INPROCEEDINGS{Oos:96,
  AUTHOR    = "Oostrom, Vincent van",
  TITLE     = "Development Closed Critical Pairs",
  BOOKTITLE = "Proceedings of the Second International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '95)",
  YEAR      = 1996,
  EDITOR    = "Dowek, G. and Heering, J. and Meinke, K. and
              M{\"o}ller, B.",
  SERIES    = lncs,
  VOLUME    = 1074,
  PAGES     = "185--200",
  OPTADDRESS   = "Paderborn, Germany"
}

@INPROCEEDINGS{Oos:96:b,
  AUTHOR     ="Oostrom, Vincent van",
  TITLE     = "Higher-Order Families",
  BOOKTITLE = "Proceedings of the 7th International Conference on
              Rewriting Techniques and Applications (RTA '96)",
  YEAR      = 1996,
  EDITOR    = "Ganzinger, Harald",
  SERIES    = lncs,
  VOLUME    = 1103,
  PAGES     = "392-407",
  OPTADDRESS   = "New Brunswick, USA"
}

@MISC{Oos:96:c,
  AUTHOR = "Oostrom, Vincent van",
  TITLE  = "Personal communication",
  YEAR   = 1996
}

@INPROCEEDINGS{Oos:Raa:93a,
  AUTHOR    = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE     = "Comparing Combinatory Reduction Systems and
               Higher-order Rewrite Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  OPTADDRESS   = "Amsterdam"
}

@TECHREPORT{Oos:Raa:93b,
  AUTHOR      = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE       = "Comparing Combinatory Reduction Systems and
                Higher-order Rewrite Systems",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9361",
  OPTMONTH       = sep,
  YEAR        = 1993
}


@INPROCEEDINGS{Oos:Raa:94,
  AUTHOR    = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE     = "Weak orthogonality implies confluence:
              the higher-order case",
  BOOKTITLE = "Proceedings of the Third International Symposium
              on Logical Foundations of Computer Science (LFCS '94)",
  YEAR      = 1994,
  EDITOR    = "Nerode, A. and Matiyasevich, Yu.V.",
  PAGES     = "379--392",
  OPTADDRESS   = "St. Petersburg",
  OPTMONTH     = jul,
  SERIES    = lncs,
  VOLUME    = 813
}

@TECHREPORT{Oos:95,
  AUTHOR      = "Oostrom, Vincent van and Raamsdonk, Femke van",
  TITLE       = "Weak orthogonality implies confluence:
                the higher-order case",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9501",
  OPTMONTH       = jan,
  YEAR        = 1995
}

@INPROCEEDINGS{Par:90,
  AUTHOR    = "Parigot, Michel",
  TITLE     = "Internal Labellings in Lambda-Calculus",
  BOOKTITLE = "Proceedings of the 15th Symposium on
              Mathematical Foundations of Computer Science (MFCS '90)",
  YEAR      = 1990,
  EDITOR    = "Rovan, B.",
  PAGES     = "439--445",
  OPTADDRESS   = "Bansk{\'a} Bystrica, Czechoslovakia",
  OPTMONTH     = aug,
  SERIES    = lncs,
  VOLUME    = 452
}


@TECHREPORT{Pkh:77,
  AUTHOR      = "Pkhakadze, Sh.",
  TITLE       = "Some problems of the Notation Theory",
  INSTITUTION = "I. Vekua Institute of Applied Mathematics",
  YEAR        = 1977,
  NOTE        = "In Russian",
  OPTADDRESS     = "Tblisi, Georgia"
}


@ARTICLE{Plo:77,
  AUTHOR  = "Plotkin, G.D.",
  TITLE   = "{LCF} considered as a programming language",
  JOURNAL = tcs,
  YEAR    = 1977,
  VOLUME  = 5,
  PAGES   = "223--255"
}


@TECHREPORT{Plo:81,
  AUTHOR      = "Plotkin, Gordon D.",
  TITLE       = "A structured approach to operational semantics",
  INSTITUTION = "Aarhus University",
  NUMBER      = "DAIMI FN-19",
  OPTMONTH       = sep,
  YEAR        = 1981,
}

@INPROCEEDINGS{Pol:93,
  AUTHOR    = "Pol, J.C. van de",
  TITLE     = "Termination Proofs for Higher-Order Rewrite Systems",
  BOOKTITLE = "Proceedings of the First International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '93)",
  YEAR      = 1994,
  EDITOR    = "Heering, J. and Meinke, K. and
              M{\"o}ller, B. and Nipkow, T.",
  SERIES    = lncs,
  VOLUME    = 816,
  PAGES     = "305--325",
  OPTADDRESS   = "Amsterdam, The Netherlands"
}

@INPROCEEDINGS{Pol:Sch:95,
  AUTHOR    = "Pol, Jaco van de and Schwichtenberg, Helmut ",
  TITLE     = "Strict Functionals for Termination Proofs",
  BOOKTITLE = "Proceedings of the Second International Conference on
              Typed Lambda Calculi and Applications (TLCA '95)",
  YEAR      = 1995,
  EDITOR    = "Dezani-Ciancaglini, M. and Plotkin, G.",
  SERIES    = lncs,
  NUMBER    = 902,
  PAGES     = "350--364",
  OPTADDRESS   = "Edinburgh"
}

@INPROCEEDINGS{Pol:96,
  AUTHOR    = "Pol, Jaco van de",
  TITLE     = "Two {\em different} strong normalization proofs?",
  BOOKTITLE = "Proceedings of the Second International Workshop
              on Higher-Order Algebra, Logic and Term Rewriting
              (HOA '95)",
  YEAR      = 1996,
  EDITOR    = "Dowek, G. and Heering, J. and Meinke, K. and
              M{\"o}ller, B.",
  SERIES    = lncs,
  VOLUME    = 1074,
  PAGES     = "201--220",
  OPTADDRESS   = "Paderborn, Germany"
}



@PHDTHESIS{Pre:95,
  AUTHOR  = "Prehofer, Christian",
  TITLE   = "Solving Higher-Order Equations:
            From Logic to Programming",
  SCHOOL  = "Technische Universit{\"a}t M{\"u}nchen",
  YEAR    = 1995
}

@UNPUBLISHED{Raa:92,
  AUTHOR = "Raamsdonk, Femke van",
  TITLE  = "Representations of $\lambda$-terms as Proof Nets",
  YEAR   = 1992,
  NOTE   = "Master's Thesis"
}

@INPROCEEDINGS{Raa:93,
  AUTHOR    = "Raamsdonk, Femke van",
  TITLE     = "Confluence and Superdevelopments",
  BOOKTITLE = "Proceedings of the 5th International Conference on
              Rewriting Techniques and Applications (RTA '93)",
  YEAR      = 1993,
  EDITOR    = "Kirchner, Claude",
  PAGES     = "168--182",
  OPTADDRESS   = "Montreal, Canada",
  OPTMONTH     = jun,
  NOTE      = "Volume 690 of Lecture Notes in Computer Science"
}

@PHDTHESIS{Raa:96,
  AUTHOR  = "Raamsdonk, Femke van",
  TITLE   = "Confluence and Normalisation for 
            Higher-Order Rewriting",
  SCHOOL  = "Vrije Universiteit",
  YEAR    = 1996,
  OPTADDRESS = "Amsterdam",
  OPTMONTH   = may,
  NOTE    = "Available at \verb+http://www.cwi.nl/~femke+"
}

@TECHREPORT{Raa:Sev:95,
  AUTHOR      = "Raamsdonk, F. van and Severi, P.",
  TITLE       = "On Normalisation",
  INSTITUTION = "CWI",
  NUMBER      = "CS-R9545",
  OPTMONTH       = jun,
  YEAR        = 1995
}

@PHDTHESIS{Reg:92,
  AUTHOR  = "R{\'e}gnier, Laurent",
  TITLE   = "Lambda-calcul et r{\'e}seaux",
  SCHOOL  = "Universit{\'e} Paris {VII}",
  YEAR    = 1992
}

@INPROCEEDINGS{Rey:74,
  AUTHOR    = "Reynolds, John C.",
  TITLE     = "Towards a theory of type structure",
  BOOKTITLE = "Proceedings of the `Colloque sur la
              Programmation'",
  YEAR      = 1974,
  SERIES    = lncs,
  NUMBER    = 19,
  PAGES     = "408--425",
  OPTADDRESS   = "Paris, France"
}

@TECHREPORT{Roo:Ter:93,
  AUTHOR      = "Roorda, Dirk and Terlouw, Jan",
  TITLE       = "$\lambda$-calculus",
  INSTITUTION = "Rijksuniversiteit Groningen",
  YEAR        = 1993,
  NOTE        = "Coursnotes"
}


@PHDTHESIS{Ros:96,
  AUTHOR  = "Rose, Kristoffer H.",
  TITLE   = "Operational Reduction Models
            for Functional Programming Languages",
  SCHOOL  = "University of Copenhagen",
  YEAR    = 1996
}

@ARTICLE{Ros:73,
  AUTHOR  = "Rosen, Barry K.",
  TITLE   = "Tree-Manipulating Systems and
            {C}hurch-{R}osser Theorems",
  JOURNAL = jacm,
  YEAR    = 1973,
  VOLUME  = 20,
  NUMBER  = 1,
  PAGES   = "160--187",
  OPTMONTH   = jan
}

@INPROCEEDINGS{Ros:82,
  AUTHOR    = "Rosser, J. Barkley",
  TITLE     = "Highlights of the History of the
              Lambda-calculus",
  BOOKTITLE = "Proceedings of the ACM symposium on
              {LISP} and Functional Programming",
  YEAR      = 1982,
  PAGES     = "216--225",
  OPTADDRESS   = "New York"
}

@ARTICLE{Sch:24,
  AUTHOR  = "Sch{\"o}nfinkel, M.",
  TITLE   = "{\"U}ber die {B}austeine der mathematischen {L}ogik",
  JOURNAL = ma,
  YEAR    = 1924,
  VOLUME  = 92,
  PAGES   = "305--316"
}



@PHDTHESIS{Sch:65,
  AUTHOR  = "Schroer, D.E.",
  TITLE   = "The Church-Rosser Theorem",
  SCHOOL  = "Cornell University",
  YEAR    = 1965
}


@PHDTHESIS{Sch:94,
  AUTHOR  = "Schellinx, H.A.J.M.",
  TITLE   = "The Noble Art of Linear Decorating",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1994,
  OPTMONTH   = feb,
}


@INPROCEEDINGS{Sek:Ram:90,
  AUTHOR    = "Sekar, R.C. and Ramakrishnan, I.V.",
  TITLE     = "Programming in Equational Logic:
              Beyond strong sequentiality",
  BOOKTITLE = "Proceedings of the seventh International
              Symposium on Logic in Computer Science (LICS '90)",
  YEAR      = 1990,
  PAGES     = "230--241"
}

@PHDTHESIS{Spr:95,
  AUTHOR  = "Springintveld, Jan",
  TITLE   = "Algorithms for Type Theory",
  SCHOOL  = "Universiteit Utrecht",
  YEAR    = 1995,
  OPTMONTH   = may
}

@BOOK{Sten:72,
  AUTHOR    = "Stenlund, S.",
  TITLE     = "Combinators, $\lambda$-terms, and Proof Theory",
  PUBLISHER = "Reidel",
  YEAR      = 1972
}


@INPROCEEDINGS{Tak:93,
  AUTHOR    = "Takahashi, Masako",
  TITLE     = "$\lambda$-Calculi with Conditional Rules",
  BOOKTITLE = "Proceedings of the International Conference on
              Typed Lambda Calculi and Applications
              (TLCA '93)",
  YEAR      = 1993,
  EDITOR    = "Bezem, M. and Groote, J.F.",
  PAGES     = "406--417",
  OPTADDRESS   = "Utrecht, The Netherlands",
  OPTMONTH     = mar,
  VOLUME    = 664,
  SERIES    = lncs
}

@ARTICLE{Tai:67,
  AUTHOR  = "Tait, W.W.",
  TITLE   = "Intensional interpretation of functionals of finite type {I}",
  JOURNAL = jsl,
  YEAR    = 1967,
  VOLUME  = 32,
  PAGES   = "198--212",
}
 

@ARTICLE{Tak:95,
  AUTHOR  = "Takahashi, Masako",
  TITLE   = "Parallel Reductions in $\lambda$--Calculus",
  JOURNAL = ic,
  YEAR    = 1995,
  VOLUME  = 118,
  PAGES   = "120--127",
}

@ARTICLE{Ter:95,
  AUTHOR  = "Terlouw, Jan",
  TITLE   = "Strong normalization in type systems:
            a model theoretic approach",
  JOURNAL = apal,
  YEAR    = 1995,
  VOLUME  = 73,
  PAGES   = "53--78"
}


@ARTICLE{Vrij:85,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "A direct proof of the finite developments theorem",
  JOURNAL = jsl,
  YEAR    = 1985,
  VOLUME  = 50,
  NUMBER  = 2,
  PAGES   = "339--343",
  OPTMONTH   = jun
}

@PHDTHESIS{Vrij:87,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "Surjective Pairing and Strong Normalization:
            Two Themes in Lambda Calculus",
  SCHOOL  = "Universiteit van Amsterdam",
  YEAR    = 1987,
  OPTMONTH   = jan
}

@ARTICLE{Vrij:87:b,
  AUTHOR  = "Vrijer, Roel de",
  TITLE   = "Exactly estimating functionals and strong normalization",
  JOURNAL = "Proceedings of the Koninklijke Nederlandse Akademie van
            Wetenschappen",
  YEAR    = 1987,
  VOLUME  = 90,
  NUMBER  = 4,
  OPTMONTH   = dec
}

@PHDTHESIS{Wad:71, 
  AUTHOR  = "Wadsworth, C.P.",
  TITLE   = "Semantics and Pragmatics of the Lambda-Calculus",
  SCHOOL  = "Oxford University",
  YEAR    = 1971
}

@INPROCEEDINGS{Wol:91,
  AUTHOR    = "Wolfram, D.A.",
  TITLE     = "Rewriting, and Equational Unification:
              the Higher-Order Cases",
  BOOKTITLE = "Proceedings of the 4th International Conference on
              Rewriting Techniques and Applications (RTA '91)",
  YEAR      = 1991,
  ADRESS    = "Como, Italy"
}


@BOOK{Wol:93,
  AUTHOR     = "Wolfram, D.A.",
  TITLE      = "The Clausal Theory of Types",
  PUBLISHER  = cup,
  YEAR       = 1993,
  SERIES     = cttcs,
  VOLUME     = 21
}


@ARTICLE{henk91:jfp,
  AUTHOR  = "Barendregt, H.",
  TITLE   = "Introduction to {G}eneralised {T}ype {S}ystems",
  JOURNAL = "Journal of Functional Programming",
  YEAR    = 1991,
  VOLUME  = 1,
  NUMBER  = 2,
  PAGES = {125--154},
  OPTMONTH   = apr
}


@PHDTHESIS{herman:thesis,
	AUTHOR = {Geuvers, H.},
	TITLE = {Logics and type systems},
	SCHOOL = {University of Nijmegen},
	YEAR = {1993}
}

@PHDTHESIS{randy:thesis,
	AUTHOR = {Pollack, R.},
	TITLE = {The Theory of {LEGO}: {A} Proof Checker for the Extended
  Calculus of Constructions},
	SCHOOL = {University of Edinburgh},
	YEAR = {1994}
}

@PHDTHESIS{frederic:thesis,
	AUTHOR = {Blanqui, F.},
	TITLE = {Type Theory and Rewriting},
	SCHOOL = {University Paris-Sud},
	YEAR = {2001}
}



@ARTICLE{GN91:jfp,
  AUTHOR  = "Geuvers, H. and Nederhof, M.J.",
  TITLE   = "A modular proof of strong normalisation for the {C}alculus of
  {C}onstructions",
  JOURNAL = "Journal of Functional Programming",
  YEAR    = 1991,
  VOLUME  = 1,
  NUMBER  = 2,
  PAGES = {155--189},
  OPTMONTH   = apr
}

@INPROCEEDINGS{BFG94:lics,
	AUTHOR = {Barbanera, F. and Fern{\'a}ndez, M. and Geuvers, H.},
	TITLE = {Modularity of strong normalisation and confluence in the algebraic
  $\lambda$-cube},
	BOOKTITLE = {Proc. of LICS},
	PAGES = {406--415},
	YEAR = {1994}
}
 
@INPROCEEDINGS{gh95:hoa,
	AUTHOR = {Barthe, G. and  Geuvers, H.},
	TITLE = {Modular properties of algebraic type systems},
	BOOKTITLE = {Proc. of HOA},
	PAGES = {37--56},
	YEAR = {1995}
}








@misc{stehr99pure,
author = "M. Stehr and J. Meseguer",
title = "Pure type systems in rewriting logic",
text = "M.-O. Stehr and J. Meseguer. Pure type systems in rewriting logic. Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages.",
year = "1999",
url = "citeseer.nj.nec.com/stehr99pure.html" }



@article{ler00:jfp,
author={X. Leroy},
title={A modular module system},
journal="Journal of Functional Programming",
volume= 10,
number=3,
pages={269--303}, 
month=may,
year=2000}



@Article{KPT96:ic,
  title =        "A Typed Pattern Calculus",
  author =       "D. Kesner and L. Puel and V. Tannen",
  pages =        "32--61",
  journal =      "Information and Computation",
  month =        "10",
  year =         "1996",
  volume =       "124",
  number =       "1"}