Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types

DOI10.1016/j.entcs.2020.08.005OpenAlexW3092413010WikidataQ113317317 ScholiaQ113317317MaRDI QIDQ2229149

Cecilia Manzino, Alberto Pardo

Publication date: 22 February 2021

Full work available at URL: https://doi.org/10.1016/j.entcs.2020.08.005

zbMATH Keywords

Agdanon-interferencetype safetydependently-typed programminginformation flow type systems

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Haskell
• Agda

Cites Work

• Concrete Semantics
• From Exponential to Polynomial-Time Security Typing via Principal Types
• Dependently Typed Programming in Agda
• A lattice model of secure information flow
• Dependent Types at Work
• On flow-sensitive security types

This page was built for publication: Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types