G. Barthe, M. J. Frade, T. Uustalu
Under consideration for publication in Math. Struct. in Comp. Science Type-based termination of recursive de nitions
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (2004)
Barthe, G., Cederquist, J.G., Tarento, S.
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 pertaining...
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (2004)
Barthe, G., Cederquist, Dr. J.G., Tarento, S.
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 pertaining...
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (2004)
Barthe, G., Cederquist, J.G., Tarento, S.
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 pertaining...
RESET Roadmap for European research on Smartcard rElated Technologies (2003)
Gras, F., Le Dantec, B., Trebucq, O., Cucinelli, B, Leduc, M., Simplot, D., ...
The objective of RESET (Roadmap for European research on Smartcard related Technologies) is to investigate the RTD needs corresponding to current and expected future technology gaps, identified by...
RESET Roadmap for European research on Smartcard rElated Technologies (2003)
Gras, F., Le Dantec, B., Trebucq, O., Cucinelli, B, Leduc, M., Simplot, D., ...
The objective of RESET (Roadmap for European research on Smartcard related Technologies) is to investigate the RTD needs corresponding to current and expected future technology gaps, identified by...
RESET Roadmap for European research on Smartcard rElated Technologies (2003)
Gras, F., Le Dantec, B., Trebucq, O., Cucinelli, B, Leduc, M., Simplot, D., ...
The objective of RESET (Roadmap for European research on Smartcard related Technologies) is to investigate the RTD needs corresponding to current and expected future technology gaps, identified by...
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines (2002)
G. Barthe, G. Dufay, L. Jakubiec
Many formal specications of the JavaCard Virtual Machine are defensive, in that they perform type-checking at run-time. In this paper, we show how to construct from such a defensive virtual machine...
Jakarta: A Toolset for Reasoning about JavaCard (2001)
G. Barthe, G. Dufay, M. Huisman
JavaCard [22] is a dialect of Java that enables Java technology to run on new generation smart cards and other devices with limited memory. As JavaCard is becoming increasingly popular, there has...
On the Subject Reduction Property for Algebraic Type Systems (1997)
Algebraic type systems provide a general framework for the study of the interaction between typed -calculi and typed rewriting systems. A major problem in the development of a general theory for...
A constructive proof of the Heine-Borel covering theorem for formal reals (1996)
Barthe, G., Cederquist, Dr. J.G., Tarento, S.
The continuum is here presented as a formal space by means of a finitary inductive definition. In this setting a constructive proof of the Heine-Borel covering theorem is given.
A constructive proof of the Heine-Borel covering theorem for formal reals (1996)
Barthe, G., Cederquist, J.G., Tarento, S.
The continuum is here presented as a formal space by means of a finitary inductive definition. In this setting a constructive proof of the Heine-Borel covering theorem is given.
On the Subject Reduction Property for Algebraic Type Systems (1996)
Abstract. Algebraic type systems provide a general framework for the study of the interaction between typed-calculi and typed rewriting systems. A major problem in the development of a general theory...
A Two-Level Approach towards Lean Proof-Checking (1996)
. 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...
Towards Lean Proof Checking (1996)
. Logical formal systems are inefficient at computations. In order to increase their efficiency, we aim to extend these systems with computational power. In this paper, we suggest a general, powerful...
Towards Lean Proof Checking (1996)
Barthe And, G. Barthe, H. Elbers
. Logical formal systems are inefficient at computations. In order to increase their efficiency, we aim to extend these systems with computational power. In this paper, we suggest a general, powerful...