ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 23:30 - 00:00 at TyDe - Session II Chair(s): Dominic Orchard

Dependent type systems are powerful tools to eliminate bugs from programs. Unlike other systems of formal methods, dependent type systems can re-use the methodology and syntax that functional programmers are already familiar with for the construction of formal proofs. However, implementations of these languages still have substantial usability issues arising from the conservative equality commonly used in intentional type theories, which can manifest as confusing error messages. In this paper we show how to take a full-spectrum dependently typed language and optimistically delay some equality checking until runtime. The advantage of our method is clear runtime error messages supported by blame that pinpoints the exact source of failure.

paper (paper.pdf)502KiB

Sun 22 Aug

Displayed time zone: Seoul change