ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Tue 5 Sep 2023 11:00 - 11:30 at B - Fifth Avenue - Dependent types Chair(s): James Chapman

In dependently-typed functional programming languages that allow general
recursion, programs used as proofs must be evaluated to retain type soundness. As a result,
programmers must make a trade-off between performance and safety. To address
this problem, we propose System DE, an explicitly-typed, moded core calculus
that supports termination tracking and equality reflection. Programmers can
write inductive proofs about potentially diverging programs in a logical
sublanguage and reflect those proofs to the type checker, while knowing that
such proofs will be erased by the compiler before execution. A key
feature of System DE is its use of modes for both termination and relevance
tracking, which not only simplifies the design but also leaves it
open for future extension. System DE is suitable for use in the Glasgow
Haskell Compiler, but could serve as the basis for any general purpose
dependently-typed language.

Tue 5 Sep

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
Dependent typesICFP Papers and Events at B - Fifth Avenue
Chair(s): James Chapman Input Output
Is Sized Typing for Coq Practical?JFP Presentation
ICFP Papers and Events
Jonathan Chan University of Pennsylvania, Yufeng Li University of Waterloo, William J. Bowman University of British Columbia
Link to publication DOI Media Attached
Dependently-Typed Programming with Logical Equality Reflection
ICFP Papers and Events
Yiyun Liu University of Pennsylvania, Stephanie Weirich University of Pennsylvania
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
ICFP Papers and Events
Andreas Abel Gothenburg University, Nils Anders Danielsson Chalmers and Gothenburg University, Oskar Eriksson Chalmers and Gothenburg University