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

Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi. Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. pages 102-120, ACM, 2023. [doi]

Abstract

Abstract is missing.