Compiling with dependent types
Dependently typed languages have proven useful for developing large-scale fully verified software, but we do not have any guarantees after compiling that verified software. A verified program written in a dependently typed language, such as Coq, can be type checked to ensure that the program meets i...
| Published: |
|
|---|---|
| Online Access: | http://hdl.handle.net/2047/D20316239 |