Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
The Curry-Howard correspondence identifies functions with theorems, providing a promising link between well explored areas of math and software engineering. However dependently typed systems can be cumbersome when used as a programming language. We believe that one solution is to extend dependently typed languages with a proof search interface that can be activated at run-time, delaying constraint solving as late as possible. We describe insights gained from ongoing work implementing a prototype Call-By-Value dependently typed language with these run-time solving capabilities that should help other teams trying to implement something similar.
Sun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
15:30 - 17:00
|Predictable Macros for Hindley-Milner (Extended Abstract)|
|Strongly Bounded Termination with Applications to Security and Hardware Synthesis|
|Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)|