Systems and
Formalisms Lab

Articles by Quentin Corradi

  1. A certificate-based conversion checking algorithm for Rocq?

    Rocq uses an algorithm with heuristics to test convertibility of terms. While these heuristics work fine for many problems, some simple convertibility problems can take forever. Usually, these problems are between convertible terms obtained using a reduction tactic. We propose to add a convertibility checker that takes a convertibility certificate to speed up convertibility checks in such cases.

    A proof that passes can take forever at Qed time because of convertibility tests. Our proposed solution to this issue is to replay a computation trace instead of relying on heuristics.

    Fixpoint boom n :=
  match n with
  | 0 => 0
  | S k => (if Nat.eqb n 24 then 1 else 0) + boom k + boom k
  end.


    1 + (boom 50 + 1) = 1 + boom 50 + 1
    

    1 + (boom 50 + 1) = 1 + boom 50 + 1
    
      
    Finished transaction in 0. secs (0.u,0.s) (successful)
    S (boom 50 + 1) = S (boom 50 + 1)
    
      
    Finished transaction in 0. secs (0.u,0.s) (successful)
    

    The command has indeed failed with message:
Timeout!
    
    Abort.