# 研究目的
- OSやアプリケーションの信頼性を高めることは重要な課題である。

- 研究室でCbCという言語を開発している。その信頼性を証明したい。

    - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。

- 課題として、CbC はC言語とアセンブラの中間に位置しているため、人がコーディングするのは困難となっている。

- GearsOS での実装と Gears Agda による実装の違いを極力無くすためにも Gears Agda からGearsOS の生成をしたい。

# 今週やったこと

- Agdaのreflectionについて調べた