Gilles Barthe

Gilles Barthe, Juan Manuel Crespo, César Kunz: Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. LFCS 2013: 29-43

Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron: From relational verification to SIMD loop synthesis. PPOPP 2013: 123-134

Gilles Barthe, Jorge Cuéllar, Javier Lopez, Alexander Pretschner: Preface. Journal of Computer Security 20(4): 307-308 (2012)

José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin: Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. ACM Conference on Computer and Communications Security 2012: 488-500

Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin: Verified security of redundancy-free encryption from Rabin and RSA. ACM Conference on Computer and Communications Security 2012: 724-735

Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin: Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP 2012: 7-8

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna: Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. CSF 2012: 186-197

Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin: Verified Security of Merkle-Damgård. CSF 2012: 354-368

Gilles Barthe, Delphine Demange, David Pichardie: A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. ESOP 2012: 47-66

Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas: Secure Multi-Execution through Static Program Transformation. FMOODS/FORTE 2012: 186-202

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin: Computer-Aided Cryptographic Proofs. ITP 2012: 11-27

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC 2012: 1-6

Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin: Probabilistic relational reasoning for differential privacy. POPL 2012: 97-110

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin: Verified Indifferentiable Hashing into Elliptic Curves. POST 2012: 209-228

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Computer-Aided Cryptographic Proofs. SAS 2012: 1-2

Gilles Barthe, Benjamin Livshits, Riccardo Scandariato (Eds.): Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings. Lecture Notes in Computer Science 7159, Springer 2012, isbn 978-3-642-28165-5

Gilles Barthe, Anupam Datta, Sandro Etalle (Eds.): Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers. Lecture Notes in Computer Science 7140, Springer 2012, isbn 978-3-642-29419-8

José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin: Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. IACR Cryptology ePrint Archive 2012: 258 (2012)

Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin: Verified Security of Redundancy-Free Encryption from Rabin and RSA. IACR Cryptology ePrint Archive 2012: 308 (2012)

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin: Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptology ePrint Archive 2012: 695 (2012)

Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure information flow by self-composition. Mathematical Structures in Computer Science 21(6): 1207-1252 (2011)

Gilles Barthe, César Kunz: An Abstract Model of Certificate Translation. ACM Trans. Program. Lang. Syst. 33(4): 13 (2011)

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin: Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO 2011: 71-90

Gilles Barthe, Boris Köpf: Information-Theoretic Bounds for Differentially Private Mechanisms. CSF 2011: 191-204

Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin: Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA 2011: 180-196

Gilles Barthe, Juan Manuel Crespo, César Kunz: Relational Verification Using Product Programs. FM 2011: 200-214

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna: Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. FM 2011: 231-245

Gilles Barthe, Mathilde Duclos, Yassine Lakhnech: A Computational Indistinguishability Logic for the Bounded Storage Model. FPS 2011: 102-117

Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin: Verifiable Security of Boneh-Franklin Identity-Based Encryption. ProvSec 2011: 68-83

Gilles Barthe, Exequiel Rivas: Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language. TGC 2011: 73-88

Gilles Barthe (Ed.): Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science 6602, Springer 2011, isbn 978-3-642-19717-8

Gilles Barthe, Alberto Pardo, Gerardo Schneider (Eds.): Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings. Lecture Notes in Computer Science 7041, Springer 2011, isbn 978-3-642-24689-0

Jorge Cuéllar, Javier Lopez, Gilles Barthe, Alexander Pretschner (Eds.): Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers. Lecture Notes in Computer Science 6710, Springer 2011, isbn 978-3-642-22443-0

Gilles Barthe, Boris Köpf: Information-theoretic Bounds for Differentially Private Mechanisms. IACR Cryptology ePrint Archive 2011: 71 (2011)

Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld: Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. 13(3) (2010)

Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech: Computational indistinguishability logic. ACM Conference on Computer and Communications Security 2010: 375-386

Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi: Robustness Guarantees for Anonymity. CSF 2010: 91-106

Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud: A Machine-Checked Formalization of Sigma-Protocols. CSF 2010: 246-260

