Automated techniques for provably safe mobile code.

DOI10.1016/S0304-3975(01)00201-8zbMath1064.68027OpenAlexW2041673946MaRDI QIDQ1853627

Yanyan Li

Publication date: 21 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00201-8

zbMATH Keywords

Proof-carrying codeType systemsCertifying compilersType safetyTyped assembly language

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Uses Software

• Twelf
• Elf
• TIL
• TALx86

Cites Work

• Stack-based typed assembly language
• A framework for defining logics
• Stack-based typed assembly language
• A dependently typed assembly language
• Resource bound certification
• A semantic model of types and machine instructions for proof-carrying code
• A type system for expressive security policies
• Elf: A meta-language for deductive systems
• On equivalence and canonical forms in the LF type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item