Inductive continuity via Brouwer trees

DOI10.4230/LIPICS.MFCS.2023.37MaRDI QIDQ6647666zbMATH OpenFDO

Authors Liron Cohen, Paiva Bruno Da Rocha, Vincent Rahli, Ayberk Tosun

Publication date 3 December 2024

Full work available at URL https://doi.org/10.4230/LIPICS.MFCS.2023.37

zbMATH Keywords

agdaconstructive type theorycontinuitydialogue treesextensional type theoryintuitionistic logicrealizabilitystateful computationstheorem proving

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cited in

(2)

• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• Separating Markov's principles

This page was built for publication: Inductive continuity via Brouwer trees

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6647666)