%% SERIES and PUBLISHERS @string{lnai="Lecture Notes in Artificial Intelligence"} @string{lncs="Lecture Notes in Computer Science"} @string{lnm="Lectures Notes in Mathematics"} @string{springer="Springer-Verlag"} @string{entcs="Electronic Notes in Theoretical Computer Science"} @string{nh="North-Holland"} %% Journals %% To be junked @STRING{JoACM = {Journal of the ACM}} @STRING{ACMCS = {ACM Computing Surveys}} @STRING{grund={Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik}} @STRING{SL={Studia Logica}} @string{sicomp="{SIAM} Journal on Computing"} @STRING{AfML = {Archive for Mathematical Logic}} @STRING{JoSL = {Journal of Symbolic Logic}} @STRING{JoSC = {Journal of Symbolic Computation}} @STRING{ActaCyb = {Acta Cybernetica}} @STRING{InfComp = {Information and Computation}} @STRING{SIAMJoC = {SIAM Journal of Computing}} @STRING{caap = {Colloquium on Trees in Algebras and Programming}} @STRING{ToPLaS = {ACM Transactions on Programming Languages and Systems}} @STRING{BoAMS = {Bulletin of Am. Math. Soc.}} %% To keep @string{polymorphism="Polymorphism: The {ML}/{LCF}/{HOPE} Newsletter"} @STRING{IndaMat = {Indagationes Mathematicae}} @STRING{AoM = {Annals of Mathematics}} @STRING{AJoM = {American Journal of Mathematics}} @STRING{FoCS = {Foundations of Computer Science}} @STRING{NDJoFL = {Notre Dame Journal of Formal Logic}} @STRING{CRaAdS = {Compte Rendu \`{a} l'Acad\'{e}mie des Sciences}} @STRING{TotAMS = {Transactions of the American Mathematical Society}} @STRING{InfCont = {Information and Control}} @STRING{IJoPP = {International Journal of Parallel Programming}} @STRING{ac= {Acta Cybernetica}} @STRING{ai={Acta Informatica}} @STRING{acmcs={ACM Computing Surveys}} @STRING{aml={Archive for Mathematical Logic}} @string{apal={Annals of Pure and Applied Logic}} @STRING{bams={Bulletin of Am. Math. Soc.}}@string{cacm="Communications of the {ACM}"} @string{fac={Formal Aspects of Computing}} @STRING{fi= {Fundamenta Informaticae}} @string{ic="Information and Computation"} @string{ipl ={Information Processing Letters}} @string{jacm={Journal of the ACM}} @string{jar="Journal of Automated Reasoning"} @string{jcss={Journal of Computer and System Sciences}} @string{jfp="Journal of Functional Programming"} @string{jlc="Journal of Logic and Computation"} @string{jsc="Journal of Symbolic Computation"} @string{jsl="Journal of Symbolic Logic"} @string{mscs="Mathematical Structures in Computer Science"} @string{mst="Mathematical Systems Theory"} @string{pnas="Proceedings National Academy of Sciences {USA}"} @string{scp = "Science of Computer Programming"} @string{siamc="{SIAM} Journal on Computing"} @string{sl= {Studia Logica}} @string{tcs="Theoretical Computer Science"} @string{toplas="{ACM} Transactions on Programming Languages and Systems"} @string{zml="Zeitschrift {f\"ur} Mathematische Logik und Grundlagen der Mathematik"} %% Institutions @string{lfcs={Laboratory for the Foundations of Computer Science, University of Edinburgh}} @string{kun={Department of Computer Science, University of Nijmegen}} @string{cwi={Centrum voor Wiskunde en Informatica, Amsterdam}} @STRING{TUE = {Eindhoven University of Technology}} @STRING{tlca1 ={Proceedings of TLCA'93}} @STRING{tlca2 ={Proceedings of TLCA'95}} @inproceedings{gh95:csl, author={G. Barthe and H. Geuvers}, title={Congruence types}, year={1996}, booktitle={Proceedings of CSL'95}, Publisher= {Springer-Verlag}, series= lncs, editor={H. Kleine Buening}, pages={36--51}, volume={1092}} @inproceedings{gh95:hoa, author={G. Barthe and H. Geuvers}, title={Modular properties of algebraic type systems}, year={1996}, booktitle={Proceedings of HOA'95}, Publisher= {Springer-Verlag}, series= lncs, pages={37-56}, editor={G. Dowek and J. Heering and K. Meinke and B. M{\"o}ller}, volume={1074}} @inproceedings{gmh95:braNR, author={G. Barthe and M. Ruys and H. Barendregt}, title={A two-level approach towards lean proof-checking}, year={1996}, Booktitle={Proceedings of TYPES'95}, Publisher= {Springer-Verlag}, series= lncs, volume={1158}, editor={S. Berardi and M. Coppo}, pages={16--35}} @InProceedings{g95:tlca , Author ={G. Barthe} , Title={Extensions of pure type systems} ,Booktitle={Proceedings of TLCA'95} , Year= 1995 , Publisher= {Springer-Verlag} , series= lncs , volume= {902} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , pages={16-31} , month={April} , crossref={tlca95}} @unpublished{gha96:csl, author={N. Ghani}, title={Eta-expansions: {$F^{\omega}$}}, booktitle={Proceedings of CSL'96}, year={1997}, note={Proceedings of CSL'96. To appear as LNCS}} @inproceedings{BR96, Author = "R. Bloo and K. Rose", Title = "Combinatory Reduction Systems with Explicit Substitutions that Preserve Strong Normalisation", booktitle= "RTA '96", series =lncs, editor={H. Ganzinger}, publisher=springer, volume={1103}, Year = {1996}, } @unpublished{gjm:wnsn, author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen}, title={{Weak Normalization implies Strong Normalization in Generalized Non-Dependent Pure Type Systems}}, year={1997}, note={Draft}} @unpublished{gpal, author={G. Barthe and P.-A. Melli{\`e}s}, title={On the subject reduction property for algebraic type systems}, year={1996}, note={Proceedings of CSL'96. To appear as LNCS}} @INPROCEEDINGS{arb96:clm, author={F. Arbab}, title={The {IWIM} model for coordination of concurrent activities}, BOOKTITLE={Coordination Languages and Models}, SERIES=lncs, volume={1061}, pages={34--56}, year={1996}, editor={P. Ciancarini and C. Hankin}} @INPROCEEDINGS{KW96:compass, author={J. Kamperman and H. Walters}, title={Minimal Term Rewriting Systems}, BOOKTITLE={Recent Trends in Data Type Specification}, SERIES=lncs, volume={1130}, pages={274--290}, year={1996}, editor={M. Haveraaen and O. Owe and O.-J. Dahl}} @inproceedings{GKW96:disco, author={S. Gray and N. Kajler and P.S. Wang}, title={Pluggability issues in the multi-protocol}, year={1996}, Publisher= {Springer-Verlag}, series= lncs, booktitle={Proceedings of DISCO'96}, editor={J. Calmet and C. Limongelli}, volume={1128}, pages={343--356}} @INPROCEEDINGS{fri78 , AUTHOR = {Friedman, H.} , TITLE = {Classically and Intuitionistically Provably Recursive Functions} , BOOKTITLE = {Higher Set-theory} , SERIES = lncs , VOLUME = 669 , EDITOR = {M\"uller, G.H. and Scott, D.S} , PUBLISHER = springer , PAGES = {21--28} , YEAR = 1978} @inproceedings{merill, Author = "B. Matthews", Title = "{MERILL}: An Equational Reasoning System in Standard {ML}", Booktitle = "Proceedings of RTA'93", Editor = "C. Kirchner", Series = lncs, Volume = 690, Pages = {441-445}, Publisher = springer, Year = 1993 } @INPROCEEDINGS{RS94:tacs , AUTHOR = {Rehof, N.J. and M.H. S{\o}rensen} , TITLE = {The $\lambda_{\Delta}$ calculus} , BOOKTITLE = {Proceedings of TACS'94} , SERIES = lncs , VOLUME = 789 , EDITOR = {Hagiya, M. and J. Mitchell} , PUBLISHER = springer , PAGES = {516--542} , YEAR = 1994 } @InProceedings{plu90:ctrs, author={D. Plump}, title={Implementing term rewriting by graph reduction: termination of combined systems}, series=lncs, booktitle={Proceedings of CTRS'90}, year={1991}, pages={307--317}, editor={S. Kaplan and M. Okada}, volume={516}} @InProceedings{BF93:icalp, author = "F. Barbanera and M. Fern{\'a}ndez", title = "Modularity of termination and confluence in combinations of rewrite systems with {$\lambda_\omega$}", series = lncs, booktitle = "Proceedings of ICALP'93", year = "1993", pages={657--668}, editor={A. Lingas and R. Karlsson and S. Karlsson}, volume={700}, publisher =springer} @InProceedings{DJK95:rta, author = "N. Dershowitz and J.-P. Jouannaud and J.W. Klop", title = "Problems in Rewriting {III}", pages = "457--471", year = "1995", month = apr, editor = "J. Hsiang", booktitle = "Proceedings of RTA'95", series = lncs, volume={914}, publisher = springer, } @InProceedings{TKB:rta89, author = "Y. Toyama and J.W. Klop and H. Barendregt", month = apr, year = "1989", title = "Termination for the Direct Sum of Left-Linear Term Rewriting Systems", booktitle = "Proceedings of RTA'89", editor = "N. Dershowitz", series = lncs, pages = "477--491", publisher = springer, volume={355}} @InProceedings{CMMS91:tacs, title = "An Extension of system~{$F$} with Subtyping", author = "L. Cardelli and S. Martini and J. Mitchell and A. Scedrov", pages = "750--770", booktitle = {Proceedings of TACS'91}, editor = "T. Ito and A. Meyer", series = lncs, volume = "526", year = "1991", month = sep, publisher = springer} @incollection(obj, title = "An Introduction to {OBJ3}", author = "J. Goguen and C. Kirchner and H. Kirchner and A. M\'egrelis and J. Meseguer", booktitle = "Proceedings of CTRS'88", editor = "J.-P. Jouannaud and S. Kaplan", publisher =springer, series=lncs, volume={308}, year = 1988, pages = "258--263") @inproceedings{xi97:tlca, AUTHOR = {Xi, H.} , TITLE = {Weak and Strong Normalisations in typed $\lambda$-calculi} , YEAR = 1997 , NOTE = {To appear} , editor ={J. Hindley} , booktitle={Proceedings of TLCA'97} , publisher =springer, series=lncs} @InProceedings{Qia90, author = "Z. Qian", title = "Higher-order order-sorted algebras.", booktitle = {Proceedings of ALP'90}, publisher = springer, SERIES = lncs, year = "1990"} @InProceedings{GJM85:icalp, title = "Operational semantics for order-sorted algebra", author = "J. Goguen and J.-P. Jouannaud and J. Meseguer", booktitle = {Proceedings of the ICALP'85}, year = "1985", pages = "221--231", editor = "W. Brauer", publisher = springer, series = lncs, volume = "194", } @INPROCEEDINGS{CP88:colog, AUTHOR = "T. Coquand and C. Paulin", TITLE = "Inductively defined types", BOOKTITLE = "Proceedings of {COLOG'88}", EDITOR = "P. Martin-{L}{\"o}f and G. Mints", YEAR = "1988", PUBLISHER = springer, SERIES = lncs, PAGES = "50--66", volume = "417"} @inproceedings{mh95:bra, author={M. Stefanova and H. Geuvers}, title={A simple set-theoretic semantics for the {C}alculus of {C}onstructions}, booktitle={Proceedings of TYPES'95}, EDITOR ={S. Berardi and M. Coppo} , SERIES = lncs , PUBLISHER = springer , volume={1158} , YEAR = 1996 , crossref={types95}} @inproceedings{qed, AUTHOR=".", TITLE="The {QED} manifesto", BOOKTITLE="Proceedings of CADE-12", EDITOR="A.Bundy", PAGES="238--251", PUBLISHER="Springer-Verlag", YEAR=1994, MONTH="June/July", NOTE="lnai 814"} @inproceedings{DCK93:icalp, author = "Di Cosmo, R. and D. Kesner", title = "A confluent reduction for the extensional typed $\lambda-$calculus with pairs, sums, recursion and terminal object", pages={645--656}, booktitle = "Proceedings of ICALP'93", year = "1993", editor={A. Lingas and R. Karlsson and S. Karlsson}, volume={700}, publisher= springer} @inproceedings{elf, AUTHOR="F. Pfenning", TITLE="Elf: a meta-language for deductive systems", BOOKTITLE="Proceedings of CADE-12", EDITOR="A. Bundy", PAGES="811--815", series=lnai, volume={814}, PUBLISHER="Springer-Verlag", YEAR={1994}} @inproceedings{BMcK:del, title = "Deliverables: An Approach to Program Development in the Calculus of Constructions", author = "R. Burstall and J. McKinna", booktitle = "Proceedings of MFCS'93", editor = {A.M. Borzyszkowski and S. Sokolowski}, series=lncs, volume={711}, publisher=springer, pages = {32--67}, year = 1993} @inproceedings{dow91:mfcs, title = "A Second-Order Pattern Matching Algorithm for the Cube of Typed Lambda-Calculi", author = "G. Dowek", booktitle = "Proceedings of MFCS'91", editor = {A. Tarlecki}, series=lncs, volume={520}, publisher=springer, pages = {151--160}, year = 1991} @InProceedings{gro94:caap, author = {de Groote, P.}, title = {A {CPS}-Translation of the $\lambda\mu$-Calculus}, booktitle = {Proceedings of CAAP'94}, editor = {Tison, S.}, volume = 787, series = LNCS, year = 1994, publisher = springer, pages = {85--99} } @InProceedings{gro95:tlca, author = {de Groote, P.}, title = {A Simple Calculus of Exception Handling}, crossref = {tlca95}, booktitle={Proceedings of TLCA'95}, pages = {201--215}, year={1995}} @InProceedings{tony95:tlca, author = {Hurkens, A.}, title = {{A Simplification of Girard's Paradox}}, crossrefonly = {tlca95}, booktitle={Proceedings of TLCA'95}, pages = {266--278}, year={1995} } @InProceedings{SP94:lfcs, author = "P. Severi and E. Poll", title = "Pure Type Systems with Definitions", booktitle = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, pages = "316--328", publisher = springer, crossrefonly={lfcs94}} @InProceedings{bak94:lfcs, author = " Bakel, S. van and L. Liquori and S. Ronchi della Roncha and P. Urzyczyn", title = "Comparing Cubes", booktitle = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, pages = "353-365", publisher = springer, crossrefonly={lfcs94}} @InProceedings{randy:ext, author ="R. Pollack", title ={On Extensibility of Proof Checkers}, pages={140-161}, booktitle ={Proceedings of TYPES'94}, editor ={P.Dybjer and B.Nordstr\"om and J.Smith}, series =lncs, volume={996}, year ={1995}, crossref={types94}, publisher ="Springer-Verlag"} @inproceedings{vBMKP93:bra, author={L. van Benthem Jutting and J. McKinna and R. Pollack}, title={Checking algorithms for pure type systems}, pages={19-61}, series=lncs, publisher=springer, volume={806}, year={1994}, booktitle={Proceedings of TYPES'93}, crossref={types93}} @inproceedings (adriana94:csl, author = "A. Compagnoni" , title = "Decidability of Higher-Order Subtyping with Intersection Types", booktitle= "Proceedings of CSL'94" , publisher = springer , year = "1995", pages={46-60}, editor={L. Pacholski and J. Tiuryn}, series = LNCS, volume = "933" ) @inproceedings{jac94:cade, author = {Jackson, P.} ,title = {Exploring Abstract Algebra in Constructive Type Theory} ,booktitle = "CADE'94" ,editor = {A. Bundy} ,publisher = {Springer} ,series = lnai ,year = {1994} } @INPROCEEDINGS{pau93:tlca , AUTHOR = {C. Paulin-Mohring} , TITLE = {Inductive Definitions in the System {C}oq. {R}ules and Properties} , BOOKTITLE = tlca1 , EDITOR = {M. Bezem and J.F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 , CROSSREF = {tlca} , PAGES = {328--345} } @INPROCEEDINGS{dow93:tlca , AUTHOR = {G. Dowek} , TITLE = {The undecidability of typability in the {Lambda-Pi-Calculus}} , BOOKTITLE = tlca1 , EDITOR = {M. Bezem and J.-F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 , CROSSREF = {tlca} , PAGES = {139--145} } @InProceedings{CKT95:tlca , Author ={Y. Coscoy and G. Kahn and L. Thery.} , Title={Extracting text from proofs} , Booktitle={Proceedings of TLCA'95} , Year= 1995 , Publisher= {Springer-Verlag} , series= lncs , volume= {902} , pages={109--123} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , month={April} , crossref={tlca95}} @InProceedings{DCP95:tlca , Author ={R. Di Cosmo and G. Piperno} , Title={Expanding extensional polymorphism} , Booktitle={Proceedings of TLCA'95} , Year= 1995 , Publisher= {Springer-Verlag} , series= lncs , volume= {902} , pages={?} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , month={April} , crossref={tlca95}} @InProceedings{martin95:tlca , Author={M. Hofmann} , Title={A simple model for quotient types} ,Booktitle={Proceedings of TLCA'95} , Year= 1995 , Publisher= {Springer-Verlag} , series= lncs , volume= {902} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , pages={216-234} , month={April} , crossref={tlca95}} @InProceedings{randy95:tlca , Author={R. Pollack} , Title={A verified type-checker} ,Booktitle={Proceedings of TLCA'95} , Year= 1995 , Publisher= {Springer-Verlag} , series= lncs , volume= {902} , Editor= {M. Dezani-Ciancaglini and G. Plotkin} , pages={?} , month={April} , crossref={tlca95}} @inproceedings{zha92:ctrs, author={H. Zhang}, title={Proving group isomorphisms theorems}, booktitle={Proceedings of CTRS'92}, year={1992}, Publisher= {Springer-Verlag}, series= lncs, editor={M. Rusinovitch and J.-L. Remy}, pages={302-306}} @inproceedings{mit95:fct, author={J. Mitchell and K. Fischer}, title={A delegation-based object calculus with subtyping}, booktitle={Proceedings of FCT'95}, series=lncs, volume={965}, year={1995}, pages={42-61}, Publisher= {Springer-Verlag}, editor={H. Reichel}} @inproceedings{BBK87:rta, author={J. Baeten and J. Bergstra and J.W. Klop}, title={Priority rewrite systems}, pages={83-94}, editor={P. Lescanne}, series=lncs, volume={256}, publisher=springer, booktitle={Rewriting techniques and applications}, year={1987}} @inproceedings{BF93:tlca, author={F. Barbanera and M. Fern{\'a}ndez}, title={Combining first and higher order rewrite systems with type assignment systems}, booktitle={Proceedings of TLCA'93}, editor={M.Bezem and J.-F. Groote}, pages={60-74}, crossref={tlca} ,year={1993}} @inproceedings{FJ, author={M. Fern{\'a}ndez and J.-P.Jouannaud}, title={Modularity of termination of term-rewriting systems revisited}, pages={255-272}, booktitle={Recent Trends in Data Type Specification}, editors={E. Artesiano and G. Reggio and A. Tarlecki}, year={1994}, series=lncs, volume={906}, publisher=springer} @inproceedings{herman94:bra, author={H. Geuvers}, title={A short and flexible proof of strong normalisation for the {C}alculus of {C}onstructions}, booktitle={Proceedings of TYPES'94}, editors={P. Dybjer and B. Nordstr{\"o}m and J. Smith}, year={1995}, series=lncs, pages={14-38}, crossref={types94}, publisher=springer} @inproceedings{herman93:bra, author={H. Geuvers}, title={Conservativity between logics and typed $\lambda$-calculi}, booktitle={Proceedings of TYPES'93}, year={1993}, series=lncs, pages={79--107}, crossref={types93}, publisher=springer} @inproceedings{healf94:bra, author={H. Goguen}, title={The metatheory of UTT}, booktitle={Proceedings of TYPES'94}, editors={P. Dybjer and B. Nordstr{\"o}m and J. Smith}, year={1995}, series=lncs, pages={60-82}, crossref={types94}, publisher=springer} @InProceedings{PRW96:tableau, author = {E.~Ritter and D.~Pym and L.~A.~Wallen}, title = {On the Intuitionistic Force of Classical Search}, booktitle = {Proceedings of TABLEAU'96}, editor = {P.~Miglioli and U.~Moscato and D.~Mundici and M.~Ornaghi}, volume = 1071, series = lnai, year = 1996, publisher = springer, pages = {295--311}} @InProceedings{PRW96:cade, author = {E. Ritter and D. Pym and L. Wallen}, title = {Proof-terms for Classical and Intuitionistic Logic (extended abstract)}, booktitle = {Proceeedings of CADE'96}, series=lnai, volume={1104}, year={1996}, pages={??-??}, editor={M. McRobbie and J. Slaney}} @inproceedings{HT93:hol, author={J. Harrison and L. Thery}, title={Extending the {HOL} theorem prover with a computer algebra system to reason about the reals}, booktitle={Proceedings of HOL'93}, year={1993}, editor={J.J. Joyce and C.-J.H. Seger}, series=lncs, pages={174-184}, volume={780}, publisher=springer} @inproceedings{FM94:tacs, author={K. Fischer and J. Mitchell}, title={Notes on typed object-oriented programming}, booktitle={Proceedings of TACS'94}, year={1994}, editor={M. Hagiya and J. Mitchell}, series=lncs, pages={844-885}, volume={789}, publisher=springer} @inproceedings{MS89:rta, author={C. Mohan and M. Srivas}, title={Negation with logical variables in conditional rewiting}, booktitle={Proceedings of RTA'89}, year={1989}, editor={N. Dershowitz}, pages={292-310}, volume={355}, series=lncs, publisher=springer} @inproceedings{Moh89:rta, author={C. Mohan}, title={Priority rewriting: semantics, confluence and conditionals}, booktitle={Proceedings of RTA'89}, year={1989}, editor={N. Dershowitz}, pages={278-291}, volume={355}, series=lncs, publisher=springer} @inproceedings{CZ94:cade, author={E. Clarke and X. Zhao}, title={Combining Symbolic Computation and Theorem Proving: Some Problems of {Ramanujan}}, pages={758-763}, booktitle={Proceedings of Cade-12}, year={1994}, crossref={cade94}} @inproceedings{Kir93:tr, author={H. Kirchner}, title={Some extensions of rewriting}, booktitle={Term rewriting}, pages={54-73}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @inproceedings{Jou93:tr, author={J.-P. Jouannaud}, title={Introduction to Rewriting}, booktitle={Term rewriting}, pages={1-15}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @inproceedings{Der93:tr, author={N. Dershowitz}, title={33 examples of termination}, booktitle={Term rewriting}, pages={16-26}, crossref={CJ93}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @book{isabelle, title={Isabelle: a generic theorem prover}, author={L. Paulson}, series= lncs, volume={828}, PUBLISHER=springer, year={1994}} @PROCEEDINGS{tlca , TITLE = tlca1 , EDITOR = {M. Bezem and J.-F. Groote} , SERIES = lncs , VOLUME = 664 , PUBLISHER = springer , YEAR = 1993 } @PROCEEDINGS{tlca95 , TITLE = tlca2 , EDITOR = {M. Dezani-Ciancaglini and G. Plotkin} , SERIES = lncs , VOLUME = 902 , PUBLISHER = springer , YEAR = 1995 } @PROCEEDINGS{types93 , TITLE ={Proceedings of TYPES'93} , EDITOR ={H. Barendregt and T. Nipkow} , SERIES = lncs , VOLUME = 806 , PUBLISHER = springer , YEAR = 1994 } @PROCEEDINGS{types94 , TITLE ={Proceedings of TYPES'94} , EDITOR ={P. Dybjer and B. Nordstr{\"o}m and J. Smith} , SERIES = lncs , VOLUME = 996 , PUBLISHER = springer , YEAR = 1995 } @PROCEEDINGS{types95 , TITLE ={Proceedings of TYPES'95} , EDITOR ={S. Berardi and M. Coppo} , SERIES = lncs , PUBLISHER = springer , YEAR = 1996 , volume={1158}} @proceedings{cade94, title={Proceedings of CADE-12}, editor={A. Bundy}, volume=814, series=lnai, year={1994}, publisher=springer} @proceedings{CJ93, title={Term Rewriting}, editor={H. Comon and J.-P. Jouannaud}, series= lncs, PUBLISHER=springer, year={1993}, volume={909}} @Proceedings{WGH96, editor = "J. von Wright and J. Grundy and J. Harrison", title = "Proceedings of TPHOL'96", series = lncs, volume = 1125, year = 1996, publisher =springer} @Proceedings{lfcs94, title = "Proceedings of LFCS'94", year = {1994}, editor= {A. Nerode and Y.N. Matiyasevich}, volume = {813}, series = lncs, publisher = springer} @Article{pau86:jsc, author={L.C. Paulson}, title={Constructing Recursion Operators in Intuitionistic Type Theory}, journal=jsc, year=1986, volume=2, number=4, pages={325--355}} @Article{JO97:tcs, title={Abstract data type systems}, author={J.-P. Jouannaud and M. Okada}, pages={349--391}, journal=tcs, year=1997, volume=173, number=2} @Article{BF96:tcs, title={Intersection type assignment systems with higher-order algebraic rewriting}, author={F. Barbanera and M. Fern{\'a}ndez}, pages={173--207}, journal=tcs, month={15~} # dec, year=1996, volume=170, number={1--2}} @Article{BB96:jfp, title={Proof-irrelevance out of excluded-middle and choice in the calculus of constructions}, author={F. Barbanera and S. Berardi}, pages={519--525}, journal=jfp, month=may, year=1996, volume=6, number=3 } @Article{thomas92:tcs, title={Independence of the induction principle and the axiom of choice in the pure calculus of constructions}, author={T. Streicher}, pages={395--408}, journal=tcs, year=1992, month={14~} # sep, volume=103, number=2} Article{toy87:ipl, title={Counterexamples to termination for the direct sum of term rewriting systems}, author={Y. Toyama}, pages={141--143}, journal=ipl, year=1987, month={29~} # may, volume=25, number=3} @Article{zan94:jsc, author={H. Zantema}, title={Termination of Term Rewriting: Interpretation and Type Elimination}, journal=jsc, year=1994, volume=17, number=1, pages={23--50}, month=jan, keywords={Special Issue on Conditional Term Rewriting Systems} } @Article{lam68:mst, title={Deductive Systems and Categories {I}. {Syntactic} Calculus and Residuated Categories}, author={J. Lambek}, journal=mst, pages={287--318}, year=1968, volume=2, number=4} @ARTICLE{law64:pnas, AUTHOR = "F.W. Lawvere", TITLE = "An elementary theory of the category of sets", JOURNAL = pnas, VOLUME = 52, YEAR = 1964, PAGES = "1506--1511"} @ARTICLE{law69:dia, AUTHOR = "F.W. Lawvere", TITLE = "Ajointness in foundations", JOURNAL = "Dialectica", VOLUME = 23, YEAR = 1969, PAGES = "281--296"} @ARTICLE{man75:lms, author={C. Mann}, title={The connection between equivalences of proofs and cartesian closed categories}, journal={Proceedings of the London Mathematical Society}, volume={31}, pages={289--310}, year={1975}} @article{pot77:aml, author={G. Pottinger}, title={Normalization as a homomorphic image of cut-elimination}, journal=aml, volume={12}, pages={323--357}, year={1977}} @article{zuc74:aml, author={J. Zucker}, title={The correspondence between cut-elimination and normalization}, journal=aml, volume={7}, pages={113-155}, year={1974}} @article{sta83:grund, author={R. Statman}, title={$\lambda$-definable functionals and $\beta\eta$-conversion}, year={1983}, journal=grund, pages={21--26}, volume={23} } @inproceedings{bie96:ll, author="G.M. Bierman", title="Towards a Classical Linear $\lambda$-calculus", booktitle="Proceedings of Tokyo Conference on Linear Logic", volume=3, series=entcs, publisher="Elsevier", year=1996 } @Article{hue80:jacm, title={Confluent Reductions: Abstract Properties and Application to Term Rewriting Systems}, author={G{\'e}rard Huet}, pages={797--821}, journal=jacm, month=oct, year=1980, volume=27, number=4, } @Article{lei85:jsl, author = "Leivant, D.", title = "Syntactic Translations and Provably Recursive Functions", journal = jsl, year = "1985", volume = "50", number = "3", pages = "682--688" } @article{wan87:fi, author={M. Wand}, title={A simple algorithm and proof for type inference}, year={1987}, pages={115-122}, volume={X}, journal=FI} @Article{sel89:sl, author = {Seldin, J.P.}, title = {Normalization and Excluded Middle}, journal = SL, year = 1989, volume = {XLVIII}, number = 2, pages = {193--217} } @Article{sel86:jsl, author = {Seldin, J.P.}, title = {On the Proof theory of the Intermediate Logic {MH}}, journal = JSL, year = 1986, volume = 51, number = 3, pages = {626--647} } @Article{kri94:tcs, title={A general storage theorem for integers in call-by-name {$\lambda$}-calculus}, author={J.-L. Krivine}, journal=tcs, pages={79--94}, month=jun, year=1994, volume=129, number=1} @Article{DN95:jsl, title={Storage Operators and Directed Lambda-Calculus}, author={R. David and K. Nour}, pages={1054--1086}, journal=jsl, year=1995, month=dec, volume=60, number=4 } @Article{kri94:apal, title={Classical logic, storage operators and second-order lambda-calculus}, author={J.-L. Krivine}, pages={53--78}, journal=apal, month=jun, year=1994, volume=68, number=1} @Article{HHP93:acm, title={A Framework for Defining Logics}, author={R. Harper and F. Honsell and G. Plotkin}, pages={143--184}, journal=jacm, month=jan, year=1993, volume=40, number=1} @article{OD91:fac, author={O. Owe and O.J. Dahl}, title={{Generator Induction in Order-Sorted Algebras}}, journal=fac, pages={2--20}, volume={3}, year={1991}} @Article{dow93:jlc, title={A Complete Proof Synthesis Method for the Cube of Type Systems}, author={G. Dowek}, pages={287--315}, journal=jlc, year=1993, volume=3, number=3} @Article{martin95:mscs, title={Sound and complete axiomatisations of call-by-balue control operators}, author={M. Hofmann}, pages={461--482}, journal=mscs, month=dec, year=1995, volume=5, number=4} @Article{reh96:ipl, title={Strong normalization for non-structural subtyping via saturated sets}, author={J. Rehof}, pages={157--162}, journal=ipl, month={27}, year=1996, volume=58, number=4} @Article{thomas91:mscs, title={Dependence and independence results for (impredicative) calculi of dependent types}, author={T. Streicher}, pages={29--54}, journal=mscs, month=mar, year=1992, volume=2, number=1 } @unpublished{erik:ep, author={E. Poll}, title={Expansion Postponement}, year={1996}, note={Manuscript}} @Article{dan94:scp, title={Back to direct style}, author={O. Danvy}, pages={183--195}, journal=scp, month=jun, year=1994, volume=22, number=3} @Article{sel97:apal, title={On the proof theory of {Coquand's} calculus of constructions}, author={J.P. Seldin}, pages={23--101}, journal=apal, month={6~} # jan, year=1997, volume=83, number=1} @Article{plo75:tcs, title={Call-by-Name, Call-by-Value and the {$\lambda$}-Calculus}, author={G. Plotkin}, pages={125--159}, journal=tcs, year=1975, month=dec, volume=1, number=2 } @Article{vB93:ic, title={Typing in Pure Type Systems}, author={Benthem Jutting, L. S. van}, pages={30-41}, journal=ic, month=jul, year=1993, volume=105, number=1} @Article{coq95:jsl, title={A Semantics of Evidence for Classical Arithmetic}, author={T. Coquand}, pages={325--337}, journal=jsl, year=1995, volume=60, number=1} @Article{KN96:jfp, title={Canonical typing and {$\Pi$}-conversion in the {Barendregt Cube}}, author={F. Kamareddine and R. Nederpelt}, pages={245--267}, journal=jfp, month=mar, year=1996, volume=6, number=2 } @unpublished{paula96, author={P. Severi}, title={Pure type systems without the $\Pi$-conversion}, year={1995}, note={Manuscript}} @Article{JG95:jfp, title={The Virtues of Eta-expansion}, author={C.B. Jay and N. Ghani}, pages={135--154}, journal=jfp, month=apr, year=1995, volume=5, number=2 } @Article{CH85:jsc, author={T. Coquand and G. A. Huet}, title={A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction}, journal=jc, year=1985, volume=1, number=3, pages={323--328}, month=sep } @Article{TF92:apal, title={On the adequacy of representing higher order intuitionistic logic as a pure type system}, author={H. Tonino and K. Fujita}, pages={251--276}, journal=apal, month=jun, year=1992, volume=57, number=3} @article (adriana96:mscs, author = "A. Compagnoni and B. Pierce" , title = "Intersection Types and Multiple Inheritance", pages = {469--501}, journal = mscs, month = oct, year = 1996, volume = 6, number = 5 ) @Article{sta91:jsl, title={Normalization Theorems for Full First Order Classical Natural Deduction}, author={G. St{\aa}lmarck}, pages={129--149}, journal=jsl, year=1991, month=mar, volume=56, number=1} @Article{nak94:apal, title={A constructive logic behind the catch and throw mechanism}, author={H. Nakano}, pages={269--301}, journal=apal, month=oct, year=1994, volume=69, number={2--3}} @article{BR96:fi, author={I. Bethke and P. Rodenburg}, title={Equational Constructor Induction}, journal=FI, pages={1--16}, volume={25}, number={1}, year={1996}, note={Also appeared as Report P9219, University of Amsterdam, Programming Research Group, 1992}} @Article{BB96:ic, title={A Symmetric Lambda Calculus for Classical Program Extraction}, author={F. Barbanera and S. Berardi}, pages={103--117}, journal=ic, month=mar, year=1996, volume=125, number=2} @Article{BB95:apal, title={A strong normalization result for classical logic}, author={F. Barbanera and S. Berardi}, pages={99--116}, journal=apal, month=dec, year=1995, volume=76, number=2} @incollection{KKSV95:jsc, author={R. Kennaway and J.W. Klop and R. Sleep and F.J. de Vries}, title= {Comparing curried and uncurried rewriting}, journal=jsc, year={1996}, note={To appear}} @article {BDL95:ic, title = {Intersection and Union Types: Syntax and Semantics}, author = {F. Barbanera and M. Dezani-Ciancaglini and U. de'Liguoro}, pages = {202--230}, journal = ic, year = 1995, volume = 119, number = 2 } @article {CD78, author = "M. Coppo and M. Dezani-Ciancaglini", title = "A New Type-Assignment for $\lambda$-Terms", journal = "Archiv f{\"u}r Mathematische Logik", volume = 19, pages = "139-156", year = "1978"} @article (CL91:jfp, author = "L. Cardelli and G. Longo", title = "A semantic basis for {Q}uest", journal = "Journal of Functional Programming", year = "1991", month = "October", volume = "1", number = "4", pages = "417--458") @Article{KOR93:tcs, author = "J.W. Klop and V. van Oostrom and F. van Raamsdonk", title = "Combinatory Reduction Systems: Introduction and Survey", journal = tcs, volume = "121", number={1-2}, pages={279-308}, year = "1993"} @Article{BCM88:part2, author = "R. Backhouse and P. Chisholm and G. Malcolm", title = "Do-It-Yourself Type Theory (Part {II})", journal = "BEATCS: Bulletin of the European Association for Theoretical Computer Science", volume = "35", year = "1988", pages={205-244}} @Article{BCM88:part1, author = "R. Backhouse and P. Chisholm and G. Malcolm", title = "Do-it-yourself Type Theory (Part {I})", journal = "BEATCS: Bulletin of the European Association for Theoretical Computer Science", volume = "34", pages={68-110}, year = "1988", } @Article{GM93:ic, title = "Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation, and Coercion Problems", author = "J. Meseguer and J. Goguen", pages = "114--158", journal = ic, month = mar, year = "1993", volume = "103", number = "1", } @Article{GM92:tcs, author = "J. Goguen and J. Meseguer", title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations", journal = tcs, volume = "105", number={2}, pages={216-273}, year = "1992", } @ARTICLE{CW85, AUTHOR = "L. Cardelli and P. Wegner", TITLE = "On understanding types, data abstraction and polymorphism", JOURNAL = ACMCS, VOLUME = 4, PAGES = "471--522", YEAR = 1985} @ARTICLE{dyb94:fac, AUTHOR = "P. Dybjer", TITLE = "Inductive Families", JOURNAL = fac, VOLUME = "6", PAGES = "440-465", YEAR = 1994} @ARTICLE{dyb97:tcs, AUTHOR = "P. Dybjer", TITLE ={{Representing inductively defined sets by well-orderings in Martin-L{\"o}f's type theory}}, journal=tcs, year={199x}, note={To appear}} @ARTICLE{dyb:jsl, AUTHOR = "P. Dybjer", TITLE ={A general formulation of simultaneous inductive-recursive definitions in type theory}, journal=jsl, year={199x}, note={To appear}} @ARTICLE{DG94:mscs, AUTHOR = "J. Goguen and R. Diaconescu", TITLE = "An {O}xford survey of order sorted algebra", JOURNAL = mscs, VOLUME = "4", YEAR = 1994, PAGES = "363--392"} @article (PS97:tcs, author = "B. Pierce and M. Steffen" , title = "Higher-Order Subtyping", year = 1997, journal = "Theoretical Computer Science", volume = 176, number = "1--2", pages = "235--282" ) @article (HP95:jfp, author = "M. Hofmann and B. Pierce" , title = "A Unifying Type-Theoretic Framework for Objects", journal = jfp, pages={593-635}, volume={5}, number={4}, year={1995} ) @article (PT94:jfp, author = "B. Pierce and D. Turner" , title = "Simple Type-Theoretic Foundations for Object-Oriented Programming", journal = jfp, volume = 4, number = 2, pages = "207--247", year = "1994" ) @article{mul92:ipl, author={F. M{\"u}ller}, title={Confluence of the lambda calculus with left-linear algebraic rewriting}, journal=ipl, year={1992}, pages={293-299}, volume={41}} @article{henk91:jfp, author = "H. Barendregt", title = "Introduction to {G}eneralised {T}ype {S}ystems", journal = "J. Functional Programming", volume = 1, number = 2, pages = "125--154", year = 1991, month = {April} } @article{AHMP, author="A. Avron and F. Honsell and I. Mason and R. Pollack", title="Using Typed Lambda Calculus to Implement Formal Systems on a Machine", journal = "Journal of Automated Reasoning", year = "1992", volume = "9", pages = "309-352" } @article{toy87:acm, author={Y. Toyama}, title={On the {Church-Rosser} Property for the Direct Sum of Term Rewriting Systems}, year={1987}, volume={34}, number={1}, pages={128-143}, journal=jacm} @article{CH88:ic, author="T. Coquand and G. Huet", title={{The Calculus of Constructions}}, journal=ic, volume=76, number="2/3", pages="95--120", month={February/March}, year=1988 } @ARTICLE{church32 , AUTHOR = "A. Church" , TITLE = "A set of postulates for the foundation of logic" , JOURNAL = AoM , VOLUME = 33 , PAGES = "346--366" , YEAR = 1932 } @ARTICLE{church33 , AUTHOR = "A. Church" , TITLE = "A set of postulates for the foundation of logic" , JOURNAL = AoM , VOLUME = 34 , PAGES = "839--864" , YEAR = 1933 } @ARTICLE{church:simple , AUTHOR = "A. Church" , TITLE = "A formulation of the simple theory of types" , JOURNAL = JoSL , VOLUME = 5 , PAGES = "414--432" , YEAR = 1940 } @article{dou92:ic, author={D. Dougherty}, title={Adding algebraic rewriting to the untyped lambda calculus}, journal=ic, year={1992}, volume={101}, pages={251-267}} @article{yu , author={Y. Yu} , title={Computer proofs in group theory} , journal=jar , year=1990 , pages={251-286} , volume={6} , number={3} , month={September} } @article{imps, author={W. Farmer and J. Guttman and F. Thayer}, title={{\sc imps}: {an Interactive Mathematical Proof System}}, journal=jar, year={1993}, pages={231-248}, volume={11}} @article{telescope, author={N.G. de Bruijn}, title={Telescopic mappings in typed lambda calculus}, journal=ic, year={1991}, pages={189-204}, volume={91}, month={April}} @article{BTG:sn, author={V. Breazu-Tannen and J. Gallier}, title={Polymorphic rewriting conserves algebraic strong normalisation}, journal=tcs, volume={83}, pages={3-28}, year={1990}} @Article{CH94:jfp, title={A-translation and looping combinators in pure type systems}, author={T. Coquand and H. Herbelin}, pages={77--88}, journal=jfp, month=jan, year=1994, volume=4, number=1 } @Article{DCK96:tcs, title={Combining algebraic rewriting, extensional lambda calculi, and fixpoints}, author={R. Di Cosmo and D. Kesner}, pages={201--220}, journal=tcs, month={5~} # dec, year=1996, volume=169, number=2} @article{BTG:cr, author={V. Breazu-Tannen and J. Gallier}, title={Polymorphic rewriting conserves algebraic confluence}, journal=ic, year={1994}, volume={114}, pages={1-29}} @article{bac89:fac, author={R. Backhouse and P. Chisholm and G. Malcolm}, Title={Do-it-yourself type theory}, journal={Formal Aspects of Computing}, Volume={1}, pages={19--84}, year={1989}} @Article{FFKD87:tcs, title={A Syntactic Theory of Sequential Control}, author={M. Felleisen and D.P. Friedman and E. Kohlbecker and B. F. Duba}, pages={205--237}, journal=tcs, year=1987, volume=52, number=3} @article{GN91:jfp, author={H. Geuvers and M.-J. Nederhof}, title={A modular proof of strong normalisation for the {C}alculus of {C}onstructions}, journal=jfp, volume={1}, pages={155-189}, year={1991}} @Article{HDM93:jfp, title={Typing first-class continuations in {ML}}, author={R. Harper and B.F. Duba and D. MacQueen}, pages={465--484}, journal=jfp, month=oct, year=1993, volume=3, number=4 } @Article{HL95:jfp, title={Typing first-class continuations in {ML}}, author={M. Lillibridge and R. Harper}, journal=jfp, year=1993, note={Submitted}} @article{morten:ic, author = {S{\o}rensen, M.H.}, title = {Strong Normalization from Weak Normalization in Typed $\lambda$-Calculi}, note = {To appear}, year = {199x}, journal=ic } @Article{ter95:apal, title={Strong normalization in type systems: a model theoretic approach}, author={J. Terlouw}, pages={53--78}, journal=apal, month= may, year=1995, volume=73, number=1} @article{bak:apal, author={Bakel, S. van and Liquori, L. and Ronchi della Rocca, S. and Urzyczyn, P.}, title={Comparing cubes of Typed and Type Assignment Systems}, journal=apal, year={199x}, note={To appear}} @ARTICLE{haskell, AUTHOR = {Hudak, P. and Peyton Jones, S.L. and Wadler, P.L. and Arvind and Boutel, B. and Fairbairn, J. and Fasel, J. and Guzman, K. and Hammond, K. and Hughes, J. and Johnsson, T. and Kieburtz, R. and Nikhil, R.S. and Partain, W. and Peterson, J.}, TITLE = {Report on the functional programming language {Haskell}, version 1.2}, JOURNAL = {Special Issue of SIGPLAN Notices}, VOLUME = {27}, YEAR = {1992} } @article{jon:jfp95, author={M. Jones}, title={A system of constructor classes: overloading and implicit higher-order polymorphism}, journal=jfp, pages={1-25}, month={January}, year={1995}} @article{BCGS91:ic, author={V. Breazu-Tannen and T. Coquand and C. Gunter and A. Scedrov}, title={Inheritance as implicit coercion}, journal=ic, year={1991}, volume={93}, pages={172-221}} @article{rus87:ipl, author={M. Rusinowitch}, title={On termination of the direct sum of term-rewriting systems}, journal=ipl, pages={65-70}, volume={26}, year={1987}} @article{BK86:jcss, author={J. Bergstra and J.W. Klop}, title={Conditional rewrite rules: confluence and termination}, journal=jcss, pages={323-362}, volume={32}, year={1986}} @incollection{DC:survey, author={R. Di Cosmo}, title={A brief history of rewriting with extensionality}, booktitle={International Summer School on Type Theory and Term Rewriting, Glasgow, September 1996}, editor={F. Kamareddine}, publisher={Kluwer}, year={199x}, note={To appear}} @book{MT93:book, editor={K. Meinke and J.V. Tucker}, title={Many sorted logic and its applications}, publisher={John Wiley and Sons}, year={1993}} @book{BW:book, author={J.C.M. Baeten and W.P. Weijland}, title={Process Algebra}, publisher={Cambridge University Press}, series={Cambridge Tracts in Theoretical Computer Science}, volume={18}, year={1990}} @proceedings{dan97:wc, title={Proceedings of the Second ACM SIGPLAN Workshop on Continuations}, series={BRICS Notes}, number={NS-96-13}, editor={O. Danvy}, year={1996}} @book{ung:book, author={A. Ungar}, title={Normalization, cut-elimination and the theory of proofs}, publisher={Center for the Study of Language and Information, Stanford, CA.}, series={Lecture Notes}, number={28}, year={1992}} @incollection{coq:ccc, author={T. Coquand}, title={Computational Content of Classical Proofs}, year={1997}, booktitle={Proceedings of the {CLICS} Summer School}, editor={P. Dybjer and A. Pitts}, publisher={Cambridge University Presss}} @INCOLLECTION{HL91:otrs, AUTHOR = "Huet, G. and L{\'e}vy, J.-J.", TITLE = "Computations in Orthogonal Rewriting Systems, {I} and {II}", BOOKTITLE = "Computational Logic: Essays in honor of Alan Robinson", PUBLISHER = {The MIT Press}, YEAR = 1991, EDITOR = "Lassez, J-L. and Plotkin, G.", PAGES = "395--443"} @incollection{lam80:cur, AUTHOR = "J. Lambek", TITLE = "From $\lambda$-calculus to cartesian closed categories", BOOKTITLE = "To {H}.{B}. {C}urry: Essays on Combinatory Logic, Lambda Calculus and Formalism", EDITOR = "J.R. Hindley and J.P. Seldin", PUBLISHER = "Academic Press", YEAR = 1980, pages={375--402}} @BOOK{MTH91:book, AUTHOR = "R. Milner and M. Tofte and R. Harper", TITLE = "The Definition of Standard {ML}", PUBLISHER = "The MIT Press", YEAR = 1991} @BOOK{thomas:book, AUTHOR = "Th. Streicher", TITLE = "Semantics of Type Theory. Correctness, Completeness and Independence results", PUBLISHER = "Birkh{\"a}user", SERIES = "Progress in Theoretical Computer Science", YEAR = 1991} @incollection{coq90:lacs, author={T. Coquand}, title={Metamathematical investigations of a calculus of Constructions}, pages={91-122}, booktitle={Logic and Computer Science}, editor={P. Odifreddi}, year={1990}, publisher={Academic Press}} @InCollection{god:T, author = "K. Godel", title = "On intuitionistic arithmetic and number theory", pages = "75--81", editor = "{M. Davis}", booktitle = "The Undecidable", publisher = "Raven Press", year = "1965", } @book{AC:book, author={M. Abadi and L. Cardelli}, title={A theory of objects}, publisher={Springer-Verlag}, year={1996}} @book{jw80:crs, author={J.W. Klop}, title={Combinatory reduction systems}, institution={CWI, Amsterdam}, year={1980}, number={127}, series={Mathematical Centre Tracts}, publisher={CWI}} @BOOK{GLT:book, AUTHOR = "J.-Y. Girard and Y. Lafont and P. Taylor", TITLE = "Proofs and {T}ypes", PUBLISHER = "Cambridge University Press", YEAR = 1989, SERIES = "Tracts in Theoretical Computer Science", NUMBER = 7} @INCOLLECTION{MG85, AUTHOR = "J. Meseguer and J. Goguen", TITLE = "Initiality, induction and computability", BOOKTITLE = "Algebraic Methods in Semantics", EDITOR = "M. Nivat and J. Reynolds", PUBLISHER = "Cambridge University Press", PAGES = "459--541", YEAR = 1985} @INCOLLECTION{jw:handbook , AUTHOR = {J.W. Klop} , TITLE = {Term-rewriting systems} , BOOKTITLE = {Handbook of Logic in Computer Science} , EDITOR = {S. Abramsky and D. M. Gabbay and T.S.E. Maibaum} , PUBLISHER = {Oxford Science Publications} , CROSSREF = {AGM} , YEAR = 1992 , PAGES = {1-116} , note={Volume 2}} @incollection{GMNS, author={G. Smolka and W. Nutt and J. Goguen and J. Meseguer}, title={Order-Sorted Equational Computation}, editor={H. Ait-Kaci and M. Nivat}, booktitle={Resolution of Equations in Algebraic Structures}, Volume={2: Rewriting techniques}, pages = "299--367", publisher={Academic Press}, year={1989}} @InCollection{constructor, author = "L. Helmink", title = "Goal Directed Proof Construction In Type Theory", booktitle = "Logical Frameworks", publisher = "Cambridge University Press", year = "1991", editor = "G. Huet and G. Plotkin", note = "Proceedings of the Second Workshop of the {ESPRIT BRA} on Logical Frameworks"} @InCollection{Jones:reals, author = "C. Jones", title = "Completing the Rationals and Metric Spaces in {LEGO}", booktitle = "Logical Environments", year = "1993", editor = "G. Huet and G. Plotkin", pages = "297--316", publisher = "Cambridge University Press", note = "Proceedings of the Second Workshop of the {ESPRIT BRA} on Logical Frameworks" } @Book{app:book, author = {Appel, A.}, title = {Compiling with Continuations}, publisher = {Cambridge University Press}, year = 1992 } @incollection{ter:vd, author={J. Terlouw}, title= {Strong normalisation in type systems: a model-theoretical approach}, booktitle={Dirk van Dalen Festschrift}, editors={H. Barendregt and M. Bezem and J.W. Klop}, publisher={University of Utrecht}, pages={161-190}, note={To appear in Annals of Pure and Applied Logic}, year={1993}} @incollection{rez:vd, author={A. Rezus}, title= {Beyond {BHK}}, booktitle={Dirk van Dalen Festschrift}, editors={H. Barendregt and M. Bezem and J.W. Klop}, publisher={University of Utrecht}, pages={114--120}, year={1993}} @BOOK{pra65:book , AUTHOR = {Prawitz, D.} , TITLE = {Natural Deduction: A proof theoretical study} , PUBLISHER = {Almquist \& Wiksell} , YEAR = 1965 } @INCOLLECTION{henk:handbook , AUTHOR = {H. Barendregt} , TITLE = {Lambda Calculi with Types} , BOOKTITLE = {Handbook of Logic in Computer Science} , EDITOR = {S. Abramsky and D. M. Gabbay and T.S.E. Maibaum} , PUBLISHER = {Oxford Science Publications} , CROSSREFONLY = {AGM} , YEAR = 1992 , PAGES = {117--309} , note={Volume 2}} @incollection{dBr:role, crossref={louvain:CH}, author={N.G. de Bruijn}, title= {On the roles of types in mathematics}, pages={27-54}, editor={{P. de Groote}}, booktitle={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @incollection{vernacular, crossref={automath}, author={N.G. de Bruijn}, title= {The mathematical vernacular, a language for mathematics with typed sets}, booktitle={Selected papers on {Automath}}, pages={865-935}} @incollection{herman:louvain, crossref={louvain:CH}, author={H. Geuvers}, title= {{The Calculus of Constructions and higher-order logic}}, pages={139-192}, editor={{P. de Groote}}, booktitle={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @incollection{jut, crossref={automath}, author={L.S. van Benthem Jutting}, title={{Checking Landau's ``Grundlagen'' in the {Automath} system. Parts of Chapter 0,1, and 2. (Introduction, Preparation and Translation)}}, pages={701-720}} @incollection{zuc:classical, crossref={automath}, author={J. Zucker}, title={Formalisation of classical mathematics in {Automath}}, pages={127-140}} @incollection{zuc:analysis, crossref={automath}, author={L.S. van Benthem Jutting}, title={A text fragment from Zucker's real analysis}, pages={733-762}} @incollection{Gal:red, author={J. Gallier}, title={{On Girard's \lq\lq candidats de r\'educibilit\'e\rq\rq}}, booktitle={Logic and Computer Science}, editor={P. Odifreddi}, pages={123-203}, year={1990}, publisher={Academic Press}} @INCOLLECTION{howard:iso , AUTHOR = {W.A. Howard} , TITLE = {The formulae-as-types notion of construction} , BOOKTITLE = {Essays on Combinatory Logic, Lambda Calculus and Formalism} , EDITOR = {J.R. Hindley and J.P. Seldin} , PUBLISHER = {Academic Press} , CROSSREF = {curry:book} , YEAR = 1980 , PAGES = {479-490} } @incollection{DJ:handbook, author={N. Dershowitz and J-P. Jouannaud}, title={Rewrite systems}, editor={J. van Leeuwen}, booktitle={Formal models and semantics. Handbook of Theoretical Computer Science}, volume={B}, pages={243-320}, year={1990}, publisher={Elsevier}} @book{PE93, author={Plasmeijer, M.J. and van Eekelen, M.C.J.D.}, title={Functional Programming and Parallel Graph Rewriting}, publisher={Addison-Wesley Publishing Company}, year={1993}} @Book{luo:book, author = "Z. Luo", title = "Computation and Reasoning: A Type Theory for Computer Science", publisher = "Oxford University Press", series = "International Series of Monographs on Computer Science", year = "1994", number = 11 } @book{GM94, author={C.A. Gunter and J.C. Mitchell}, title={Theoretical Aspects of Object-Oriented Programming: Types, Semantics and Language Design}, publisher={{The MIT Press}}, year={1994}} @book{Mel:hol, author={T. Melham}, title={Higher Order Logic and Hardware Verification}, series={Tracts in Theoretical Computer Science}, volume={31}, publisher={Cambridge University Press}, year={199?}} @book{henk:book, author="H. Barendregt", title="The Lambda Calculus: Its Syntax and Semantics", edition="revised", publisher="North-Holland", year=1984, series="Studies in Logic and the Foundations of Mathematics", volume=103 } @book{Coh, author={P. Cohn}, title={Universal algebra}, publisher={D. Reidel}, series={Mathematics and its Applications}, volume={6}, year={1981}} @Book{hol, title = "Introduction to {HOL}: {A} theorem proving environment for higher-order logic", publisher = "Cambridge University Press", year = "1993", editor = "M.J.C. Gordon and T.F. Melham" } @book{ML:book, author="P. {Martin-L\"of}", title="Intuitionistic Type Theory", publisher="Bibliopolis", address="Naples", year=1984, series="Studies in Proof Theory", volume=1 } @unpublished{bart:book, author={B. Jacobs}, title={Categorical logic and type theory}, year={199x}, note={Book. In preparation}} @book{NPS:book, author = "B. Nordstr{\"{o}}m and K. Petersson and J. Smith", title = "Programming in {M}artin-L{\"{o}}f's Type Theory. An Introduction", publisher = "Oxford University Press", series= {International Series of Monographs on Computer Science}, number= 7, year = 1990 } @book{Wik87, author={A. Wikstr{\"o}m}, title={Functional Progrmmaming using Standard {ML}}, year={1987}, publisher={Prenctice Hall}, series={Interntional Series in Computer Science}} @book{ bis67, author="E. Bishop", title="Foundations of Constructive Analysis", publisher="McGraw-Hill", address="New York", year=1967, } @Book{nqthm, author = "R.S. Boyer and J.S. Moore", title = "A Computational Logic Handbook", publisher = "Academic Press", year = 1988 } @BOOK{nuprl , AUTHOR = "R.L. Constable and S.F. Allen and H.M. Bromley and W.R. Cleaveland and J.F. Cremer and R.W. Harper and D.J. Howe and T.B. Knoblock and N.P. Mendler and P. Panangaden and J.T. Sasaki and S.F. Smith" , TITLE = "Implementing Mathematics with the {N}u{P}rl Development System" , PUBLISHER = "Prentice-Hall, Inc." , YEAR = 1986 } @BOOK{maclane , AUTHOR = "S. Mc Lane" , TITLE = "Categories for the Working Mathematician" , PUBLISHER = springer , ADDRESS = "Berlin" , YEAR = {1971} } @BOOK{AGM , EDITOR = {S. Abramsky and D. Gabbay and T. Maibaum} , TITLE = {Handbook of Logic in Computer Science} , PUBLISHER = {Oxford Science Publications} , CROSSREFONLY = 1 , YEAR = 1992} @book{galois, author={I. Stewart}, title={Galois theory}, publisher={Chapman and Hall}, year={1989}, edition={second}} @book{automath , Editor={R. Nederpelt and H. Geuvers and R. de Vrijer} , Title={Selected papers on {Automath}} , publisher="North-Holland", address="Amsterdam", year=1994, series="Studies in Logic and the Foundations of Mathematics", volume=133 } @book{ontic, author={D.A. McAllester}, title={{ONTIC: A Knowledge Representation System for Mathematics}}, publisher={{MIT} Press}, year={1989}} @book{axiom, author={R.D. Jenks and R.S. Sutor}, title={{AXIOM: The Scientific Computation System}}, publisher=springer, year={1992}} @BOOK{curry:book , EDITOR = {J.R. Hindley and J.P. Seldin} , TITLE = {Essays on Combinatory Logic, Lambda Calculus and Formalism} , PUBLISHER = {Academic Press} , ADDRESS = {London} , YEAR = 1980 , CROSSREFONLY = 1 } @book{RW, author={Whitehead, A.N. and Russell, B.}, title={{Principia Mathematica}}, publisher={Cambridge University Press}, year={1910--1913}, volume={1-3}} @book{louvain:CH, editor={de Groote, P.}, title={{The Curry-Howard isomorphism}}, publisher={{Universite catholique de Louvain}}, year={1995}, volume={8}, series={{Cahiers du centre de logique}}} @InCollection{tur90:miranda, author = {Turner, D.}, title = {An Overview of {M}iranda}, crossref = {tur90:book} } @BOOK{tur90:book , EDITOR = {Turner, D.} , BOOKTITLE = {Research Topics in Functional Programming} , PUBLISHER = {Addison-Wesley} , YEAR = 1990 } @BOOK{PD:book, EDITOR={A.~Pitts and P.~Dybjer}, TITLE={Semantics and Logics of Computation}, PUBLISHER={Cambridge University Press}, SERIES={Publications of the Isaac Newton Institute}, YEAR=1997 } @InProceedings{pip95:lics, title={Normalization and Extensionality (Extended Abstract)}, author={A. Piperno}, pages={300--310}, year={1995}, booktitle={Proceedings of LICS'95} } @InProceedings{see87:lics, author={R. Seely}, title={Modelling Computations: A 2-Categorical Framework}, pages={65--71}, booktitle={Proceedings of LICS'87}, publisher={IEEE Computer Society Press}, year={1987} } @inproceedings{HS97:lics, title={Continuation Models are Universal for $\lambda\mu$-calculus}, author={M. Hofmann and T. Streicher}, booktitle={Proceedings of LICS'97}, publisher={IEEE Computer Society Press}, year={1997}, note={To appear}} @inproceedings{wel94:lics, title={Typability and Type-Checking in the Second-Order $\lambda$-Calculus are Equivalent and Undecidable}, author={J.B. Wells}, pages={176--185}, booktitle={Proceedings of LICS'94}, publisher={IEEE Computer Society Press}, year={1994}} @Inproceedings{OS97:popl, author = "C.-H.L. Ong and C.A. Stewart", title = "A {Curry-Howard Foundation} for functional computation with control", booktitle ={Proceedings of POPL'97}, publisher ={ACM Press}, pages={??--??}, year ="1997"} @Inproceedings{sai97:popl, author = "A. Saibi", title = "Typing Algorithm in Type Theory with Inheritance", booktitle ={Proceedings of POPL'97}, publisher ={ACM Press}, pages={??--??}, year ="1997"} @inproceedings{sel91:plt, author={J. Seldin}, title={Excluded Middle and Definite Descriptions in the Theory of Constructions}, booktitle={Proceedings of the First Montreal Workshop on Programming Language Theory}, editors={M. Okada and P. Scott}, pages={74--83}, year={1991}} @InProceedings{HL93:popl, title={Explicit Polymorphism and {CPS} Conversion}, author={R. Harper and M. Lillibridge}, booktitle={Proceedings of POPL'93}, pages={206--219}, year={1993}, publisher={ACM Press}} @InProceedings{fel88:popl, title={The Theory and Practice of First-Class Prompts}, author={M. Felleisen}, booktitle={Proceedings of POPL'88}, pages={180--190}, year={1988}, publisher={ACM Press} } @inproceedings{DL92:lfp, author={O. Danvy and J. Lawall}, title={Back to direct style {II}: First-class continuations}, booktitle={Proceedings of LFP'92}, year={1992}, pages={299-310}, publisher={ACM Press} } @InProceedings{HS94:lics, title={The Groupoid Model Refutes Uniqueness of Identity Proofs}, author={Martin Hofmann and Thomas Streicher}, pages={208--212}, booktitle={Proceedings of LICS'94}, year={1994}, publisher = "IEEE Computer Society Press", } @InProceedings{HD94:popl, title={A Generic Account of Continuation-Passing Styles}, author={J. Hatcliff and O. Danvy}, pages={458--471}, year={1994}, booktitle={Proceedings of POPL'94}, publisher={ACM Press}} @InProceedings{gri90:popl, title={A Formulae-as-Types Notion of Control}, author={T. Griffin}, year={1990}, pages={47--58}, booktitle={Proceedings of POPL'90}, publisher={ACM Press}} @InProceedings{chet91:lics, author={C. Murthy}, title={An Evaluation Semantics for Classical Proofs}, pages={96--107}, booktitle={Proceedings of LICS'91}, publisher = "IEEE Computer Society Press", year={1991}} @InProceedings{DHM91:popl, title={Typing First-Class Continuations in {ML}}, author={B.F. Duba and R. Harper and D. MacQueen}, booktitle={Proceedings of POPL'91}, pages={163--173}, year={1991}, publisher={ACM Press} } @InProceedings{par93:lics, title={Strong Normalization for Second Order Classical Natural Deduction}, author={M. Parigot}, pages={39--46}, booktitle={Proceedings of LICS'93}, publisher = "IEEE Computer Society Press", year={1993}} @inproceedings (car88:popl, author = "L. Cardelli", title = "Structural Subtyping and the Notion of Power Type", booktitle = "Proceedings of POPL'88", year = 1988, pages = "70-79", publisher={ACM Press}) @inproceedings (CCHMO89:fpca, author = "P. Canning and W. Cook and W. Hill and J. Mitchell and W. Olthoff", title = "F-Bounded Quantification for Object-Oriented Programming", booktitle = "Proceedings of FPCA'89", year = "1989", pages = "273--280") @InProceedings{peter91:lics, author = "P. Aczel", title = "Term Declaration Logic and Generalised Composita", booktitle = "Proceedings of LICS'91", publisher = "IEEE Computer Society Press", year = "1991", pages = "22--30"} @InProceedings{GM87:lics, author = "J. Goguen and J. Meseguer", title = "Order-Sorted Algebra solves the Constructor-Selector, Multiple", pages = "18--29", booktitle = "Proceedings of LICS'86", year = "1986", publisher = "IEEE Computer Society"} @InProceedings{adriana96:lics, author={D. Aspinall and A. Compagnoni}, title={Subtyping Dependent Types}, booktitle = "Proceedings of LICS'96", publisher = "IEEE Computer Society Press", year={1996}, pages={86--97}} @InProceedings{BTKP93:lics, author = "V. Breazu-Tannen and D. Kesner and L. Puel", title = "A Typed Pattern Calculus", booktitle = "Proceedings of LICS'93", publisher = "IEEE Computer Society Press", year = 1993, } @InProceedings(obj2 ,Author="K. Futatsugi and J. Goguen and J.-P. Jouannaud and J. Meseguer" ,Title="Principles of {OBJ}2." ,Booktitle="Proceedings of POPL'85" ,Editor="B. Reid" ,Pages="52--66" ,Year=1985 ,publisher={ACM Press}) @inproceedings{JO91:lics, author={J.-P. Jouannaud and M. Okada}, title={Executable higher-order algebraic specification languages}, booktitle={Proceedings of LICS'91}, pages={350-361}, publisher = "IEEE Computer Society Press", year={1991}} @inproceedings{pfe89:lics, author = "F. Pfenning", title="Elf: A Language for Logic Definition and Verified Metaprogramming", booktitle="Proceedings of LICS'89", publisher = "IEEE Computer Society Press", year=1989 } @inproceedings{HHP87:lics, author="R. Harper and F. Honsell and G. Plotkin", title="A Framework for Defining Logics", booktitle="Proceedings of LICS'87", year=1987, pages="194--204", publisher = "IEEE Computer Society Press"} @inproceedings{mid89:lics, author={A. Middeldorp}, title={A sufficient condition for the termination of the direct sum of term-rewriting systems}, booktitle={Proceedings of LICS'89}, pages={396-401}, year={1989}, publisher="IEEE Computer Society Press"} @inproceedings{WB89, author={P. Wadler and S. Blott}, title={How to make ad hoc polymorphism less ad hoc}, year={1989}, pages={60-76}, booktitle={Proceedings of POPL'89}, publisher={ACM Press}} @inproceedings{BT88:lics, author={V. Breazu-Tannen}, title={Combining algebra and higher-order types}, booktitle={Proceedings of LICS'88}, year={1988}, publisher = "IEEE Computer Society Press", pages={82-90}} @inproceedings{tai75:lc, author={W. Tait}, title={A realisability interpretation of the theory of species}, booktitle={Logic Colloquium 73}, editor={R. Parikh}, pages={240-251}, series=lnm, volume={453}, year={1975}} @inproceedings{coq92:bra, author={T. Coquand}, title={Pattern Matching in Type Theory}, booktitle={Informal proceedings of LF'92}, editor={B. Nordstr\"om}, pages={66-79}, note={Available from http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, year={1992}} @inproceedings{CS93:bra, author={T. Coquand and J. Smith}, title={The Status of Pattern Matching in Type Theory}, booktitle={Informal proceedings of {TYPES}'93}, editor={H. Geuvers}, pages={??-??}, note={Available from http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, year={1993}} @InProceedings{pfe93:bra, author = "F. Pfenning", title = "Refinement Types for Logical Frameworks", booktitle = "Informal Proceedings of TYPES'93", editor = "H. Geuvers", year = "1993", pages = "285--299", note = "Available from http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html"} @inproceedings{BFG94:lics, author={F. Barbanera and M. Fern{\'a}ndez and H. Geuvers}, title={Modularity of strong normalisation and confluence in the algebraic $\lambda$-cube}, booktitle={Proceedings of LICS'94}, pages={406-415}, publisher={IEEE Computer Society Press}, year={1994}} @inproceedings{GW94:lics, author={H. Geuvers and B. Werner}, title={On the {Church-Rosser} property for expressive type systems and its consequence for their metatheoretic study}, booktitle={Proceedings of LICS'94}, pages={320-329}, publisher={IEEE Computer Society Press}, year={1994}} @inproceedings{randy:imp, author = "R. Pollack", title = "Implicit Syntax", booktitle = "Informal Proceedings of First Workshop on Logical Frameworks, Antibes", year = "1990", month = "May", editor={G. Huet and G. Plotkin}} @inproceedings{AC91:popl, author={R. Amadio and L. Cardelli}, title={Subtyping recursive types}, booktitle={Proceedings of POPL'91}, year={1991}, publisher={ACM Press}, pages={104--118}} @inproceedings{mit90:popl, author={J. Mitchell}, title={Towards a typed foundation for method specialisation and inheritance}, booktitle={Proceedings of POPL'90}, year={1990}, publisher={ACM Press}, pages={109--124}} @inproceedings{BM92:popl, author={K. Bruce and J. Mitchell}, title={{PER} models of subtyping, recursive types and higher-order polymorphism}, booktitle={Proceedings of POPL'92}, year={1992}, publisher={ACM Press}, pages={316-327}} @inproceedings{DHW93:bra, author={G. Dowek and G. Huet and B. Werner}, title={On the existence of long $\beta\eta$-normal forms in the cube}, booktitle="Informal Proceedings of TYPES'93", year = "1993", pages={115-130}, note={Available from http://www.dcs.ed.ac.uk/lfcsinfo/research/types-bra/proc/index.html}, editor={H. Geuvers}} @inproceedings{zan91:csn, author={H. Zantema}, title={Termination of term-rewriting: from many-sorted to one-sorted}, booktitle={Proceedings of CSN'91}, pages={617-629}, editor={J. van Leeuwen}, year={1991}, note={Also appeared as report RUU-CS-91-18, University of Utrecht}} @inproceedings{BHC, author={C. Ballarins and K. Homann and J. Calmet}, title={Theorems and algorithms: an interface between Maple and Isabelle}, booktitle={Proceedings of ISSAC'95}, year={1995}} @inproceedings{Kaj92:issac, author={N. Kajler}, title={{CAS/PI}: a portable and extensible interface for computer algebra systems}, year={1992}, booktitle={Proceedings of ISSAC'92}, pages={376-386}} @PhdThesis{judith:thesis, author = {Underwood, J.L.}, title = {Aspects of the Computational Content of Proofs}, school = {Cornell University}, year = 1994 } @phdthesis{jasper:thesis, author={J. Kamperman}, title={Efficient compilation of term-rewriting systems}, year={1996}, school={University of Amsterdam}} @phdthesis{jaco:thesis, author={Pol, J. van de}, title={Termination of higher-order rewrite systems}, year={1996}, school={University of Utrecht}} @phdthesis{see:thesis, author={R. Seely}, title={Hyperdoctrines and natural deduction}, year={1977}, school={University of Cambridge}} @phdthesis{hugo:thesis, author={H. Elbers}, title={Thesis}, school={Technische Universiteit Eindhoven}, year={1998}, note={Forthcoming}} @book{SS:thesis, author={M. Schmidt-Schau{\ss}}, title={Computational Aspects of Order-Sorted Logic with Term Declarations}, series=lnai, publisher=springer, volume={395}, year={1989}} @PhDThesis{Simons:Thesis, author = "M. Simons", title = "The Presentation of Formal Proofs", school = "Technische Universität Berlin", year = 1996 } @mastersthesis{oostdijk:msc, author={M. Oostdijk}, title={Proofs by calculation}, school={University of Nijmegen}, year={1996}} @mastersthesis{mark:msc, author={M. Ruys}, title={{$\lambda P\omega$ is not conservative over $\lambda P2$}}, school={University of Nijmegen}, year={1991}} @PHDTHESIS{eduardo:thesis , AUTHOR = {Gimenez, E.} , TITLE = {?? coinductives } , SCHOOL = {Universit\'e de ??} , YEAR = {1996} } @PHDTHESIS{samuel:thesis , AUTHOR = {Boutin, S.} , TITLE = {Reflexions sur les types de quotients} , SCHOOL = {Universit\'e de Paris} , YEAR = {199x} } @PHDTHESIS{chet:thesis , AUTHOR = {Murthy, C.} , TITLE = {Extracting Constructive Contents from Classical Proofs} , SCHOOL = {Cornell University} , YEAR = 1990 } @phdthesis{koh:thesis, author = {M. Kohlhase}, school = {Universit{\"a}t des Saarlandes}, title = {A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle}, year = {1994}} @phdthesis{stefano:thesis, author={S. Berardi}, title={Type dependence and Constructive Mathematics}, school={University of Torino}, year={1990}} @PHDTHESIS{thomas:thesis, AUTHOR = "Th. Streicher", TITLE = "Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions", SCHOOL = "University of Passau", NOTE = "Appeared as technical report MIP - 8913", YEAR = 1989} @PhdThesis{nederpelt:thesis, author={R. Nederpelt}, title={Strong normalisation in a typed lambda calculus with lambda structured types}, school={Technical University of Eindhoven}, year={1973}} @PhdThesis{paula:thesis, author={P. Severi}, title={Normalisation in lambda calculus and its relation to type inference}, school={Technical University of Eindhoven}, year={1996}} @PhdThesis{alex:thesis, author={A. Sellinx}, title={Computer-aided verification of protocols}, school={University of Utrecht}, year={1996}} @PhdThesis{kesner:thesis, author = "D. Kesner", title = "La d\'efinition de fonctions par cas \`a l'aide de motifs dans des langages applicatifs", school = "Universit\'e Paris-Sud", year = 1993} @Phdthesis{geser:thesis, author={A. Geser}, title={Relative termination}, school={Universiteit Passau}, YEAR = 1990, NOTE = {Appeared as technical report 91-03, Ulmer Informatik-Berichte, Universit{\ä}t Ulm}} @phdthesis{ghe:thesis, author={G. Ghelli}, title={Proof theoretic studies about a minimal type system integrating inclusion and parametric polymorphism}, school={Universit{\`a} di {P}isa}, year={1990}, note={Appeared as technical report TD-6/90, {D}ipartimento di {I}nformatica, Universit{\`a} di {P}isa}} @Phdthesis{adriana:thesis, author={A. Compagnoni}, title={Higher-order subtyping with intersection types}, school={Department of Computer Science, University of Nijmegen}, year={1995}} @Phdthesis{healf:thesis, author={H. Goguen}, title={A typed operational semantics for UTT}, school={Laboratory for the Foundations of Computer Science, University of Edinburgh}, year={1994}} @Phdthesis{thorsten:thesis, author={T. Altenkirch}, title={Constructions, inductive types and strong normalisation}, school={Laboratory for the Foundations of Computer Science, University of Edinburgh}, year={1994}} @Phdthesis{martin:thesis, author={M. Hofmann}, title={Extensional concepts in intensional type theory}, school={Laboratory for the Foundations of Computer Science, University of Edinburgh}, year={1995}} @PhdThesis{randy:thesis, author = "R. Pollack", title = "The Theory of {LEGO}: {A} Proof Checker for the Extended Calculus of Constructions", school = "University of Edinburgh", year = "1994", note = "Available by anonymous ftp from {\tt ftp.cs.chalmers.se} in directory {\tt pub/users/pollack}." } @MastersThesis{bailey:msc, author = "A. Bailey", title = "Representing Algebra in {LEGO}", school = "University of Edinburgh", year = "1993" } @phdthesis{ach:thesis, author={P. Achten}, title={Interactive Functional Programs: models, methods and implementation}, school={University of Nijmegen}, year={1996}} @PHDTHESIS{pau:thesis , AUTHOR = {C. Paulin-Mohring} , SCHOOL = {Universit\'{e} Paris VII} , TITLE = {Extraction des Programmes dans le Calcul des Constructions} , YEAR = 1989 } @phdthesis{herman:thesis, author={H. Geuvers}, title={Logics and type systems}, school={University of Nijmegen}, year={1993}} @phdthesis{gir:thesis, author={J-Y. Girard}, title={{Interpr\'etation fonctionelle et \'elimination des coupures dans l'arithm\'etique d'ordre sup\'erieur}}, school={Universit{\'e} Paris 7}, year={1972}} @phdthesis{wer:thesis, author={B. Werner}, title={{M\'eta-th\'eorie du Calcul des Constructions Inductives}}, school={Universit{\'e} Paris 7}, year={1994}} @phdthesis{maribel:thesis, author={M. Fernandez}, title={Mod{\`e}les de calcul multiparadigmes fond{\'e}s sur la r{\'e\'e}criture}, school={{Universit\'e Paris-Sud Orsay}}, year={1993}} @phdthesis{jones:thesis, author={M. Jones}, title={Qualified types: theory and practice}, school={Oxford University}, year={1992}, note={ Appeared as technical monograph PRG-106}} @phdthesis{jackson:thesis , Author={P. Jackson} , Title={Enhancing the {Nuprl} proof development system and applying it to computational abstract algebra} , School={Department of Computer Science, Cornell University} , year={1995} , month={January} } @phdthesis{howe:thesis, Author={D. Howe}, title={ Automating reasoning in an implementation of constructive type theory}, School={Department of Computer Science, Cornell University}, year={1988}} @MastersThesis{gustavo:thesis, Author={G. Betarte}, title={A machine-assisted proof that the integers form an integral domain}, school={Department of Computer Science, Chalmers University}, year={1993}} @phdThesis{lena:thesis, Author={L. Magnusson}, title={The implementation of {ALF}: a proof editor based on {Martin-L\"of's} monomorphic type theory with explicit substitution}, school={Department of Computer Science, Chalmers University}, year={1994}} @phdthesis{mid:thesis, author={A. Middeldorp}, title={Modular properties of term-rewriting systems}, school={Department of Computer Science, Vrije Universiteit, Amsterdam}, year={1990}} @phdthesis{her:thesis, author={H. Herbelin}, title={S{\'e}quents qu'on calcule}, school={Universit{\'e} Paris 7}, year={1995}}