Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively.

Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi

Browse the full CPP paper archive.