• Popescu A and Traytel D. (2023). Admissible Types-to-PERs Relativization in Higher-Order Logic. Proceedings of the ACM on Programming Languages. 7:POPL. (1214-1245). Online publication date: 9-Jan-2023.

    https://doi.org/10.1145/3571235

  • Bordg A and Doña Mateo A. Encoding Dependently-Typed Constructions into Simple Type Theory. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. (78-89).

    https://doi.org/10.1145/3573105.3575679

  • Milehins M. An extension of the framework types-to-sets for Isabelle/HOL. Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. (180-196).

    https://doi.org/10.1145/3497775.3503674

  • Guttmann W. (2020). Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL. Automated Reasoning. 10.1007/978-3-030-51054-1_14. (236-253).

    http://link.springer.com/10.1007/978-3-030-51054-1_14

  • The mathlib Community . The lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. (367-381).

    https://doi.org/10.1145/3372885.3373824