Gilles Barthe, Pablo Buiras, César Kunz: A Functional Framework for Result Checking. FLOPS 2010: 72-86

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130

Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte: On the Equality of Probabilistic Terms. LPAR (Dakar) 2010: 46-63

Gilles Barthe, César Kunz: Perspectives in Certificate Translation. TGC 2010: 23-34

Gilles Barthe, Manuel V. Hermenegildo (Eds.): Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings. Lecture Notes in Computer Science 5944, Springer 2010, isbn 978-3-642-11318-5

Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk: Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. 31(5) (2009)

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet: Implementing a Direct Method for Certificate Translation. ICFEM 2009: 541-560

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Formal certification of code-based cryptographic proofs. POPL 2009: 90-101

Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo: Formally Certifying the Security of Digital Signature Schemes. IEEE Symposium on Security and Privacy 2009: 237-250

Alessandro Aldini, Gilles Barthe, Roberto Gorrieri (Eds.): Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Lecture Notes in Computer Science 5705, Springer 2009, isbn 978-3-642-03828-0

Gilles Barthe, César Kunz, Jorge Luis Sacchini: Certified Reasoning in Memory Hierarchies. APLAS 2008: 75-90

Gilles Barthe: Certificate Translation. VERIFY 2008

Gilles Barthe, Benjamin Grégoire, Mariela Pavlova: Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99

Gilles Barthe, Salvador Cavadini, Tamara Rezk: Tractable Enforcement of Declassification Policies. CSF 2008: 83-97

Gilles Barthe, Benjamin Grégoire, Colin Riba: Type-Based Termination with Sized Products. CSL 2008: 493-507

Gilles Barthe, César Kunz: Certificate Translation in Abstract Interpretation. ESOP 2008: 368-382

Gilles Barthe, César Kunz: Certificate translation for specification-preserving advices. FOAL 2008: 9-18

Gilles Barthe, César Kunz: An Introduction to Certificate Translation. FOSAD 2008: 51-95

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin: Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust 2008: 1-19

Gilles Barthe, Benjamin Grégoire, Colin Riba: A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152

Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese: Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM 2008: 127-136

Gilles Barthe, Frank S. de Boer (Eds.): Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings. Lecture Notes in Computer Science 5051, Springer 2008, isbn 978-3-540-68862-4

Gilles Barthe, Cédric Fournet (Eds.): Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers. Lecture Notes in Computer Science 4912, Springer 2008, isbn 978-3-540-78662-7

Gilles Barthe, Tamara Rezk, Amitabh Basu: Security types preserving compilation. Computer Languages, Systems & Structures 33(2): 35-59 (2007)

Gilles Barthe, Leonor Prensa Nieto: Secure information flow for a concurrent language with scheduling. Journal of Computer Security 15(6): 647-689 (2007)

Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld: 07091 Executive Summary - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007

Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld: 07091 Abstracts Collection - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007

Gilles Barthe, David Pichardie, Tamara Rezk: A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP 2007: 125-140

Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld: Security of Multithreaded Programs by Compilation. ESORICS 2007: 2-18

Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie: The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24

Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld (Eds.): Mobility, Ubiquity and Security, 25.02. - 02.03.2007. Dagstuhl Seminar Proceedings 07091, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007

Gilles Barthe, Benjamin Grégoire, Romain Janvier, Santiago Zanella Béguelin: Formal Certification of Code-Based Cryptographic Proofs. IACR Cryptology ePrint Archive 2007: 314 (2007)

Gilles Barthe, Tamara Rezk, Martijn Warnier: Preventing Timing Leaks Through Transactional Branching Instructions. Electr. Notes Theor. Comput. Sci. 153(2): 33-55 (2006)

Gilles Barthe, Thierry Coquand: Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16(2): 137-155 (2006)

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS 2006: 114-129

Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet: JACK - A Tool for Validation of Security and Behaviour of Java Applications. FMCO 2006: 152-174

