Gilles Barthe
AuthID: R-00H-7MM
141
TITLE: Validation of the JavaCard Platform with Implicit Induction Techniques
AUTHORS: Gilles Barthe; Sorin Stratulat;
PUBLISHED: 2003, SOURCE: RTA
AUTHORS: Gilles Barthe; Sorin Stratulat;
PUBLISHED: 2003, SOURCE: RTA
INDEXED IN:
DBLP
IN MY:
DBLP
142
TITLE: Setoids in type theory
AUTHORS: Gilles Barthe; Venanzio Capretta; Olivier Pons;
PUBLISHED: 2003, SOURCE: J. Funct. Program., VOLUME: 13, ISSUE: 2
AUTHORS: Gilles Barthe; Venanzio Capretta; Olivier Pons;
PUBLISHED: 2003, SOURCE: J. Funct. Program., VOLUME: 13, ISSUE: 2
INDEXED IN:
DBLP
IN MY:
DBLP
143
TITLE: CPS translating inductive and coinductive types
AUTHORS: Barthe, G; Uustalu, T;
PUBLISHED: 2002, SOURCE: ACM/SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 02) in ACM SIGPLAN NOTICES, VOLUME: 37, ISSUE: 3
AUTHORS: Barthe, G; Uustalu, T;
PUBLISHED: 2002, SOURCE: ACM/SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 02) in ACM SIGPLAN NOTICES, VOLUME: 37, ISSUE: 3
144
TITLE: Compositional Verification of Secure Applet Interactions
AUTHORS: Gilles Barthe; Dilian Gurov; Marieke Huisman;
PUBLISHED: 2002, SOURCE: FASE
AUTHORS: Gilles Barthe; Dilian Gurov; Marieke Huisman;
PUBLISHED: 2002, SOURCE: FASE
INDEXED IN:
DBLP
IN MY:
DBLP
145
TITLE: Efficient Reasoning about Executable Specifications in Coq
AUTHORS: Gilles Barthe; Pierre Courtieu;
PUBLISHED: 2002, SOURCE: TPHOLs
AUTHORS: Gilles Barthe; Pierre Courtieu;
PUBLISHED: 2002, SOURCE: TPHOLs
INDEXED IN:
DBLP
IN MY:
DBLP
146
TITLE: Preface
AUTHORS: Gilles Barthe; Peter Thiemann;
PUBLISHED: 2002, SOURCE: TIP@MPC
AUTHORS: Gilles Barthe; Peter Thiemann;
PUBLISHED: 2002, SOURCE: TIP@MPC
INDEXED IN:
DBLP
IN MY:
DBLP
147
TITLE: Type Isomorphisms and Proof Reuse in Dependent Type Theory
AUTHORS: Gilles Barthe; Olivier Pons;
PUBLISHED: 2001, SOURCE: 4th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 in FoSSaCS, VOLUME: 2030
AUTHORS: Gilles Barthe; Olivier Pons;
PUBLISHED: 2001, SOURCE: 4th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 in FoSSaCS, VOLUME: 2030
INDEXED IN:
Scopus
DBLP
IN MY:
DBLP
148
TITLE: Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo)
AUTHORS: Gilles Barthe; Blas C Ruiz Jiménez;
PUBLISHED: 2001, SOURCE: APPIA-GULP-PRODE
AUTHORS: Gilles Barthe; Blas C Ruiz Jiménez;
PUBLISHED: 2001, SOURCE: APPIA-GULP-PRODE
INDEXED IN:
DBLP
IN MY:
DBLP
149
TITLE: An induction principle for pure type systems
AUTHORS: Gilles Barthe; John Hatcliff; Morten Heine Sørensen;
PUBLISHED: 2001, SOURCE: Theor. Comput. Sci., VOLUME: 266, ISSUE: 1-2
AUTHORS: Gilles Barthe; John Hatcliff; Morten Heine Sørensen;
PUBLISHED: 2001, SOURCE: Theor. Comput. Sci., VOLUME: 266, ISSUE: 1-2
INDEXED IN:
DBLP
IN MY:
DBLP
150
TITLE: Weak normalization implies strong normalization in a class of non-dependent pure type systems
AUTHORS: Gilles Barthe; John Hatcliff; Morten Heine Sørensen;
PUBLISHED: 2001, SOURCE: Theor. Comput. Sci., VOLUME: 269, ISSUE: 1-2
AUTHORS: Gilles Barthe; John Hatcliff; Morten Heine Sørensen;
PUBLISHED: 2001, SOURCE: Theor. Comput. Sci., VOLUME: 269, ISSUE: 1-2
INDEXED IN:
DBLP
IN MY:
DBLP