Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-one and Truth-table Reducibility in Coq
(pdf)
Yannick Forster, Felix Jahn
Computer Science Logic (CSL'23), Warsaw, Poland
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory
(pdf)
Yannick Forster, Felix Jahn, Gert Smolka
CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs