scientific article; zbMATH DE number 7649976

DOI10.4230/LIPICS.ITP.2019.27MaRDI QIDQ5875439zbMATH OpenFDO

Authors Robert Sison, Toby Murray

Publication date 3 February 2023

Full work available at URL https://arxiv.org/abs/1907.00713

zbMATH Keywords

concurrencyinformation flow securitysecure compilationverification

Mathematics Subject Classification ID

Cites work

• A formally verified compiler back-end
• CakeML
• Dependent information flow types
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Security types preserving compilation

Cited in

(5)

• Information-flow control on ARM and POWER multicore processors
• Efficient Information-Flow Verification Under Speculative Execution
• scientific article; zbMATH DE number 2104621 (Why is no real title available?)
• Cogent: uniqueness types and certifying compilation
• scientific article; zbMATH DE number 7774275 (Why is no real title available?)

Describes a project that uses

Uses Software

• Archive of Formal Proofs

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875439)