Secure Distributed Programming with Value-dependent Types

Abstract : Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications and proofs becomes challenging. We present F, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F and controls their interaction. F subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs partially mechanized in Coq) and logical consistency for F.
Type de document :
Communication dans un congrès
16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan. 2011
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger
Contributeur : Pierre-Yves Strub <>
Soumis le : mardi 8 novembre 2011 - 11:24:41
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : jeudi 15 novembre 2012 - 11:26:14


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00596715, version 1



Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, et al.. Secure Distributed Programming with Value-dependent Types. 16th ACM SIGPLAN International Conference on Functional Programming, Sep 2011, Tokyo, Japan. 2011. 〈inria-00596715〉



Consultations de la notice


Téléchargements de fichiers