Compiling higher-order specifications to SMT solvers
I just gave a talk at Certified Programs and Proofs on our paper Compiling higher-order specifications to SMT solvers.
Slides:
It is a description of the type based analysis approach that we use in the Vehicle specification language to discover when the queries that a user writes are actually translatable to an SMT solver. Based on this type based analysis we either give the user a nice error message, or we use a Normalisation by Evaluation (NbE) procedure to normalise the query to one suitable for the solver. The NbE procedure is itself non-trivial to support lifting of uninterpreted functions and if-then-elses. The NbE procedure has been formalised in Agda.
Unfortunately the talk wasn't under the best of circumstances. I am in Boston for the conference, but tested positive for COVID yesterday morning. I had to give the talk from my hotel room 10 floors above the conference, which I think is possibly the worst way to give a talk.