A type system for certified binaries
DOI10.1145/503272.503293zbMATH Open1323.68383OpenAlexW1995594295MaRDI QIDQ5178908FDOQ5178908
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
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
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)
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
- A dependently typed multi-stage calculus
- Type-safe code transformations in Haskell
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)
