ICFP 2020 (series) / TyDe 2020 (series) / TyDe 2020 /
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 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
15:30 - 16:00 Talk | Predictable Macros for Hindley-Milner (Extended Abstract) TyDe | ||
16:00 - 16:30 Talk | Strongly Bounded Termination with Applications to Security and Hardware Synthesis TyDe Thomas ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.S. Naval Research Laboratory | ||
16:30 - 17:00 Talk | Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract) TyDe |