Dependently-Typed Programming with Logical Equality Reflection

Explore a groundbreaking approach to dependently-typed programming in this 31-minute video presentation from ICFP 2023. Delve into System DE, an explicitly-typed, moded core calculus that addresses the trade-off between performance and safety in dependently-typed functional programming languages. Learn how this innovative system supports termination tracking and equality reflection, allowing programmers to write inductive proofs about potentially diverging programs in a logical sublanguage. Discover the key feature of System DE's use of modes for both termination and relevance tracking, and understand its potential as a foundation for general-purpose dependently-typed languages, including its suitability for implementation in the Glasgow Haskell Compiler. Gain insights from University of Pennsylvania researchers Yiyun Liu and Stephanie Weirich as they present their work on enhancing type soundness while maintaining compiler efficiency.