Map

Iterations

Doshi

• Phase: Running
• Language: Takibi 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: Closed
• 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”