Syntactic soundness proof of a type-and-capability system with hidden state

DOI10.1017/S0956796812000366zbMath1262.68031MaRDI QIDQ4912884

François Pottier

Publication date: 28 March 2013

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

machine-checked proof of type soundnessmonotonic separation algebra

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

On models of higher-order separation logic ⋮ Bringing Order to the Separation Logic Jungle ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic

Uses Software

• CoLoR

Cites Work

• Unnamed Item
• Region-based memory management
• Resources, concurrency, and local reasoning
• Nominal techniques in Isabelle/HOL
• Polymorphic type inference and containment
• A simplified account of polymorphic references
• A syntactic approach to type soundness
• The locally nameless representation
• A canonical locally named representation of binding
• Safe manual memory management in Cyclone
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Local Reasoning for Storable Locks and Threads
• Hoare type theory, polymorphism and separation
• Realisability semantics of parametric polymorphism, general references and recursive types
• An ideal model for recursive polymorphic types
• FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
• Step-Indexed Kripke Model of Separation Logic for Storable Locks

This page was built for publication: Syntactic soundness proof of a type-and-capability system with hidden state