65 citations · 93 across the 10 of their papers we have counts for
Showing 2007Show all
2 papers · 1 filter
cs.LO2007★ 1 cited
HORPO with Computability Closure : A Reconstruction
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for…
cs.LO2007★ 1 cited
Building Decision Procedures in the Calculus of Inductive Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when r…