Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Internal and Observational Parametricity for Cubical Agda

ACM SIGPLAN via YouTube

Overview

Explore a 19-minute conference talk from POPL 2024 that introduces Agda --bridges, the first practical internally parametric proof assistant. Delve into the mechanized proofs of crucial theorems for internal parametricity, including the relativity theorem. Learn about the structure relatedness principle (SRP) and its role in proving internal parametricity. Discover how the presented parametricity theorem enables one-liner proofs of standard internal free theorems. Examine the shallowly embedded type theory developed to compose types satisfying the SRP, and understand its significance as an observational type theory of logical relations. Gain insights into the challenges of proving SRP compared to the structure identity principle (SIP) in HoTT/UF. Access the full article and supplementary materials to further explore this advancement in cubical type theory and parametricity.

Syllabus

[POPL'24] Internal and Observational Parametricity for Cubical Agda

Taught by

ACM SIGPLAN

Reviews

Start your review of Internal and Observational Parametricity for Cubical Agda

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.