Map

Iterations

Doshi

Phase: Planning
Language: New language
Design: Design new domain-specific language for device driver, RTOS, and bare metal code
Product: None
Demo: None
Paper: None

Chiers

Phase: Closed
Language: C verified by VeriFast
Design: Apply annotation to NetBSD kernel
Product: None
Demo: Verify sample application on ChibiOS/RT using VeriFast, Trying FreeRTOS using VeriFast
Paper: None

Bohai

Phase: Re-training
Language: ATS
Design: Snatch NetBSD kernel using ATS
Product: c2ats
Demo: ATS programing on Arduino, ATS programing on ChibiOS/RT, ATS programing on mbed
Paper: “ATS言語を使って不変条件をAPIに強制する”, “Arduino programing of ML-style in ATS”

Arafura

Phase: Closed
Language: Haskell (Ajhc compiler)
Design: Snatch NetBSD kernel using Ajhc Haskell compiler
Product: Ajhc Haskell compiler
Demo: Application on Android NDK, Application on Cortex-M3, Application on ChibiOS/RT, NetBSD kernel driver
Paper: “強い型によるOSの開発手法の提案”, “Systems Demonstration: Writing NetBSD Sound Drivers in Haskell”

Gantt chart

Metasepi Bohai/Chiers Plan (old) / html, planner
Metasepi Bohai Plan (old) / html, planner
Metasepi Arafura Plan (old) / html, planner

Five-Year Plans