@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"}