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
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
Mark LemayBoston University, Cheng ZhangBoston University, William BlairBoston University