2 papers
cs.LO2023
Sharing proofs with predicative theories through universe-polymorphic elaboration
Thiago Felicissimo, Frédéric Blanqui
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…
cs.LO2022
Translating proofs from an impredicative type system to a predicative one
Thiago Felicissimo, Frédéric Blanqui, Ashish Kumar Barnawal
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…