Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 20-minute conference talk from POPL 2025 that presents a novel approach to understanding gradually typed programming languages through denotational semantics. Learn how researchers Eric Giovannini, Tingting Ding, and Max S. New from the University of Michigan tackle the challenges of modeling languages that mix static and dynamic typing styles. The presentation introduces a denotational semantics framework using guarded domain theory, which combines the generality of step-indexed logical relations with the modularity of denotational semantics. Discover how this approach enables proving important properties like beta-eta equality and graduality for a simple gradually typed lambda calculus. The research has been partially mechanized in Guarded Cubical Agda, demonstrating its practical application. This talk is particularly valuable for those interested in programming language theory, type systems, and formal verification methods.
