-
- Greg Morrisett
- Cornell Univ., Ithaca, NY
-
- David Walker
- Cornell Univ., Ithaca, NY
-
- Karl Crary
- Carnegie Mellon Univ., Pittsburgh, PA
-
- Neal Glew
- Cornell Univ., Ithaca, NY
抄録
<jats:p>We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.</jats:p>
収録刊行物
-
- ACM Transactions on Programming Languages and Systems
-
ACM Transactions on Programming Languages and Systems 21 (3), 527-568, 1999-05
Association for Computing Machinery (ACM)
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1360294647042622976
-
- NII論文ID
- 30001912815
-
- ISSN
- 15584593
- 01640925
-
- データソース種別
-
- Crossref
- CiNii Articles