4 citations · 8 across the 4 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…
Typed realizability for first-order classical analysis
Valentin Blot
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed λμ-calculus. This allows a direct interpretation of classical pr…