ABSTRACT 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 Author: Hongwei Xi
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.3494
http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.83.3494
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.83.3494 2023-05-15T16:01:40+02:00 ABSTRACT A Dependently Typed Assembly Language Hongwei Xi The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.3494 http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.3494 http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf text ftciteseerx 2016-01-08T19:24:38Z 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). 1. 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). 1.
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Hongwei Xi
spellingShingle Hongwei Xi
ABSTRACT A Dependently Typed Assembly Language
author_facet Hongwei Xi
author_sort Hongwei Xi
title ABSTRACT A Dependently Typed Assembly Language
title_short ABSTRACT A Dependently Typed Assembly Language
title_full ABSTRACT A Dependently Typed Assembly Language
title_fullStr ABSTRACT A Dependently Typed Assembly Language
title_full_unstemmed ABSTRACT A Dependently Typed Assembly Language
title_sort abstract a dependently typed assembly language
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.3494
http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf
genre DML
genre_facet DML
op_source http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.3494
http://www.eecs.harvard.edu/~greg/cs255sp2004/xi2001dtal.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397434972340224

Similar Items