Search

• < Previous
• 1
• Next >

Sharing proofs with predicative theories through universe-polymorphic elaboration

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 challenges in this domain is to translate proofs written in proof assistants based on impredicative logics to proof&nbsp;[&hellip;]