Brendan Zabarauskas on Twitter: "@bentnib Ooh, thanks, will check this one out! 👍" / Twitter

Question for PL/TT Twitter: Does anyone know of any prior art in terms of extracting something like Martin-Löf Type Theory (non-cumulative, with one universe, kind of like in The Little Typer) to something like System Fω with lifted terms and types?

Bob Atkey

@bentnib

Jul 2, 2020

Maybe "A New Extraction for Coq" irif.fr/~letouzey/down ?

Brendan Zabarauskas

@brendanzab

Replying to

@bentnib

Ooh, thanks, will check this one out! 👍

9:46 AM · Jul 2, 2020Twitter Web App

Conversation