Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 16:30 - 17:00 at TyDe - Session 3

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

15:30 - 17:00: Session 3TyDe at TyDe
15:30 - 16:00
Predictable Macros for Hindley-Milner (Extended Abstract)
16:00 - 16:30
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.S. Naval Research Laboratory
16:30 - 17:00
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
Mark LemayBoston University, Cheng ZhangBoston University, William BlairBoston University