@inproceedings{0c1c00e982e941179f0e49ec126ac697,
title = "Construction of a semantic model for a typed assembly language",
abstract = "TypedAssembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to build semantic models for typing judgments in TALs based on an induction technique, so that both the type-safety theorem and the typing rules can be proved as lemmas in a simple logic. We demonstrate this technique by giving a complete model to a sampleTAL. This model allows a typing derivation to be interpreted as a machine-checkable safety proof at the machine level.",
author = "Gang Tan and Appel, {Andrew W.} and Swadi, {Kedar N.} and Dinghao Wu",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2004.; 5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004 ; Conference date: 11-01-2004 Through 13-01-2004",
year = "2004",
doi = "10.1007/978-3-540-24622-0_4",
language = "English (US)",
isbn = "9783540208037",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "30--43",
editor = "Bernhard Steffen and Giorgio Levi",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings",
address = "Germany",
}