Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Pierre-Yves Strub Connect in order to contact the contributor
Submitted on : Tuesday, November 8, 2011 - 11:24:41 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:20 AM
Long-term archiving on: : Thursday, November 15, 2012 - 11:26:14 AM


Files produced by the author(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. ⟨inria-00596715⟩



Les métriques sont temporairement indisponibles