4 citations · 6 across the 2 of their papers we have counts for
2 papers
cs.LO2023★ 2 cited
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most…
cs.LO2022★ 4 cited
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance +4
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited…