Internal and Observational Parametricity for Cubical Agda

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.

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