TALK : Typed Assembly Language for Kernel

TALK is a typed assembly language which is flexible and expressive enough to implement important OS facilities, such as memory management (e.g., malloc/free) and multi-thread management.

TALK for IA-32
(last updated 2005-10-27 : version 0.0.0.2. ChangeLog. Old versions
TALK is licensed under the GNU General Public License.

Notes

The "assembler" just emits binary executables annotated with type information. It does not perform type-checks.
The type-check is performed by the "verifier".

Documents

We are sorry but we have not prepared any user manual of TALK. (Please see the programs in TOS at this time)

Further Readings

  1. Toshiyuki Maeda and Akinori Yonezawa.
    Writing practical memory management code with a strictly typed assembly language.
    In 3rd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE 2006). Informal proceedings.
  2. Toshiyuki Maeda.
    Ph.D. Thesis (2006)
  3. Toshiyuki Maeda and Akinori Yonezawa.
    Typed Assembly Language for SMP/Multi-core CPUs (Japanese). (2008)
    In 6th Dependable System Workshop (DSW 2008).

Contact Information

Toshiyuki Maeda
tosh @ is.s.u-tokyo.ac.jp
../