Security-typed programming within dependently typed programming

DOI10.1145/1863543.1863569MaRDI QIDQ5176937zbMATH OpenOpenAlexFDO

Authors Jamie Morgenstern, Daniel R. Licata

Publication date 5 March 2015

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

Full work available at URL https://doi.org/10.1145/1863543.1863569

zbMATH Keywords

Agdadependent typessecurity typed programming

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Dependent information flow types
• Secure distributed programming with value-dependent types
• Secure distributed programming with value-dependent types
• scientific article; zbMATH DE number 2163037
• Dependently typed programming in Agda

Cited in

(6)

• Aglet
• Secure distributed programming with value-dependent types
• Secure distributed programming with value-dependent types
• Flexible dynamic information flow control in the presence of exceptions
• scientific article; zbMATH DE number 2163037 (Why is no real title available?)
• scientific article; zbMATH DE number 1948407 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ynot
• AURA
• Agda

This page was built for publication: Security-typed programming within dependently typed programming

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