Gilles Barthe

Santiago Zanella Béguelin

Sylvain Heraud

Proceedings of the Formal Aspects in Security and Trust, 5th International Workshop, 2008

An Introduction to Certificate Translation.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Security Analysis and Design V, 2008

Certificate translation for specification-preserving advices.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, 2008

Certificate Translation in Abstract Interpretation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2008

Type-Based Termination with Sized Products.

[BibT_eX]

[DOI]

Colin Riba

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Tractable Enforcement of Declassification Policies.

[BibT_eX]

[DOI]

Salvador Cavadini

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Preservation of Proof Obligations from Java to the Java Virtual Machine.

[BibT_eX]

[DOI]

Mariela Pavlova

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Certificate Translation.

[BibT_eX]

[DOI]

Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

Certified Reasoning in Memory Hierarchies.

[BibT_eX]

[DOI]

Jorge Luis Sacchini

Proceedings of the Programming Languages and Systems, 6th Asian Symposium, 2008

2007

Secure information flow for a concurrent language with scheduling.

[BibT_eX]

[DOI]

Leonor Prensa Nieto

J. Comput. Secur., 2007

Security types preserving compilation.

[BibT_eX]

[DOI]

Amitabh Basu

Comput. Lang. Syst. Struct., 2007

The MOBIUS Proof Carrying Code Infrastructure.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

07091 Abstracts Collection - Mobility, Ubiquity and Security.

[BibT_eX]

[DOI]

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

07091 Executive Summary - Mobility, Ubiquity and Security.

[BibT_eX]

[DOI]

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

2006

Remarks on the equational theory of non-normalizing pure type systems.

[BibT_eX]

[DOI]

Thierry Coquand

J. Funct. Program., 2006

MOBIUS: Mobility, Ubiquity, Security.

[BibT_eX]

[DOI]

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Deriving an Information Flow Checker and Certifying Compiler for Java.

[BibT_eX]

[DOI]

David A. Naumann

Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.

[BibT_eX]

[DOI]

Fernando Pastawski

Proceedings of the Logic for Programming, 2006

JACK - A Tool for Validation of Security and Behaviour of Java Applications.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

2005

A computational view of implicit coercions in type theory.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2005

Tool-Assisted Specification and Verification of Typed Low-Level Languages.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Preventing Timing Leaks Through Transactional Branching Instructions.

[BibT_eX]

[DOI]

Martijn Warnier

Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005

Non-interference for a JVM-like language.

[BibT_eX]

[DOI]

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Practical Inference for Type-Based Termination in a Polymorphic Setting.

[BibT_eX]

[DOI]

Fernando Pastawski

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Precise Analysis of Memory Consumption using Program Logics.

[BibT_eX]

[DOI]

Mariela Pavlova

Gerardo Schneider

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Proof Obligations Preserving Compilation.

[BibT_eX]

[DOI]

Ando Saabas

Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

Formal Methods for Smartcard Security.

[BibT_eX]

[DOI]

Guillaume Dufay

Proceedings of the Foundations of Security Analysis and Design III, 2005

2004

Type-based termination of recursive definitions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2004

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming.

[BibT_eX]

[DOI]

Peter Dybjer

Peter Thiemann

J. Funct. Program., 2004

Security Types Preserving Compilation: (Extended Abstract).

[BibT_eX]

[DOI]

Amitabh Basu

Proceedings of the Verification, 2004

A Machine-Checked Formalization of the Random Oracle Model.

[BibT_eX]

[DOI]

Sabrina Tarento

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Tool-Assisted Framework for Certified Bytecode Verification.

[BibT_eX]

[DOI]

Guillaume Dufay

Proceedings of the Fundamental Approaches to Software Engineering, 2004

Formally verifying information flow type systems for concurrent and thread systems.

[BibT_eX]

[DOI]

Leonor Prensa Nieto

Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, 2004

Enforcing High-Level Security Properties for Applets.

[BibT_eX]

[DOI]

Proceedings of the Smart Card Research and Advanced Applications VI, 2004

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.

[BibT_eX]

[DOI]

Jan Cederquist

Sabrina Tarento

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Setoids in type theory.

[BibT_eX]

[DOI]

Venanzio Capretta

Olivier Pons

J. Funct. Program., 2003

Validation of the JavaCard Platform with Implicit Induction Techniques.

[BibT_eX]

[DOI]

