Continuity of Gödel's system T definable functionals via effectful forcing

DOI10.1016/J.ENTCS.2013.09.010zbMATH Open1334.68126OpenAlexW2152195288WikidataQ113317966 ScholiaQ113317966MaRDI QIDQ265800

Martín Hötzel Escardó

Publication date: 12 April 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2013.09.010

zbMATH Keywords

continuityBaire spacesemanticsuniform continuitydialogueCantor spaceAgdaGödel's system Tintensional Martin-Löf theorylogical relation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming with algebraic effects and handlers
• Algebraic operations and generic effects
• When is a functional program not a functional program?
• A Note on Forcing and Type Theory
• Recursive Functionals and Quantifiers of Finite Types I
• Representations of Stream Processors Using Nested Fixed Points
• Ordinal analysis of terms of finite type
• Dependent Types at Work
• A Computational Interpretation of Forcing in Type Theory

Related Items (7)

Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ Characterising Brouwer's continuity by bar recursion on moduli of continuity ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity ⋮ Unnamed Item ⋮ Higher order functions and Brouwer’s thesis

Uses Software

• Eff

This page was built for publication: Continuity of Gödel's system T definable functionals via effectful forcing