Idris implementation of a type-correct, stack-safe compiler including exception handling.
Based on the following papers:
- A type-correct, stack-safe, provably correct, expression compiler in Epigram
- Dependently-Typed Compilers Don't Go Wrong
Check our report explaining our development process and conclusions about the project.
Install Idris 1.
$ idris throw.idr
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.3.3
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
*throw> compiledProgram
PUSH (VNat 3)
(STORE "x"
(LOAD "x"
(PUSH (VNat 1)
(ADD (STORE "x"
(LOAD "x"
(PUSH (VNat 2)
(ADD (STORE "y"
HALT))))))))) : Code []
[]
[]
[("y",
NatTy),
("x",
NatTy),
("x",
NatTy)]- Francisco MartÃnez Lasaca
- Morten Skøtt Knudsen
- Jeppe Vinberg