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

YouTube

Internal Parametricity Without an Interval

ACM SIGPLAN via YouTube

Overview

Explore a groundbreaking approach to internal parametricity in type theory through this 19-minute conference talk from POPL 2024. Delve into a novel extension of Martin-Löf type theory that achieves internal parametricity without relying on explicit higher-dimensional cubes or interval sorts. Discover how the presenters, Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman, introduce new type formers, term formers, and equations to create a simpler syntax where geometry emerges implicitly. Learn about the presheaf model over the BCH cube category, the span-based parametricity approach, and the gluing model that ensures external parametricity and canonicity. Gain insights into this theory's potential as a special case of modal type theory and its implications for demonstrating computational properties in higher observational type theory.

Syllabus

[POPL'24] Internal parametricity, without an interval

Taught by

ACM SIGPLAN

Reviews

Start your review of Internal Parametricity Without an Interval

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.