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

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

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)

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