1 citations · 2 across the 3 of their papers we have counts for
3 papers
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
Computability Closure: Ten Years Later
Frédéric Blanqui
The notion of computability closure has been introduced for proving the termination of higher-order rewriting with first-order matching by Jean-Pierre Jouannaud and Mitsuhiro Okada…
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…