Gilles Barthe, Benjamin Grégoire, Fernando Pastawski: CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271

Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk: Certificate Translation for Optimizing Compilers. SAS 2006: 301-317

Gilles Barthe, Tamara Rezk, David A. Naumann: Deriving an Information Flow Checker and Certifying Compiler for Java. IEEE Symposium on Security and Privacy 2006: 230-242

Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard: MOBIUS: Mobility, Ubiquity, Security. TGC 2006: 10-29

Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet (Eds.): Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3956, Springer 2006, isbn 3-540-33689-3

Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa: Tool-Assisted Specification and Verification of Typed Low-Level Languages. J. Autom. Reasoning 35(4): 295-354 (2005)

Gilles Barthe: A computational view of implicit coercions in type theory. Mathematical Structures in Computer Science 15(5): 839-874 (2005)

Gilles Barthe, Guillaume Dufay: Formal Methods for Smartcard Security. FOSAD 2005: 133-177

Gilles Barthe, Tamara Rezk, Ando Saabas: Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust 2005: 112-126

Gilles Barthe, Mariela Pavlova, Gerardo Schneider: Precise Analysis of Memory Consumption using Program Logics. SEFM 2005: 86-95

Gilles Barthe, Benjamin Grégoire, Fernando Pastawski: Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85

Gilles Barthe, Tamara Rezk: Non-interference for a JVM-like language. TLDI 2005: 103-112

Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean (Eds.): Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3362, Springer 2005, isbn 3-540-24287-2

Gilles Barthe, Peter Dybjer, Peter Thiemann: Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. J. Funct. Program. 14(1): 1-2 (2004)

Gilles Barthe, Maria João Frade, E. Giménez, Luis Pinto, Tarmo Uustalu: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14(1): 97-141 (2004)

Gilles Barthe, Jan Cederquist, Sabrina Tarento: A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. IJCAR 2004: 385-399

Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet: Enforcing High-Level Security Properties for Applets. CARDIS 2004: 1-16

Gilles Barthe, Leonor Prensa Nieto: Formally verifying information flow type systems for concurrent and thread systems. FMSE 2004: 13-22

Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. CSFW 2004: 100-114

Gilles Barthe, Guillaume Dufay: A Tool-Assisted Framework for Certified Bytecode Verification. FASE 2004: 99-113

Gilles Barthe, Sabrina Tarento: A Machine-Checked Formalization of the Random Oracle Model. TYPES 2004: 33-49

Gilles Barthe, Amitabh Basu, Tamara Rezk: Security Types Preserving Compilation: (Extended Abstract). VMCAI 2004: 2-15

Gilles Barthe, Venanzio Capretta, Olivier Pons: Setoids in type theory. J. Funct. Program. 13(2): 261-293 (2003)

Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: Pure patterns type systems. POPL 2003: 250-261

Gilles Barthe, Sorin Stratulat: Validation of the JavaCard Platform with Implicit Induction Techniques. RTA 2003: 337-351

Gilles Barthe, Peter Thiemann: Preface. Electr. Notes Theor. Comput. Sci. 75: 114-115 (2002)

Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa: Tool-Assisted Specification and Verification of the JavaCard Platform. AMAST 2002: 41-59

Gilles Barthe, Dilian Gurov, Marieke Huisman: Compositional Verification of Secure Applet Interactions. FASE 2002: 15-32

Gilles Barthe, Tarmo Uustalu: CPS translating inductive and coinductive types. PEPM 2002: 131-142

Gilles Barthe, Pierre Courtieu: Efficient Reasoning about Executable Specifications in Coq. TPHOLs 2002: 31-46

Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa: A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. VMCAI 2002: 32-45

Gilles Barthe, Peter Dybjer, Luis Pinto, João Saraiva (Eds.): Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures. Lecture Notes in Computer Science 2395, Springer 2002, isbn 3-540-44044-5

Gilles Barthe, John Hatcliff, Morten Heine Sørensen: An induction principle for pure type systems. Theor. Comput. Sci. 266(1-2): 773-818 (2001)

