TALx86
Typed assembly language (TAL). TALx86: A Realistic Typed Assembly Language. In previous work, we presented a formalism for a statically typed, idealized assembly language called TAL. The goal of TAL was to provide an extremely lowlevel, statically-typed target language that is better suited than Java bytecodes for supporting a wide variety of source languages and a number of important optimizations. In this paper, we present our progress in defining and implementinga realistic typed assembly language called TALx86. The TALx86 instructions comprise a relatively complete fragment of the Intel IA32 (32-bit 80x86 flat model) assembly language and are thus executable on processors such as the Intel Pentium. The type system for the language incorporates a number of advanced features necessary for safely compiling large programs to good code. To motivate the design of the type system, we present a type-safe, C-based language called Popcorn and show how various Popcorn features are compiled to TALx86.
Keywords for this software
References in zbMATH (referenced in 45 articles )
Showing results 1 to 20 of 45.
Sorted by year (- Haller, Philipp; Miller, Heather: A reduction semantics for direct-style asynchronous observables (2019)
- Kouzapas, Dimitrios; Pérez, Jorge A.; Yoshida, Nobuko: On the relative expressiveness of higher-order session processes (2019)
- Laneve, Cosimo; Lienhardt, Michael; Pun, Ka I.; Román-Díez, Guillermo: Time analysis of actor programs (2019)
- Kouzapas, Dimitrios; Pérez, Jorge A.; Yoshida, Nobuko: On the relative expressiveness of higher-order session processes (2016)
- Patrignani, Marco; Clarke, Dave: Fully abstract trace semantics for protected module architectures (2015)
- Schmidt-Schauß, Manfred; Sabel, David; Niehren, Joachim; Schwinghammer, Jan: Observational program calculi and the correctness of translations (2015)
- Zunino, Roberto; Nikolić, Đurica; Priami, Corrado; Kahramanoğulları, Ozan; Schiavinotto, Tommaso: (\ell): an imperative DSL to stochastically simulate biological systems (2015) ioport
- Honda, Kohei; Yoshida, Nobuko; Berger, Martin: An observationally complete program logic for imperative higher-order functions (2014)
- Appel, Andrew W.; Dockins, Robert; Leroy, Xavier: A list-machine benchmark for mechanized metatheory (2012)
- Myreen, Magnus O.; Gordon, Michael J. C.: Function extraction (2012)
- Bolduc, Claude; Ktari, Béchir: Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra (2011)
- Langar, Mahjoub; Mejri, Mohamed; Adi, Kamel: Formal enforcement of security policies on concurrent systems (2011)
- Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
- Wang, Shengyuan; Dong, Yuan: A verifiable low-level concurrent programming model based on colored Petri nets (2011)
- Wang, Wei: Certifying assembly programs with trails (2011)
- Rudolph, Johannes; Thiemann, Peter: \textscMnemonics: type-safe bytecode generation at run time (2010)
- Feng, Xinyu; Shao, Zhong; Guo, Yu; Dong, Yuan: Certifying low-level programs with hardware interrupts and preemptive threads (2009)
- Leroy, Xavier: A formally verified compiler back-end (2009)
- Albert, Elvira; Puebla, Germán; Hermenegildo, Manuel: Abstraction-carrying code: a model for mobile code safety (2008)
- Iwama, Futoshi; Kobayashi, Naoki: A new type system for JVM lock primitives (2008)