TOS : Typed Operating System

TOS is an experimental operating system kernel which is written in our strictly and statically typed assembly language, TALK.

Today, computers (PCs, cell-phones, etc.) are widely used in the world and their network become one of the indispensable social infrastructures. Therefore, the importance of ensuring safety of software is commonly-recognized and many programs come to be written in strongly-typed languages (Java, C#, Objective Caml). This is because the program that is written in a strongly-typed language and passes its type-check is ensured not to raise errors at runtime.

However, there is one kind of programs that are never written in typed-languages: Operating systems. For example, existing OSes (e.g., Linux, FreeBSD, Windows XP, Solaris, etc.) are written in C and assembly languages.

One of the reason that OSes were not written in typed-languages is that it is believed that OS facilities, such as memory management, multi-thread management and device drivers, cannot be written in the typed-languages.

To break the mistaken belief, we have developed a statically and strictly typed assembly language, called TALK, and implemented a prototype OS kernel, called TOS, in TALK.

So far, the functionality of TOS is very poor (no user programs, no file systems ...), but we plan to extend TOS to have the same facilities as existing OS kernels.

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

Contact Information

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