\(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity

DOI10.46298/lmcs-20(2:18)2024MaRDI QIDQ6597949

Liron Cohen, Vincent Rahli

Publication date: 4 September 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

continuitytheorem provingrealizabilityconstructive type theoryAgdaintuitionismextensional type theorystateful computations

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

This page was built for publication: \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity