Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence | Vidéo | Carmin.tv

00:00:00 / 00:00:00

Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

Apparaît dans la collection : MALINCA Kick-off meeting

In this talk I present Trocq, a proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq interactive theorem prover, in the Rocq-Elpi meta-language.

This is a joint work with Enzo Crance and Assia Mahboubi.

Informations sur la vidéo

Date de captation 03/10/2025
Date de publication 15/12/2025
Institut IHP
Licence CC BY NC ND
Langue Anglais
Audience Chercheurs, Doctorants
Réalisateur(s) Mandarine Audiovisuel
Format MP4
Lieu IHP - Hermite Amphitheater

Domaine(s)

Logique en informatique

Bibliographie

Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence. ACM Transactions on Programming Languages and Systems (TOPLAS), 2025, pp.1-40. ⟨10.1145/3737283⟩. ⟨hal-05192017⟩

Codes MSC

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow

Copyright Carmin.tv 2025

Donner son avis