A Dependently Typed Assembly Language

We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at the assembly level. DTAL improves upon TAL, enabling certain important compiler optimizations such as run-time array...

Full description

Bibliographic Details
Main Authors: Hongwei Xi, Robert Harper
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: ACM Press 1999
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905
http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.29.1905
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.29.1905 2023-05-15T16:01:40+02:00 A Dependently Typed Assembly Language Hongwei Xi Robert Harper The Pennsylvania State University CiteSeerX Archives 1999 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905 http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps en eng ACM Press http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905 http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps text 1999 ftciteseerx 2016-01-07T21:28:52Z We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at the assembly level. DTAL improves upon TAL, enabling certain important compiler optimizations such as run-time array bound check elimination and tag check elimination. Also, DTAL formally addresses the issue of representing sum types at assembly level, making it suitable for handling not only datatypes in ML but also dependent datatypes in Dependent ML (DML). Text DML Unknown
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at the assembly level. DTAL improves upon TAL, enabling certain important compiler optimizations such as run-time array bound check elimination and tag check elimination. Also, DTAL formally addresses the issue of representing sum types at assembly level, making it suitable for handling not only datatypes in ML but also dependent datatypes in Dependent ML (DML).
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Hongwei Xi
Robert Harper
spellingShingle Hongwei Xi
Robert Harper
A Dependently Typed Assembly Language
author_facet Hongwei Xi
Robert Harper
author_sort Hongwei Xi
title A Dependently Typed Assembly Language
title_short A Dependently Typed Assembly Language
title_full A Dependently Typed Assembly Language
title_fullStr A Dependently Typed Assembly Language
title_full_unstemmed A Dependently Typed Assembly Language
title_sort dependently typed assembly language
publisher ACM Press
publishDate 1999
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905
http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps
genre DML
genre_facet DML
op_source http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905
http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397433533693952

Similar Items