A type system for certified binaries

DOI10.1145/503272.503293MaRDI QIDQ5178908zbMATH OpenOpenAlexFDO

Authors Zhong Shao, Bratin Saha, Valery Trifonov, Nikolaos S. Papaspyrou

Publication date 17 March 2015

Published in Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Cryptography (94A60) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• An expressive, scalable type theory for certified code
• Verified bytecode verification and type-certifying compilation
• scientific article; zbMATH DE number 1956458
• A type system for the Java bytecode language and verifier
• Formalizing the SAFECode type system
• scientific article; zbMATH DE number 1746459
• A type inference algorithm for secure ambients

Cited in

(8)

• Cogent: uniqueness types and certifying compilation
• A self-certifying compilation framework for WebAssembly
• Testing your (static analysis) truths
• An expressive, scalable type theory for certified code
• Type-level computation using narrowing in \(\Omega\)mega
• ANF preserves dependent types up to extensional equality
• Type-safe code transformations in Haskell
• A dependently typed multi-stage calculus

This page was built for publication: A type system for certified binaries

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