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 soundness; monotonic separation algebra

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03B70: Logic in computer science

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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