| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2013: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Outline of Final Research Achievements |
We have implemented code extraction from proof assistant Coq to programming language Scala. Once a proof is given to a code written in Coq, then the extracted code is guaranteed that it behaves correctly. There are many working systems written in Java, and Scala code is easily integrated with them because it runs on Java VM. Our code itself is originally written in Coq and is extracted from a proof on Coq that it works correctly.
|
