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

(6)

• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• Separating Markov's principles
• Computation first: rebuilding constructivism with effects (invited talk)
• A zoo of continuity properties in constructive type theory
• Internal effectful forcing in system T
• An innermost DP framework for constrained higher-order rewriting

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)