Internal Effectful Forcing in System T

Martin H. Escardo, Bruno da Rocha Paiva, Vincent Rahli +1

The effectful forcing technique allows one to show that the denotation of a closed System T term of type $({\hat{I}}^1\to {\hat{I}}^1)\to {\hat{I}}^1$ in the set-theoretical model is a continuous function $…