Semantic foundations for typed assembly languages

Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, Daniel C. Wang

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and Lc, a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and Lc to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler. To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations. This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.

Original languageEnglish (US)
Article number1709094
JournalACM Transactions on Programming Languages and Systems
Volume32
Issue number3
DOIs
StatePublished - Mar 1 2010

Fingerprint

Semantics
Polymorphism
Flow control
Specifications

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Ahmed, A., Appel, A. W., Richards, C. D., Swadi, K. N., Tan, G., & Wang, D. C. (2010). Semantic foundations for typed assembly languages. ACM Transactions on Programming Languages and Systems, 32(3), [1709094]. https://doi.org/10.1145/1709093.1709094
Ahmed, Amal ; Appel, Andrew W. ; Richards, Christopher D. ; Swadi, Kedar N. ; Tan, Gang ; Wang, Daniel C. / Semantic foundations for typed assembly languages. In: ACM Transactions on Programming Languages and Systems. 2010 ; Vol. 32, No. 3.
@article{f744a046335842de970b4aea96c44c69,
title = "Semantic foundations for typed assembly languages",
abstract = "Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and Lc, a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and Lc to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler. To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations. This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.",
author = "Amal Ahmed and Appel, {Andrew W.} and Richards, {Christopher D.} and Swadi, {Kedar N.} and Gang Tan and Wang, {Daniel C.}",
year = "2010",
month = "3",
day = "1",
doi = "10.1145/1709093.1709094",
language = "English (US)",
volume = "32",
journal = "ACM Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery (ACM)",
number = "3",

}

Semantic foundations for typed assembly languages. / Ahmed, Amal; Appel, Andrew W.; Richards, Christopher D.; Swadi, Kedar N.; Tan, Gang; Wang, Daniel C.

In: ACM Transactions on Programming Languages and Systems, Vol. 32, No. 3, 1709094, 01.03.2010.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Semantic foundations for typed assembly languages

AU - Ahmed, Amal

AU - Appel, Andrew W.

AU - Richards, Christopher D.

AU - Swadi, Kedar N.

AU - Tan, Gang

AU - Wang, Daniel C.

PY - 2010/3/1

Y1 - 2010/3/1

N2 - Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and Lc, a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and Lc to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler. To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations. This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.

AB - Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and Lc, a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and Lc to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler. To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations. This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.

UR - http://www.scopus.com/inward/record.url?scp=77949560721&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77949560721&partnerID=8YFLogxK

U2 - 10.1145/1709093.1709094

DO - 10.1145/1709093.1709094

M3 - Article

AN - SCOPUS:77949560721

VL - 32

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 3

M1 - 1709094

ER -