Sorin Stratulat

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Pure patterns type systems.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

2002

Preface.

[BibT_eX]

[DOI]

Peter Thiemann

Proceedings of the International Workshop in Types in Programming, 2002

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2002

Efficient Reasoning about Executable Specifications in Coq.

[BibT_eX]

[DOI]

Pierre Courtieu

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

CPS translating inductive and coinductive types.

[BibT_eX]

[DOI]

Tarmo Uustalu

Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '02), 2002

Compositional Verification of Secure Applet Interactions.

[BibT_eX]

[DOI]

Dilian Gurov

Marieke Huisman

Proceedings of the Fundamental Approaches to Software Engineering, 2002

Tool-Assisted Specification and Verification of the JavaCard Platform.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 2002

2001

Weak normalization implies strong normalization in a class of non-dependent pure type systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

An induction principle for pure type systems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

Type Isomorphisms and Proof Reuse in Dependent Type Theory.

[BibT_eX]

[DOI]

Olivier Pons

Proceedings of the Foundations of Software Science and Computation Structures, 2001

A Formal Executable Semantics of the JavaCard Platform.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2001

Jakarta: A Toolset for Reasoning about JavaCard.

[BibT_eX]

[DOI]

Proceedings of the Smart Card Programming and Security, 2001

Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo).

[BibT_eX]

[DOI]

Blas C. Ruiz Jiménez

Proceedings of the APPIA-GULP-PRODE 2001: Joint Conference on Declarative Programming, 2001

2000

Domain-free pure type systems.

[BibT_eX]

[DOI]

J. Funct. Program., 2000

Static Reduction Analysis for Imperative Object Oriented Languages.

[BibT_eX]

[DOI]

Bernard P. Serpette

Proceedings of the Logic for Programming and Automated Reasoning, 2000

Constructor Subtyping in the Calculus of Inductive Constructions.

[BibT_eX]

[DOI]

Femke van Raamsdonk

Proceedings of the Foundations of Software Science and Computation Structures, 2000

An Introduction to Dependent Type Theory.

[BibT_eX]

[DOI]

Thierry Coquand

Proceedings of the Applied Semantics, International Summer School, 2000

1999

CPS Translations and Applications: The Cube and Beyond.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 1999

Type-checking injective pure type systems.

[BibT_eX]

[DOI]

J. Funct. Program., 1999

Order-Sorted Inductive Types.

[BibT_eX]

[DOI]

Inf. Comput., 1999

Expanding the Cube.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structure, 1999

Partial Evaluation and Non-interference for Object Calculi.

[BibT_eX]

[DOI]

Bernard P. Serpette

Proceedings of the Functional and Logic Programming, 4th Fuji International Symposium, 1999

Constructor Subtyping.

[BibT_eX]

[DOI]

Maria João Frade

Proceedings of the Programming Languages and Systems, 1999

1998

The Semi-Full Closure of Pure Type Systems.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

The Relevance of Proof-Irrelevance.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1997

Monadic Type Systems: Pure Type Systems for Impure Settings.

[BibT_eX]

[DOI]

Peter Thiemann

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

A notion of classical pure type system.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, 1997

Reflections on Reflections.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1997

Termination of Algebraic Type Systems: The Syntactic Approach.

[BibT_eX]

[DOI]

Femke van Raamsdonk

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

Explicit Substitutions for the Lambda-Calculus.

[BibT_eX]

[DOI]

Fairouz Kamareddine

Alejandro Ríos

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

1996

Towards Lean Proof Checking.

[BibT_eX]

[DOI]

Hugo Elbers

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

On the Subject Reduction Property for Algebraic Type Systems.

[BibT_eX]

[DOI]

Paul-André Melliès

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995

A Two-Level Approach Towards Lean Proof-Checking.

[BibT_eX]

[DOI]

Mark Ruys

Henk Barendregt

Proceedings of the Types for Proofs and Programs, 1995

Implicit Coercions in Type Systems.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1995

Extensions of Pure Type Systems.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1995

Modular Properties of Algebraic Type Systems.

[BibT_eX]

[DOI]

Herman Geuvers

Proceedings of the Higher-Order Algebra, 1995

A Simple Abstract Semantics for Equational Theories.

[BibT_eX]

[DOI]

Proceedings of the Fundamentals of Computation Theory, 10th International Symposium, 1995

Congruence Types.

[BibT_eX]

[DOI]