2026-07-22T13:27:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23634 2025-07-07T17:36:47Z ddc:004 open_access

Internal Effectful Forcing in System T Escardó, Martín H. da Rocha Paiva, Bruno Rahli, Vincent Tosun, Ayberk Effectful forcing Continuity System T Constructive Mathematics The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι ⇒ ι) ⇒ ι in the set-theoretical model is a continuous function (ℕ → ℕ) → ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martín H. Escardó and Bruno da Rocha Paiva and Vincent Rahli and Ayberk Tosun 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.19 urn:nbn:de:0030-drops-236344 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.19 eng https://creativecommons.org/licenses/by/4.0/legalcode