Gilles Barthe
AuthID: R-00H-7MM
141
TITLE: A Machine-Checked Formalization of the Random Oracle Model
AUTHORS: Gilles Barthe; Sabrina Tarento;
PUBLISHED: 2004, SOURCE: TYPES
AUTHORS: Gilles Barthe; Sabrina Tarento;
PUBLISHED: 2004, SOURCE: TYPES
INDEXED IN: 
DBLP
DBLP IN MY: DBLP
DBLP142
TITLE: Security Types Preserving Compilation: (Extended Abstract)
AUTHORS: Gilles Barthe; Amitabh Basu; Tamara Rezk;
PUBLISHED: 2004, SOURCE: VMCAI
AUTHORS: Gilles Barthe; Amitabh Basu; Tamara Rezk;
PUBLISHED: 2004, SOURCE: VMCAI
INDEXED IN: DBLP
DBLP IN MY: DBLP
DBLP143
TITLE: Pure patterns type systems
AUTHORS: Gilles Barthe; Horatiu Cirstea; Claude Kirchner; Luigi Liquori;
PUBLISHED: 2003, SOURCE: POPL
AUTHORS: Gilles Barthe; Horatiu Cirstea; Claude Kirchner; Luigi Liquori;
PUBLISHED: 2003, SOURCE: POPL
INDEXED IN: DBLP
DBLP IN MY: DBLP
DBLP144
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
DBLP IN MY: DBLP
DBLP145
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
DBLP IN MY: DBLP
DBLP146
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
147
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
DBLP IN MY: DBLP
DBLP148
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
DBLP IN MY: DBLP
DBLP149
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
DBLP IN MY: DBLP
DBLP150
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
Scopus DBLP IN MY: DBLP
DBLP