Secure distributed programming with value-dependent types

DOI10.1145/2034773.2034811zbMath1323.68229OpenAlexW4240226860MaRDI QIDQ5176981

Nikhil Swamy, Juan Chen, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang, Cédric Fournet

Publication date: 5 March 2015

Published in: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00939188/file/secure-distributed-programming-with-value-dependent-types-jfp-1.pdf

zbMATH Keywords

security typesrefinement types

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Unified Syntax with Iso-types ⋮ A Delta for Hybrid Type Checking ⋮ Program synthesis for interactive-security systems ⋮ The essence of ornaments ⋮ The Essence of Functional Programming on Semantic Data ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Global progress for dynamically interleaved multiparty sessions ⋮ A Classical Realizability Model for a Semantical Value Restriction ⋮ Cryptographic Verification by Typing for a Sample Protocol Implementation ⋮ A Gentle Introduction to Multiparty Asynchronous Session Types ⋮ F* ⋮ Information Flow Analysis for Valued-Indexed Data Security Compartments ⋮ Proof-Carrying Code in a Session-Typed Process Calculus ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs

Uses Software

• Coq
• Ott
• z3
• AURA