research
∙
08/29/2023
Sharing proofs with predicative theories through universe polymorphic elaboration
As the development of formal proofs is a time-consuming task, it is impo...
share
research
∙
07/17/2023
A framework for erased syntax and bidirectional typing
We introduce CompLF, a logical framework allowing for the definition of ...
research
∙
11/10/2022
Translating proofs from an impredicative type system to a predicative one
As the development of formal proofs is a time-consuming task, it is impo...
research
∙
05/05/2022