Map
Mind map
Old map
Iterations
Danvers
- Phase: Not yet touch
- Language: Chisel, Verilog
- Design: System call caught by HDL
- 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