1 citations · 1 across the 1 of their papers we have counts for
2 papers
cs.LO2021★ 1 cited
General Automation in Coq through Modular Transformations
Valentin Blot, Louise Dubois de Prisque, Chantal Keller +1
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed…
cs.LO2018
An interpretation of system F through bar recursion
Valentin Blot
There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the pro…