Graded Modal Dependent Type Theory with Universe and Erasure - Formalized
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 30-minute conference talk from ICFP 2023 that presents a graded modal type theory with a universe and erasure, fully formalized in Agda. Delve into the theory's features, including Π-types, weak and strong Σ-types, natural numbers, an empty type, and a universe, as well as extensions with a unit type and graded Σ-types. Examine how the theory is parameterized by a modality, allowing for different grade systems to track variable usage in terms and types. Focus on the erasure modality for marking function arguments as erasable. Learn about the formalization's meta-theoretic properties, including subject reduction, consistency, normalization, and decidability of definitional equality. Investigate the extraction function that translates terms to an untyped λ-calculus and removes erasable content. Understand the conditions under which extraction is proven sound for a certain class of modalities. Access supplementary materials, including the article and archive, to further explore this advanced topic in dependent type theory and formal verification.
Syllabus
[ICFP'23] A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
Taught by
ACM SIGPLAN
Related Courses
Peter Dybjer - Intuitionistic Type TheoryHausdorff Center for Mathematics via YouTube The Intellectual Ascent to Agda
CppNow via YouTube Programming Languages in Agda - Propositions as Types
GOTO Conferences via YouTube Vehicle - A Specification Language for Neural Network Properties
ACM SIGPLAN via YouTube Timely Computation - A Formal Approach to Digital Circuit Design
ACM SIGPLAN via YouTube