A semantic model of types and machine instructions for proof-carrying code

DOI10.1145/325694.325727zbMath1323.68351OpenAlexW2153297607MaRDI QIDQ5178856

Andrew W. Appel, Amy P. Felty

Publication date: 17 March 2015

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

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

Mathematics Subject Classification ID

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

Related Items (4)

Proof-carrying code from certified abstract interpretation and fixpoint compression ⋮ Efficient Substitution in Hoare Logic Expressions ⋮ Type Theories from Barendregt’s Cube for Theorem Provers ⋮ Automated techniques for provably safe mobile code.

This page was built for publication: A semantic model of types and machine instructions for proof-carrying code