The Proof Assistant as an Integrated Development Environment
- Nick Benton
Invited talk. Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS 2013) |
Published by Springer
We discuss the potential of doing program development, code generation, application-specific modelling, and verification entirely within a proof assistant.