sign in
english version rss feed

inria-00596715, version 1

Secure Distributed Programming with Value-dependent Types

Nikhil Swamy () 1, Juan Chen () 1, Cédric Fournet () 2, Pierre-Yves Strub () 3, Karthikeyan Bhargavan () 34, Jean Yang () 5

16th ACM SIGPLAN International Conference on Functional Programming (2011)

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.

  • Domain : Computer Science/Programming Languages
    Computer Science/Logic in Computer Science
  • Comment : Related Projects * F*: A Verifying ML Compiler for Distributed Programming
 
  • inria-00596715, version 1
  • oai:hal.inria.fr:inria-00596715
  • From: 
  • Submitted on: Tuesday, 8 November 2011 11:24:41
  • Updated on: Tuesday, 8 November 2011 11:30:53
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...