Reduction Free Normalisation for a proof irrelevant type of propositions

Thierry Coquand. Reduction Free Normalisation for a proof irrelevant type of propositions. Logical Methods in Computer Science, 19(3), 2023. [doi]

Abstract

Abstract is missing.