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.


References in zbMATH (referenced in 45 articles )

Showing results 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Haller, Philipp; Miller, Heather: A reduction semantics for direct-style asynchronous observables (2019)
  2. Kouzapas, Dimitrios; Pérez, Jorge A.; Yoshida, Nobuko: On the relative expressiveness of higher-order session processes (2019)
  3. Laneve, Cosimo; Lienhardt, Michael; Pun, Ka I.; Román-Díez, Guillermo: Time analysis of actor programs (2019)
  4. Kouzapas, Dimitrios; Pérez, Jorge A.; Yoshida, Nobuko: On the relative expressiveness of higher-order session processes (2016)
  5. Patrignani, Marco; Clarke, Dave: Fully abstract trace semantics for protected module architectures (2015)
  6. Schmidt-Schauß, Manfred; Sabel, David; Niehren, Joachim; Schwinghammer, Jan: Observational program calculi and the correctness of translations (2015)
  7. Zunino, Roberto; Nikolić, Đurica; Priami, Corrado; Kahramanoğulları, Ozan; Schiavinotto, Tommaso: (\ell): an imperative DSL to stochastically simulate biological systems (2015) ioport
  8. Honda, Kohei; Yoshida, Nobuko; Berger, Martin: An observationally complete program logic for imperative higher-order functions (2014)
  9. Appel, Andrew W.; Dockins, Robert; Leroy, Xavier: A list-machine benchmark for mechanized metatheory (2012)
  10. Myreen, Magnus O.; Gordon, Michael J. C.: Function extraction (2012)
  11. Bolduc, Claude; Ktari, Béchir: Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra (2011)
  12. Langar, Mahjoub; Mejri, Mohamed; Adi, Kamel: Formal enforcement of security policies on concurrent systems (2011)
  13. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  14. Wang, Shengyuan; Dong, Yuan: A verifiable low-level concurrent programming model based on colored Petri nets (2011)
  15. Wang, Wei: Certifying assembly programs with trails (2011)
  16. Rudolph, Johannes; Thiemann, Peter: \textscMnemonics: type-safe bytecode generation at run time (2010)
  17. Feng, Xinyu; Shao, Zhong; Guo, Yu; Dong, Yuan: Certifying low-level programs with hardware interrupts and preemptive threads (2009)
  18. Leroy, Xavier: A formally verified compiler back-end (2009)
  19. Albert, Elvira; Puebla, Germán; Hermenegildo, Manuel: Abstraction-carrying code: a model for mobile code safety (2008)
  20. Iwama, Futoshi; Kobayashi, Naoki: A new type system for JVM lock primitives (2008)

1 2 3 next