レジスタマシンをターゲットとする「正しいコンパイラ」を依存型言語Agdaによって実装する．具体的には，ソース言語，マシン語コード，ソース言語からマシン語コードへのコンパイラ，マシン語コードを実行するレジスタマシンをそれぞれAgdaで記述する．Agdaを用いることによりマシン語コードの型の中に実行前後のマシンの状態を表現でき，おかしな動作記述になっていないことが型検査により保証される．スタックマシンをターゲットとするコンパイラのAgdaによる実装については先行研究があり，本研究では，それを基にレジスタマシンに特有な部分の適切な型表現を考案した上でレジスタマシンを定義している．