It is our pleasure to anounce the availability of the following paper:
A Dependently Typed Assembly Language
Hongwei Xi and Robert Harper
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 assembly level. DTAL
overcomes several significant limitations in recently proposed
low-level languages including Java bytecode language and a typed
assembly language, which prevent them from handling certain important
compiler optimizations such as run-time array bound check elimination.
We also mention a compiler which generates code in DTAL from compiling
some high-level programs.
The paper is available as an OGI tech report: CSE-99-008, or as
Also an extended abstract is provided for a smooth introduction.
\~~~~/ \\ // \\ // @ Mail: firstname.lastname@example.org
C-o^o, ))__|| \\__//_ // \\ Url: http://www.cse.ogi.edu/~hongwei
( ^ ) ))__|| \--/-\\ \\ Tel: +1 503 748 1584 (office)
/ \V\ )) || // \\ \\ Fax: +1 503 748 1553 (department)
------ // || o // \\ \\//
Department of Computer Science and Engineering
Oregon Graduate Institute of Science and Technology
P. O. Box 91000, Portland, OR 97291-1000, USA