Compositional Pre-processing for Automated Reasoning in Dependent Type Theory

Valentin Blot, Denis Cousineau 0003, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial. Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. 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 63-77, ACM, 2023. [doi]

Abstract

Abstract is missing.