Gilles Barthe, John Hatcliff, Morten Heine Sørensen: Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theor. Comput. Sci. 269(1-2): 317-361 (2001)

Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa: Jakarta: A Toolset for Reasoning about JavaCard. E-smart 2001: 2-18

Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa: A Formal Executable Semantics of the JavaCard Platform. ESOP 2001: 302-319

Gilles Barthe, Olivier Pons: Type Isomorphisms and Proof Reuse in Dependent Type Theory. FoSSaCS 2001: 57-71

Gilles Barthe, Morten Heine Sørensen: Domain-free pure type systems. J. Funct. Program. 10(5): 417-452 (2000)

Gilles Barthe, Thierry Coquand: An Introduction to Dependent Type Theory. APPSEM 2000: 1-41

Gilles Barthe, Femke van Raamsdonk: Constructor Subtyping in the Calculus of Inductive Constructions. FoSSaCS 2000: 17-34

Gilles Barthe, Bernard P. Serpette: Static Reduction Analysis for Imperative Object Oriented Languages. LPAR 2000: 344-361

Gilles Barthe: Order-Sorted Inductive Types. Inf. Comput. 149(1): 42-76 (1999)

Gilles Barthe: Type-checking injective pure type systems. J. Funct. Program. 9(6): 685-698 (1999)

Gilles Barthe, John Hatcliff, Morten Heine Sørensen: CPS Translations and Applications: The Cube and Beyond. Higher-Order and Symbolic Computation 12(2): 125-170 (1999)

Gilles Barthe, Maria João Frade: Constructor Subtyping. ESOP 1999: 109-127

Gilles Barthe, Bernard P. Serpette: Partial Evaluation and Non-inference for Object Calculi. Fuji International Symposium on Functional and Logic Programming 1999: 53-67

Gilles Barthe: Expanding the Cube. FoSSaCS 1999: 90-103

Gilles Barthe: Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. CSL 1998: 241-259

Gilles Barthe: The Relevance of Proof-Irrelevance. ICALP 1998: 755-768

Gilles Barthe: The Semi-Full Closure of Pure Type Systems. MFCS 1998: 316-325

Gilles Barthe, John Hatcliff, Morten Heine Sørensen: A notion of classical pure type system. Electr. Notes Theor. Comput. Sci. 6: 4-59 (1997)

Gilles Barthe, John Hatcliff, Peter Thiemann: Monadic Type Systems: Pure Type Systems for Impure Settings. Electr. Notes Theor. Comput. Sci. 10: 54-120 (1997)

Gilles Barthe, Femke van Raamsdonk: Termination of Algebraic Type Systems: The Syntactic Approach. ALP/HOA 1997: 174-193

Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos: Explicit Substitutions for the Lambda-Calculus. ALP/HOA 1997: 209-223

Gilles Barthe, Morten Heine Sørensen: Domain-Free Pure Type Systems. LFCS 1997: 9-20

Gilles Barthe, John Hatcliff, Morten Heine Sørensen: Reflections on Reflections. PLILP 1997: 241-258

Gilles Barthe, Paul-André Melliès: On the Subject Reduction Property for Algebraic Type Systems. CSL 1996: 34-57

Gilles Barthe, Hugo Elbers: Towards Lean Proof Checking. DISCO 1996: 61-62

Gilles Barthe, Herman Geuvers: Congruence Types. CSL 1995: 36-51

Gilles Barthe: A Simple Abstract Semantics for Equational Theories. FCT 1995: 126-135

Gilles Barthe, Herman Geuvers: Modular Properties of Algebraic Type Systems. HOA 1995: 37-56

Gilles Barthe: Extensions of Pure Type Systems. TLCA 1995: 16-31

Gilles Barthe: Implicit Coercions in Type Systems. TYPES 1995: 1-15

Gilles Barthe, Mark Ruys, Henk Barendregt: A Two-Level Approach Towards Lean Proof-Checking. TYPES 1995: 16-35