Non-Interference for a JVM-like Language ∗ (Extended Abstract) (2009)
Gilles Barthe, Inria Sophia Antipolis, Tamara Rezk
We define an information flow type system for a sequential JVM-like language that includes classes, objects, and exceptions. Furthermore, we show that it enforces noninterference. Our work provides,...
Precise Analysis of Memory Consumption using Program Logics ∗ (2009)
Gilles Barthe, Mariela Pavlova, Gerardo Schneider
Memory consumption policies provide ameans tocontrol resource usage on constrained devices, and play an important role in ensuring the overall quality of software systems, and in particular...
A Framework for Language-Based Cryptographic Proofs (2008)
Gilles Barthe, Benjamin Grégoire, Romain Janvier, Santiago Zanella Béguelin
Motivation In cryptography, provable security advocates a mathematical approach where the goals and requirements of cryptographic systems are specified precisely, and where the security proof is...
Proof Obligations Preserving Compilation Extended abstract (2008)
Gilles Barthe, Tamara Rezk, Ando Saabas
Abstract. The objective of this work is to study the interaction between program verification and program compilation, and to show that the proof that a source program meets its specification can be...
Formal Methods for Smartcard Security (2008)
Gilles Barthe, Guillaume Dufay
Abstract. Smartcards are trusted personal devices designed to store and process confidential data, and to act as secure tokens for providing access to applications and services. Smartcards are widely...
Virtual machines, such as the Java Virtual Machine, Java Card Virtual (2008)
Gilles Barthe, Inria Sophia Antipolis, Guillaume Dufay
Abstract. Bytecode verification is one of the key security functions of several architectures for mobile and embedded code, including Java, Java Card, and.NET. Over the last few years, its formal...
ABSTRACT Pure Patterns Type Systems (2008)
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
We introduce a new framework of algebraic pure type systems in which we consider rewrite rules as lambda terms with patterns and rewrite rule application as abstraction application with built-in...
Certificate Translation for Optimizing Compilers ⋆ (extended abstract) (2008)
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
Abstract. Certifying compilation provides a means to ensure that untrusted mobile code satisfies its functional specification. A certifying compiler generates code as well as a machine-checkable...
Static Reduction Analysis for Imperative Object Oriented Languages (2008)
Gilles Barthe, Bernard Paul Serpette
Abstract. We de ne a novel static analysis, Static Reduction Analysis (SRA), for an untyped objectoriented language featuring side-e ects and exceptions. While its aims and range of applications...
DOI: 10.1017/S0956796802004501 Printed in the United Kingdom Setoids in type theory (2008)
Gilles Barthe, Venanzio Capretta
Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids...
Practical Inference for Typed-Based Termination in a Polymorphic Setting (2008)
Gilles Barthe, Benjamin Gregoire, Fernando Pastawski
We introduce a polymorphic #-calculus that features inductive types and that enforces termination of recursive definitions through typing. Then, we define a sound and complete type inference...
Preservation of proof obligations for hybrid verification methods (2008)
Barthe, Gilles, Kunz, César, Pichardie, David, Samborski-Forlese, Julian
Program verification environments increasingly rely on hybrid methods that combine static analyses and verification condition generation. While such verification environments operate on source...
Preservation of proof obligations for hybrid verification methods (2008)
Barthe, Gilles, Kunz, César, Pichardie, David, Samborski-Forlese, Julian
Program verification environments increasingly rely on hybrid methods that combine static analyses and verification condition generation. While such verification environments operate on source...
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. Formalising mathematics in dependent type theory often requires to use setoids, i.e. types with an explicit equality relation, as a representation of sets. This paper surveys some possible...
Abstract. We propose a theoretical foundation for proof reuse, based on the novel idea of a computational interpretation of type isomorphisms. 1
A Two-Level Approach towards (2007)
Lean Proof-checking, Gilles Barthe, Mark Ruys, Henk Barendregt
We present a simple and effective methodology for equational reasoning in proof checkers. The method is based on a two-level approach distinguishing between syntax and semantics of mathematical...
Static Reduction Analysis for Imperative Object Oriented Languages (2007)
Gilles Barthe, Bernard Paul Serpette
Abstract. We dene a novel static analysis, Static Reduction Analysis (SRA), for an untyped objectoriented language featuring side-eoeects and exceptions. While its aims and range of applications...
Gilles Barthe, Chalmers Tekniska Hogskola
Abstract. We propose a general technique, inspired from proof-irrelevance, to prove strong normalisation and consistency for extensions of the Calculus of Constructions. 1
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. We show that two approaches commonly used to formalise sets in type theory, partial setoids and total setoids, are in fact not equivalent. More precisely, we show that total setoids form a
with subtyping and bounded quantification. Order-sorted algebra is an extension of many-sorted algebra with overloading and subtyping. We combine both formalisms to obtain
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. Formalising mathematics in dependent type theory often requires to use setoids, i.e. types with an explicit equality relation, as a representation of sets. This paper surveys some possible...
Abstract. We propose a theoretical foundation for proof reuse, based on the novel idea of a computational interpretation of type isomorphisms.
Departamento de Inform#tica (2007)
In memory of Yossi Shamir Injective Pure Type Systems form a large class of Pure Type Systems for which one can compute by purely syntactic means two sorts elmt(\GammajM) and sort(\GammajM), where...
On the Equational Theory of Non-Normalising Pure Type Systems (2007)
Pure Type Systems [1, 8] provide a generic framework for the description of
Gilles Barthe, Dilian Gurov, Marieke Huisman
Compositional specication and verication of control AEow based security properties of multi-application programs
Explicit substitutions for the \Delta-calculus (2007)
Gilles Barthe, Fairouz Kamareddine
Abstract. The \Delta-calculus is a-calculus with a control-like operator whose reduction rules are closely related to normalisation procedures in classical logic. We introduce \Deltaexp, an explicit...
Gilles Barthe, Fairouz Kamareddine
. The \Delta-calculus is a -calculus with a control-like operator whose reduction rules are closely related to normalisation procedures in classical logic. We introduce \Deltaexp, an explicit...
Secure Information Flow for a Concurrent Language with Scheduling (2007)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have specified an information flow type system for a...
Secure Information Flow for a Concurrent Language with Scheduling (2007)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have specified an information flow type system for a...
A Certified Lightweight Non-Interference Java Bytecode Verifier (2007)
Barthe, Gilles, Pichardie, David, Rezk, Tamara
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow...
A Certified Lightweight Non-Interference Java Bytecode Verifier (2007)
Barthe, Gilles, Pichardie, David, Rezk, Tamara
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow...
Mobius: Mobility, ubiquity, security: Objectives and progress report (2007)
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, ...
Abstract. Through their global, uniform provision of services and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize...
A certified lightweight non-interference java bytecode verifier (2007)
Abstract. Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate...
Mobius: Mobility, ubiquity, security: Objectives and progress report (2007)
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, ...
Abstract. Through their global, uniform provision of services and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize...
Security of multithreaded programs by compilation (2007)
Gilles Barthe, Tamara Rezk, Ro Russo, Andrei Sabelfeld
Abstract. Information security is a pressing challenge for mobile code technologies. In order to claim end-to-end security of mobile code, it is necessary to establish that the code neither...
07091 Executive Summary -- Mobility, Ubiquity and Security (2007)
Barthe, Gilles, Mantel, Heiko, Müller, Peter, Myers, Andrew C., Sabelfeld, Andrei
Increasing code mobility and ubiquity raises serious concerns about the security of modern computing infrastructures. The focus of this seminar was on securing computing systems by design and by...
07091 Abstracts Collection -- Mobility, Ubiquity and Security (2007)
Barthe, Gilles, Mantel, Heiko, Müller, Peter, Myers, Andrew C., Sabelfeld, Andrei
From 25.02.2007 to 02.03.2007, the Dagstuhl Seminar 07091 ``Mobility, Ubiquity and Security'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the...
A Certified Lightweight Non-Interference Java Bytecode Verifier (2006)
Barthe, Gilles, Pichardie, David, Rezk, Tamara
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow...
A Certified Lightweight Non-Interference Java Bytecode Verifier (2006)
Barthe, Gilles, Pichardie, David, Rezk, Tamara
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow...
A Certified Lightweight Non-Interference Java Bytecode Verifier (2006)
Barthe, Gilles, Pichardie, David, Rezk, Tamara
Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow...
Secure Information Flow for a Concurrent Language with Scheduling (2006)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have specified an information flow type system for a...
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
practical tool for the Coq proof assistant
Deriving an information flow checker and certifying compiler for java (2006)
Gilles Barthe, David Naumann, Tamara Rezk
Language-based security provides a means to enforce endto-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smartcard and mobile phone...
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
Abstract. We present a practical tool for defining and proving properties of recursive functions in the Coq proof assistant. The tool generates from pseudo-code the graph of the intended function as...
Libraries Virtual Machine (2005)
Gilles Barthe, Martin Abadi, Amy Felty, Rustan Leino, Inria Lmu Münich, Ru Nijmegen, ...
16 members
A Machine-Checked Formalization of the Random Oracle Model (2005)
Gilles Barthe, Sabrina Tarento
Abstract. Most approaches to the formal analysis of cryptography protocols make the perfect cryptographic assumption, which entails for example that there is no way to obtain knowledge about the...
Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems (2004)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have machine-checked a recent work of Boudol and...
Type-based termination of recursive definitions (2004)
Barthe, Gilles, Frade, M. J., Giménez, E., Pinto, Luís F., Uustalu, T.
This paper introduces "lambda-hat", a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy...
Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems (2004)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have machine-checked a recent work of Boudol and...
Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems (2004)
Barthe, Gilles, Prensa Nieto, Leonor
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant Isabelle/HOL, we have machine-checked a recent work of Boudol and...
Enforcing high-level security properties for applets (2004)
Mariela Pavlova, Mariela Pavlova, Gilles Barthe, Gilles Barthe, Lilian Burdy, Lilian Burdy, ...
apport de recherche
Enforcing High-Level Security Properties for Applets (2004)
Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-louis Lanet
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties,...
Enforcing High-Level Security Properties for Applets (2004)
Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-louis Lanet
Smart card applications often handle privacy-sensitive information, and therefore must obey certain security policies. Typically, such policies are described as high-level security properties,...
A machine-checked formalization of the generic model and the random oracle model (2004)
Gilles Barthe, Jan Cederquist, Sabrina Tarento
Abstract. Most approaches to the formal analyses of cryptographic protocols make the perfect cryptography assumption, i.e. the hypothese that there is no way to obtain knowledge about the plaintext...
Compositional verication of secure applet interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Abstract. Recent developments in mobile code and embedded systems have lead to an increased interest in open platforms, i.e. platforms which enable dierent applications to interact in a dynamic...
T.: CPS translating inductive and coinductive types (extended abstract (2002)
We investigate CPS translatability of typed -calculi with inductive and coinductive types. We show that tenable Plotkin-style call-by-name CPS translations exist for simply typed -calculi with a...
T.: CPS translating inductive and coinductive types (extended abstract (2002)
We investigate CPS translatability of typed -calculi with inductive and coinductive types. We show that tenable Plotkin-style call-by-name CPS translations exist for simply typed -calculi with a...
Compositional verification of secure applet interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Abstract. Recent developments in mobile code and embedded systems have lead to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic...
Compositional Verification of Secure Applet Interactions (2002)
Gilles Barthe, Dilian Gurov, Marieke Huisman
Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment....
Modular Specification of Frame Properties in JML (2001)
Kees Huizing, Ruurd Kuiper, Davide Ancona, Giovanni Lagorio, ...
Program Committee:
A Formal Executable Semantics of the JavaCard Platform (2001)
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette
Abstract. We present a formal executable speci cation of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Veri er (BCV). Moreover, we relate both...
Barthe, Gilles, Gurov, Dilian, Huisman, Marieke
The paper presents a compositional program model of multi-application programs and sketches a framework for compositional specification and verification of temporal properties of such programs.
Constructor subtyping in the Calculus of Inductive Constructions (2000)
Gilles Barthe, Femke Van Raamsdonk
The Calculus of Inductive Constructions (CIC) is a powerful type system, featuring dependent types and inductive definitions, that forms the basis of proof-assistant systems such as Coq and Lego. We...
Constructor subtyping : extended version (1999)
Constructor subtyping is a form of subtyping in which an inductive type $\sigma$ is viewed as a subtype of another inductive type $\tau$ if $\tau$ has more elements than $\sigma$. Its (potential)...
Constructor subtyping is a form of subtyping in which an inductive type A is viewed as a subtype of another inductive type B if B has more constructors than A. Its (potential) uses include proof...
Gilles Barthe, Maria Joao Frade
Constructor subtyping is a form of subtyping in which an inductive type is viewed as a subtype of another inductive type Ï if Ï has more constructors than. As suggested in [5, 12], its...
Gilles Barthe, Maria Jo~ao Frade
Abstract. Constructor subtyping is a form of subtyping in which an inductive type oe is viewed as a subtype of another inductive type if has more constructors than oe. As suggested in [5, 12], its...
Existence and uniqueness of normal forms in pure type systems with βη-conversion (1999)
Pure Type Systems (PTS fi s) provide a parametric framework for typed-calculi `a la Church [1, 2, 10, 11]. One important aspect of PTS fi s is to feature a definitional equality based on...
Abstract. We prove strong normalization of fi-reduction+j-expansion for the Calculus of Constructions, thus providing the first strong normalization result for fi-reduction+j-expansion in calculi of...
Gilles Barthe, Maria João Frade, Maria Jo~ao Frade
. Constructor subtyping is a form of subtyping in which an inductive type oe is viewed as a subtype of another inductive type ø if ø has more constructors than oe. As suggested in [5, 12], its...
Constructor Subtyping (extended Version) (1999)
Gilles Barthe, Maria João Frade, Maria Jo~ao Frade
Constructor subtyping is a form of subtyping in which an inductive type sigma is viewed as a subtype of another inductive type tau if tau has more constructors than sigma. As suggested in [5, 12],...
The semi-full closure of Pure Type Systems (1998)
Abstract. We show that every functional Pure Type System may be extended to a semi-full Pure Type System. Moreover, the extension is conservative and preserves weak normalization. Based on these...
An induction principle for Pure Type Systems (1998)
Gilles Barthe, John Hatclioe, Morten Heine
We present an induction principle for Pure Type Systems and use that principle to dene CPS translations and to solve the problem of Expansion Postponement for a large class of Pure Type Systems. Our...
An induction principle for Pure Type Systems (1998)
Gilles Barthe, John Hatclioe, Morten Heine
We present an induction principle for Pure Type Systems and use that principle to dene CPS translations and to solve the problem of Expansion Postponement for a large class of Pure Type Systems. Our...
Type-checking injective Pure Type Systems (1998)
Injective Pure Type Systems form a large class of Pure Type Systems for which one can compute by purely syntactic means two sorts elmt(\GammajM ) and sort(\GammajM ), where \Gamma is a pseudo-context...
Monadic Type Systems: Pure Type Systems for Impure Settings (1998)
Gilles Barthe, John Hatcliff, Peter Thiemann
Pure type systems and computational monads are two parameterized frameworks that have proved to be quite useful in both theoretical and practical applications. We join the foundational concepts of...
CPS Translations and Applications: The Cube and Beyond (1998)
Continuation passing style (CPS) translations of typed -calculi have numerous applications. However, the range of these applications has been confined by the fact that CPS translations are known for...
An Induction Principle for Pure Type Systems (1998)
We present an induction principle for Pure Type Systems and use that principle to define CPS translations and to solve partially the -- open -- problem of Expansion Postponement. Our principle...
Gilles Barthe, John Hatcliff, Morten Heine Srensen
The Barendregt-Geuvers-Klop conjecture states that every weakly normalizing pure type system is also strongly normalizing. We show that this is true for a uniform class of systems which includes,...
Termination of algebraic type systems: the syntactic approach (1997)
Gilles Barthe, Femke Van Raamsdonk
Combinations of type theory and rewriting are of obvious interest for the study of higher-order programming and program transformation with algebraic data types specifications; more recently, they...
A Notion of Classical Pure Type System (1997)
Gilles Barthe, John Hatcliff, Morten Heine Srensen
We present a notion of classical pure type system, which extends the formalism of pure type system with a double negation operator. 1 Introduction It is an old idea that proofs in formal logics are...
A Notion of Classical Pure Type System (1997)
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
this paper, we nevertheless establish that it is possible to define a notion of classical pure type system (CPTS) which has suitable properties for systems of dependent types. We do not claim that...
Termination of Algebraic Type Systems: The Syntactic Approach (1997)
Gilles Barthe, Femke Van Raamsdonk
this paper, especially termination by stability, may also be adapted to yield similar results for confluence, extending the `confluence by stability' result in [16].
Monadic Type Systems: Pure Type Systems for Impure Settings (Preliminary Report) (1997)
Gilles Barthe, John Hatcliff, Peter Thiemann
Pure type systems and computational monads are two parameterized frameworks that have proved to be quite useful in both theoretical and practical applications. We join the foundational concepts of...
Reflections on Reflections (1997)
Gilles Barthe, John Hatcliff, Morten Heine Sørensen, Morten Heine S��rensen
. In the functional programming literature, compiling is often expressed as a translation between source and target program calculi. In recent work, Sabry and Wadler proposed the notion of a...
Explicit Substitutions for Control Operators (1997)
Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos
. The \Delta-calculus is a -calculus with a local operator closely related to normalisation procedures in classical logic and control operators in functional programming. We introduce \Deltaexp, an...
Implicit coercions in type systems (1996)
Abstract. We propose a notion of pure type system with implicit coercions. In our framework, judgements are extended with a context of coercions \Delta and the application rule is modified so as to...
Modular Properties of Algebraic Type Systems (1996)
. We introduce the framework of algebraic type systems, a generalisation of pure type systems with higher order rewriting `a la JouannaudOkada, and initiate a generic study of the modular properties...
CPS Translations and Applications: The Cube and Beyond (1996)
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
this paper we introduce CPS translations of the -cube [2], including the calculus of constructions and the LF calculus. This is then generalized further to what we call persistent pure type systems....
. We introduce a type-theoretical framework in which canonical term rewriting systems can be represented faithfully both from the logical and the computational points of view. The framework is based...
Modular Properties of Algebraic Pure Type Systems (1996)
. We introduce the framework of algebraic pure type systems, a generalisation of pure type systems with higher order rewriting `a la Jouannaud-Okada, and initiate a generic study of the modular...
CPS Translations and Applications: The Cube and Beyond (1996)
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
Continuation passing style (CPS) translations of typed -calculi numerous applications. However, the range of these applications is confined by the fact that CPS translations are known for...
CPS Translations and Applications: The Cube and Beyond (1996)
Gilles Barthe, John Hatcliff, Morten Heine Sørensen, Morten Heine S��rensen
Continuation passing style (CPS) translations of typed -calculi have numerous applications. However, the range of these applications have been confined thus far by the fact that CPS translations are...
CPS Translations and Applications: the Cube and Beyond (preliminary report) (1996)
Gilles Barthe, John Hatcliff, Morten Heine S��rensen
Continuation passing style (CPS) translations of typed -calculi have numerous applications. However, the range of these applications have been confined thus far by the fact that CPS translations are...
Domain-free pure type systems (1995)
Gilles Barthe, Morten Heine S#rensen
Pure type systems make use of domain-full-abstractions x: D: M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free-abstractions x: M. Domain-free...
A Simple Abstract Semantics for Equational Theories (1995)
. We show that a suitable abstraction of the notion of termalgebra, called compositum, can be used to capture in a precise mathematical way the intuition that the category of algebras of most...
Extensions of Pure Type Systems (1995)
. We extend pure type systems with quotient types and subset types and establish an equivalence between four strong normalisation problems: subset types, quotient types, definitions and the so-called...
Formalising mathematics in UTT: fundamentals and case studies (1994)
We give a detailed account of the use of type theory as a foundational language to formalise mathematics. We develop in the type system UTT a coherent approach to naive set theory and elementary...
Domain-Free Pure Type Systems (1993)
Gilles Barthe, Morten Heine Sørensen, Morten Heine S��rensen
Pure type systems make use of domain-full -abstractions x : D : M . We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free -abstractions x : M ....
Formalization in Coq of the Java Card Virtual Machine
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette, Simão Sousa, Shen-Wei Yu
Introduction Java has quickly become a standard for Internet and, through Java Card, for smartcard programming, putting security issues at stake. Yet recent research has unveiled several problems in...