C. Angiuli, Internalizing Representation Independence with Univalence, February 25 at 11:30 Eastern

[Chris Kapulkin]

The next HoTTEST will be given by Carlo Angiuli on February 25 at
11:30 Eastern. The title and abstract are below.

As always, we will have a one-hour talk followed by a 30-minute discussion.

The Zoom link is

https://zoom.us/j/994874377

Instructions for connecting are available at

http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html

The web page also includes video and slides from past talks.

Best,
Chris

*

Carlo Angiuli
Carnegie Mellon University

Internalizing Representation Independence with Univalence

In programming language theory, the principle of representation
independence states that programs indexed by structured types are
invariant under a wide range of structure-preserving correspondences.
The Structure Identity Principle (SIP) states that constructions in
HoTT respect structured isomorphisms, but many instances of
representation independence involve non-isomorphic types.

In this talk, I will motivate representation independence, explain its
connection to proof reuse and transfer, and recall the basics of
cubical type theory and the SIP. Then, I will describe our recent work
on a relational variant of the SIP that uses HIT quotients to improve
representation independence scenarios into structured isomorphisms and
thence equalities of structured types. Our results are formalized in
Cubical Agda.

Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at
https://dl.acm.org/doi/10.1145/3434293.