@unpublished{gf05:ni, author = {G. Barthe and F. Kamm\"uller}, title = {{Certified bytecode verifier for non-interference}}, year = {2005}, note={Manuscript}} @TECHREPORT{BaPiRe06:longreport, AUTHOR = {G. Barthe and D. Pichardie and T. Rezk}, TITLE = {Non-Interference for low level languages}, NOTE = {\url{http://hal.inria.fr/inria-00106182}}, INSTITUTION = {INRIA}, YEAR = 2006 } @PHDTHESIS{Rezk:phd, TITLE = {Verification of confidentiality policies for mobile code}, AUTHOR = {T. Rezk}, YEAR = {2006}, SCHOOL = {Universit\'e de Nice Sophia-Antipolis} } @unpublished{BRRS07, TITLE = {Security of Multithreaded Programs by Compilation}, AUTHOR = {G. Barthe and T. Rezk and A. Russo and A. Sabelfeld}, note={Manuscript}, year={2007} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % PROCEEDINGS % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @INPROCEEDINGS{BPR07:esop, TITLE = {A Certified Lightweight Non-Interference Java Bytecode Verifier}, AUTHOR = {G. Barthe and D. Pichardie and T. Rezk}, BOOKTITLE = {European Symposium on Programming}, YEAR = {2007}, EDITOR = {R. De Niccola}, SERIES = lncs, publisher=springer, volume={4xxx}, pages={xxx} } @INPROCEEDINGS{g+06:flops, AUTHOR = {G. Barthe and J. Forest and D. Pichardie and V. Rusu}, TITLE = {{Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant}}, PAGES = {114-129}, BOOKTITLE = {Proceedings of FLOPS'06}, YEAR = 2006, PUBLISHER = {Springer-Verlag}, SERIES = {Lecture Notes in Computer Science}, VOLUME = 3945, EDITOR = {M. Hagiya and P. Wadler} } @InProceedings{gdt06:sp, author = {G. Barthe and D. Naumann and T. Rezk}, title = {{Deriving an Information Flow Checker and Certifying Compiler for Java}}, booktitle = {Symposium on Security and Privacy, 2006}, pdfurl = {http://mobius.inria.fr/twiki/pub/Publications/WebHome/Barthe-Naumann-Rezk-SP06.pdf}, year = {2006}, publisher = {IEEE Press} } @inproceedings{gta05:fast, author = {G. Barthe and T.Rezk and A. Saabas}, title = {{Proof obligations preserving compilation}}, year = {2005}, booktitle="Proceedings of FAST'05", OPTeditor="T.~Dimitrakos and F.~Martinelli and P.~Ryan and S.~Schneider", series=lncs, volume={3866}, pages="112-126", publisher=springer} @inproceedings{gg05:fosad, author = {G. Barthe and G. Dufay}, title = {{Formal methods for smartcard security}}, year = {2005}, booktitle="Proceedings of FOSAD'05", editor="A.~Aldini and R.~Gorrieri and F.~Martinelli", series=lncs, volume={3xxx}, publisher=springer} @inproceedings{gmg05:sefm, author = {G. Barthe and M. Pavlova and G. Schneider}, title = {{Precise analysis of memory consumption using program logics}}, year = {2005}, booktitle="Proceedings of SEFM'05", editor="B.~Aichernig and B.~Beckert", publisher="IEEE Press"} @inproceedings{gtm05:qapl, author = {G. Barthe and T. Rezk and M. Warnier}, title = {{Preventing timing leaks through transactional branching instructions}}, year = {2005}, booktitle={Proceedings of {QAPL}'05}, editor={A. Cerone and H. Wiklicky}, publisher=elsevier, series=entcs, note={To appear}} @inproceedings{gbf05:tlca, author={G. Barthe and B. Gr\'egoire and F. Pastawski}, title={Practical inference for typed-based termination in a polymorphic setting}, year={2005}, booktitle={Proceedings of {TLCA}'05}, editor={P. Urzyczyn}, publisher=springer, series=lncs, volume=3641, pages={71-85}} @inproceedings{gt05:tldi, author={G. Barthe and T. Rezk}, title={Non-interference for a {JVM}-like language}, year={2005}, booktitle={Proceedings of {TLDI}'05}, editor={M. F\"ahndrich}, publisher={ACM Press}, pages={103--112}} @inproceedings{gpt04:csfw, author={G. Barthe and P. D'Argenio and T. Rezk}, title={{Secure Information Flow by Self-Composition}}, editor={R. Foccardi}, booktitle={Proceedings of CSFW'04}, pages={100-114}, publisher={IEEE Press}, year={2004}} @inproceedings{gjs04:ijcar, author = {G. Barthe and J. Cederquist and S. Tarento}, title = {{A Machine-Checked Formalization of the Generic Model and the Random Oracle Model}}, year = {2004}, booktitle={Proceedings of IJCAR'04}, editor={D. Basin and M. Rusinowitch}, series=lncs, volume={3097}, pages={385-399}} @inproceedings{mariela+04:cardis, author={M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet}, title={Enforcing High-Level Security Properties For Applets}, editor={P. Paradinas and J.-J. Quisquater}, booktitle={{Proceedings of CARDIS'04}}, publisher={Kluwer}, year={2004}, pages={}} @inproceedings{gl04:fmse, author={G. Barthe and L. Prensa-Nieto}, title={Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems}, booktitle={Proceedings of FMSE'04}, editor={M. Backes and D. Basin and M. Waidner}, publisher={ACM Press}, year={2004}, pages={13-22}} @inproceedings{gg04:fase, author ={G. Barthe and G. Dufay}, title = {{A Tool-Assisted Framework for Certified Bytecode Verification}}, year = {2004}, booktitle={Proceedings of {FASE}'04}, series=lncs, publisher=springer, volume={2984}, pages={99-113}, editors={M. Wermelinger and T. Margaria-Steffen}} @inproceedings{gat04:vmcai, author={G. Barthe and A. Basu and T. Rezk}, title={Security Types Preserving Compilation}, year={2004}, booktitle={Proceedings of {VMCAI}'04}, series=lncs, publisher=springer, volume={2934}, editor="B. Steffen and G. Levi", pages={2--15}} @inproceedings{gs03:rta, author = {G. Barthe and S. Stratulat}, title = {{Using Implicit Induction Techniques for the Validation of the JavaCard Platform}}, year = {2003}, booktitle={Proceedings of RTA'03}, editor={R. Nieuwenhuis}, series=lncs, Publisher=springer, volume={2706}, pages={337 - 351}} @inproceedings{g+03:popl, author={G. Barthe and H. Cirstea and C. Kirchner and L. Liquori}, title={Pure Pattern Type Systems}, booktitle={Proceedings of POPL'03}, year={2003}, editor={ACM Press}} @inproceedings{g+02:amast, author = {G. Barthe and P. Courtieu and G. Dufay and S. Melo de Sousa}, title = {{Tool-Assisted Specification and Verification of the JavaCard Platform}}, booktitle={Proceedings of AMAST'02}, editor={H. Kirchner and C. Ringessein}, series=lncs, year = {2002}, Publisher=springer, volume={2422}, pages={41--59}} @inproceedings{gt00:appsem, author = {G. Barthe and T. Coquand}, title = {{An Introduction to Dependent Type Theory}}, booktitle = {Applied Semantics. Lecture Notes for the APPSEM Summer School}, year = {2002}, editor={G. Barthe and P. Dybjer and L. Pinto and J. Saraiva}, series=lncs, Publisher=springer, volume={2395}, pages={1--41}} @inproceedings{gp02:tphols, author = {G. Barthe and P. Courtieu}, title = {{Efficient Reasoning about Executable Specifications in Coq}}, booktitle={Proceedings of TPHOLs'02}, editor={V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar}, series=lncs, year = {2002}, Publisher=springer, volume={2410}, pages={31--46}} @inproceedings{g+02:vmcai, author = {G. Barthe and G. Dufay and L. Jakubiec and S. Melo de Sousa}, title = {{A formal correspondence between offensive and defensive JavaCard virtual machines}}, year = {2002} , Booktitle={Proceedings of VMCAI'02} , Publisher=springer , series= lncs , volume= {2294} , Editor= {A. Cortesi} , pages={32--45}} @inproceedings{gt02:pepm, author ={G. Barthe and T. Uustalu}, title = {CPS Translating Inductive and Coinductive Types}, editor={P. Thiemann}, booktitle={Proceedings of PEPM'02}, publisher={ACM Press}, year ={2002} } @inproceedings{gb01:agp, author = {G. Barthe and B. Ruiz Jiménez}, title = {Principal types and semi-full closure for Extended Pure Type Systems (In Spanish)}, year = {2001} , Booktitle={Proceedings of AGP'01} , Editor={L. Moniz Pereira and P. Quaresma} } @inproceedings{gdm01:ftfjp, author = {G. Barthe and D. Gurov and M. Huisman}, title = {{Compositional specification and verification of control flow based security properties of multi-application programs}}, year = {2001} , Booktitle={Proceedings of FTfJP'01} , Editor= {S. Drossopoulou et al} } @inproceedings{g+01:esmart, author = {G. Barthe and G. Dufay and M. Huisman and S. Melo de Sousa}, title = {{Jakarta: a toolset to reason about the JavaCard platform}}, year = {2001} , Booktitle={Proceedings of e-SMART'01} , Publisher=springer , series= lncs , volume= {2140} , pages={2--18} , editor= {I. Attali and T. Jensen} } @inproceedings{go01:fossacs, author = {G. Barthe and O. Pons}, title = {{Type Isomorphisms and Proof Reuse in Dependent Type Theory}}, year = {2001} , Booktitle={Proceedings of {FOSSACS}'01} , Publisher=springer , series= lncs , volume= {2030} , Editor= {F. Honsell and M. Miculan} , pages={57--71} } @inproceedings{g+01:esop, author = {G. Barthe and G. Dufay and L. Jakubiec and B. Serpette and S. Melo de Sousa}, title = {{A Formal Executable Semantics of the JavaCard Platform}}, year = {2001} , Booktitle={Proceedings of ESOP'01} , Publisher=springer , series= lncs , volume= {2028} , Editor= {D. Sands} , pages={302--319}} @InProceedings{gb00:lpar , Author ={G. Barthe and B. Serpette} , Title={Static Reduction Analysis for Imperative Object Oriented Languages} ,Booktitle={Proceedings of LPAR'00} , Year= 2000 , Publisher=springer , series= lncs , volume= {1955} , Editor= {M. Parigot and A. Voronkov} , pages={344--361}} @INPROCEEDINGS{g+00:ftfjp, AUTHOR = {Barthe, G. and Dufay, G. and Jakubiec, L. and Serpette, B. P. and Sousa, S. Melo de and Yu, S.-W.} , Title={{Formalisation of the Java Card Virtual Machine in Coq}} , Booktitle={Proceedings of FTfJP'00---ECOOP Workshop on Formal Techniques for Java Programs} , editor={Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.} , Year= 2000} @INPROCEEDINGS{gf00:fossacs , AUTHOR = {Barthe, G. and Raamsdonk, F. van} , Title={Constructor Subtyping in the Calculus of Inductive Constructions} , Booktitle={Proceedings of {FOSSACS}'00} , Year= 2000 , Publisher=springer , series= lncs , volume= {1784} , Editor= {J. Tuyrin} , pages={17--34}} @InProceedings{gb99:flops , Author ={G. Barthe and B. Serpette} , Title={Partial evaluation and non-interference for object calculi} ,Booktitle={Proceedings of FLOPS'99} , Year= 1999 , Publisher=springer , series= lncs , volume= {1722} , Editor= {A. Middeldorp and T. Sato} , pages={53--67}} @InProceedings{g99:fossacs , Author ={G. Barthe} , Title={Expanding the cube} ,Booktitle={Proceedings of {FOSSACS}'99} , Year= 1999 , Publisher=springer , series= lncs , volume= {1578} , Editor= {W. Thomas} , pages={90--103}} @InProceedings{gmj99:esop, author={G. Barthe and M.J. Frade}, title={{Constructor subtyping}}, year={1999}, Booktitle={Proceedings of {ESOP}'99} , Publisher=springer , series= lncs , volume= {1576} , Editor= {D. Swiestra} , pages={109--127}} @inproceedings{g98:csl, author={G. Barthe}, title={Existence and Uniqueness of Normal Forms in Pure Type Systems with $\beta\eta$-conversion}, year={1999}, Booktitle={Proceedings of CSL'98}, editor={G. Gottlob and E. Grandjean and K. Seyr}, pages={241--259}, Publisher=springer, series= lncs, volume= {1584}} @InProceedings{g98:icalp , Author ={G. Barthe} , Title={The relevance of proof-irrelevance} ,Booktitle={Proceedings of ICALP'98} , Year= 1998 , Publisher=springer , series= lncs , volume= {1443} , Editor= {K.G. Larsen and S. Skyum and G. Winskel} , pages={755--768}} @InProceedings{g98:mfcs , Author ={G. Barthe} , Title={{The semi-full closure of Pure Type Systems}} ,Booktitle={Proceedings of MFCS'98} , Year= 1998 , Publisher=springer , series= lncs , volume= {1450} , Editor= {L. Brim and J. Gruska and J. Zlatuska} , pages={316--325}} @inproceedings{gjp97:hoots, author={G. Barthe and J. Hatcliff and P. Thiemann}, title={Monadic type systems: Pure Type Systems for Impure Settings}, year={1998}, booktitle={Proceedings of HOOTS'97}, editor={A. Gordon and A. Pitts and C. Talcott}, series=entcs, volume=10, publisher=elsevier} @INPROCEEDINGS{gf97:hoa, AUTHOR = {Barthe, G. and Raamsdonk, F. van}, TITLE = {Termination of Algebraic Type Systems: the Syntactic Approach}, BOOKTITLE = {Proceedings of ALP '97 - HOA '97}, YEAR = 1997, EDITOR = {Hanus, M. and Heering, J.}, PAGES = {174--193}, VOLUME = 1298, SERIES = lncs, PUBLISHER = springer } @INPROCEEDINGS{gfa97:alp, AUTHOR = {Barthe, G. and Kamareddine, F. and R{\'\i}os, A.}, TITLE = {Explicit substitutions for the $\lambda\Delta$-calculus}, BOOKTITLE = {Proceedings of ALP '97 - HOA '97}, YEAR = 1997, EDITOR = {Hanus, M. and Heering, J.}, PAGES = {209--223}, VOLUME = 1298, SERIES = lncs, PUBLISHER = springer } @inproceedings{gjm97:mfps, author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen}, title={A notion of classical pure type system}, year={1997}, series=entcs, editor={S. Brookes and M. Mislove}, volume={6}, booktitle={Proceedings of MFPS'97}, publisher={Elsevier}} @inproceedings{gjm97:plilp, author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen}, title={Reflections on reflections}, booktitle={Proceedings of PLILP'97}, editor={H. Glaser and P. Hartel and H. Kuchen}, series=lncs, volume=1292, pages={241--258}, year={1997}} @inproceedings{gm97:lfcs, author={G. Barthe and M.H. S{\o}rensen}, title={Domain-free pure type systems}, year={1997}, booktitle={Proceedings of LFCS'97}, series=lncs, publisher=springer, editor={S. Adian and A. Nerode}, volume={1234}, pages={9--20}} @inproceedings{gjm97:wc, author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen}, title={{CPS}-translations and applications: the cube and beyond}, booktitle={Proceedings of the Second ACM SIGPLAN Workshop on Continuations}, series={BRICS Notes}, number={NS-96-13}, pages={4/1--4/31}, editor={O. Danvy}, year={1996}} @inproceedings{gpa96:csl, author={G. Barthe and P.-A. Melli{\`e}s}, title={On the subject reduction property for algebraic type systems}, booktitle={Proceedings of CSL'96}, series=lncs, editor={D. van Dalen and M. Bezem}, publisher=springer, year={1997}, volume={1258}, pages={34--57}} @inproceedings{gh96:disco, author={G. Barthe and H. Elbers}, title={Towards lean proof checking}, year={1996}, Publisher= {Springer-Verlag}, series= lncs, booktitle={Proceedings of DISCO'96}, editor={J. Calmet and C. Limongelli}, volume={1128}, pages={61-62}} @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:types, 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, editor={S. Berardi and M. Coppo}, volume={1158}, pages={16--35}} @inproceedings{g95:types, author={G. Barthe}, title={Implicit coercions in type systems}, year={1996}, Booktitle={Proceedings of {TYPES}'95}, Publisher= {Springer-Verlag}, series= lncs, editor={S. Berardi and M. Coppo}, volume={1158}, pages={16--35}} @inproceedings{g95:fct, author={G. Barthe}, title={A simple abstract semantics for equational theories}, year={1995}, Publisher= {Springer-Verlag}, series= lncs, volume= {965}, editor={H. Reichel}, booktitle={Proceedings of FCT'95}, pages={126--135}} @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} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % JOURNALS % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @article{gl06:jcs, author={G. Barthe and L. Prensa-Nieto}, title={Secure Information Flow for a Concurrent Language with Scheduling}, journal=jcs, year={200x}, note={To appear}} @article{g+06:jar, author = {G. Barthe and P. Courtieu and G. Dufay and S. Melo de Sousa}, title = {{Jakarta: tool-assisted specification and verification of the JavaCard Platform}}, year = {2006}, journal=jar, note={To appear}} @article{BRB07:cl, author={G. Barthe and A. Basu and T. Rezk}, title={Security Types Preserving Compilation}, year={2007}, journal={Journal of Computer Languages, Systems and Structures}, note={To appear}} @article{gt04:jfp, author ={G. Barthe and T. Coquand}, title = {On the equational theory of non-normalizing Pure Type Systems}, journal= jfp, year = {2004}, volume=14, number=2, pages={191--209}, month=mar } @article{gvo03:jfp, author = {G. Barthe and V. Capretta and O. Pons}, title = {Setoids in Type Theory}, journal= jfp, year = {2003}, pages={261--293}, volume=13, issue=2, month=mar} @article{g+04:mscs, author = {G. Barthe and M. J. Frade and E. Gim{\'e}nez and L. Pinto and T. Uustalu}, title = {Type-Based Termination of Recursive Definitions}, year = {2004}, journal=mscs, month=feb, volume=14, issue=1, pages={97--141}} @article{g04:mscs, author = {G. Barthe}, title = {Type Isomorphisms and Back-and-Forth Coercions in Type Theory}, year = {2005}, journal=mscs, note={To appear}} @article{gjm01: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={2001}, month=oct, journal=tcs, pages={317--361}, volume={269}, number={1-2}} @article{gjm01:ip, author={G. Barthe and J. Hatcliff and M.H.B. S{\o}rensen}, title={{An induction principle for Pure Type Systems}}, year={2001}, month=sep, journal=tcs, volume={266}, number={1-2}, pages={773-818}} @article{gm00:jfp, author={G. Barthe and M.H. S{\o}rensen}, title={{Domain-free pure type systems}}, year={2000}, journal=jfp, month=sep, pages={417--452}, volume={10}, number={5}} @Comment note={Preliminary version in S. Adian and A. Nerode, @Comment editors, Proceedings of LFCS'97, LNCS 1234, pp @Comment 9-20}} @article{g99:jfp, author={G. Barthe}, title={{Type-Checking Injective Pure Type Systems}}, year={1999}, journal=jfp, volume=9, number=6, pages={675--698}} @article{gjm99:hosc, author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen}, title={{CPS}-translations and applications: the cube and beyond}, journal=hosc, volume=12, number=2, year=1999, month=sep, pages={125--170}} @article{g99:ic, author={G. Barthe}, title={Order-sorted inductive types}, journal=ic, pages={42--76}, month=feb, year=1999, volume=149, number=1} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % HDR % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @PHDTHESIS{Bar:hdr, TITLE = {De la th\'eorie des types \`a la v\'erification formelles des petits objets portables de s\'ecurit\'e}, AUTHOR = {G. Barthe}, YEAR = {2004}, SCHOOL = {Universit\'e de Nice Sophia-Antipolis}, TYPE = {Habilitation {\`a} Diriger des Recherches} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % MISC % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @unpublished{g+:certicartes, author = {G. Barthe and G. Dufay and S. Melo de Sousa}, title = {{A Formal Executable Semantics of the JavaCard Platform}}, year = {2003}, note={Manuscript}} @Unpublished{g+:ext, author = {G. Barthe and G. Betarte and M. J. Frade and L. Pinto and J. Zwanenburg}, title = {Extensible Overloaded Functions}, note = {Manuscript}, year = {2000} } @techreport{g98:peoc, author={G. Barthe}, number={UMDITR9806}, title={Partial evaluation of object calculi}, institution={Department of Computer Science, University of Minho}, year={1998},} @techreport{gmj:cs, author={G. Barthe and M.J. Frade}, number={UMDITR9807}, title={Constructor subtyping}, institution={Department of Computer Science, University of Minho}, year={1998}} @techreport{gfa96:es, author={G. Barthe and F. Kamareddine and A. R{\'\i}os}, title={Explicit substitutions for control operators}, institution={Department of Computer Science, University of Glasgow}, year={1996}} @techreport{g95:form, author={G. Barthe}, title={Formalising mathematics in type theory: fundamentals and case studies}, year={1995}, number={CSI-R9508}, institution={University of Nijmegen}} @techreport{g95:ver, author={G. Barthe}, title={Towards a mathematical vernacular}, year={1995}, number={CSI-N9502}, institution=kun} @techreport{g95:hol, author={G. Barthe}, title={Strong normalisation of quotient and subset types in higher order logic}, year={1995}, institution=kun, number={CSI-R9509}} @phdthesis{g:thesis, author={G. Barthe}, title={Term Declaration Logic and Generalised Composita}, school={University of Manchester}, year={1993}} @Unpublished{g:str, author = {G. Barthe}, title = {On the failure of strengthening in Domain-Free Pure Type Systems}, note = {Manuscript}, year = {2001} } @unpublished{gjp98:pe, author={G. Barthe and J. Hatcliff and P. Thiemann}, title={Partial evaluation of monadic type systems}, year={1998}, note={Unpublished notes}} @unpublished{gm:classif, author={G. Barthe and M.H. S{\o}rensen}, title={The virtues of Classification}, year={1998}} @unpublished{gh97:cwi, author={G. Barthe and H. Elbers}, title={Implementing efficient procedures for equation reasoning}, note={Manuscript}, year={1997}} @unpublished{companion, author={G. Barthe}, title={On strong normalisation of algebraic type systems}, year={1997}} @unpublished{g96:equa, author={G. Barthe}, title={Combining dependent type theories with equational term-rewriting}, year={1995}, note={Manuscript}} @unpublished{g95:eta, author={G. Barthe}, title={$\eta$-reduction and algebraic rewriting in $\lambda$-calculus}, year={1995}, note={Manuscript}} @unpublished{AB93, author={P. Aczel and G. Barthe}, title={Classes in type theory}, year={1993}, note={Note}}