index

Martin Escardo, Bruno da Rocha Paiva, Ayberk Tosun, and Vincent Rahli, June 2023

The main theorem is that for every system T closed term t : (ι → ι) → ι
there is a system T term which Church-encodes a dialogue tree of the
standard interpretation ⟦ t ⟧ of t (defined in the file System T).


{-# OPTIONS --safe --without-K #-}

module EffectfulForcing.Internal.index where

import EffectfulForcing.Internal.SystemT
import EffectfulForcing.Internal.Internal
import EffectfulForcing.Internal.Subst
import EffectfulForcing.Internal.External
import EffectfulForcing.Internal.Correctness
import EffectfulForcing.Internal.FurtherThoughts
import EffectfulForcing.Internal.InternalModCont    -- by Ayberk Tosun
import EffectfulForcing.Internal.InternalModUniCont -- by Ayberk Tosun
import EffectfulForcing.Internal.Degrees            -- by Ayberk Tosun
import EffectfulForcing.Internal.PaperIndex
import EffectfulForcing.Internal.AnotherCorrectnessProof -- by Chuangjie Xu


 1. The file Internal gives Church-encoded dialogue trees of system T
    terms t : (ι → ι) → ι.

 2. The file EffectfulForcing.Internal.External gives a semantics in terms of
    inductive dialogue trees and formulates and proves the correctness of the
    produced dialogue trees.

 3. The file Correctness proves the correctness of (1) using the
    composition of the logical relation defined in (2) with a second
    logical relation defined for that purpose.

 4. The file EffectfulForcing.Internal.FurtherThoughts contains some work in
    progress.

 5. The file `EffectfulForcing.Internal.InternalModCont` contains the proof of
    correctness of the internal modulus of continuity operator.

 6. The file `EffectfulForcing.Internal.InternalModUniCont` contains the proof
    of correctness of the internal modulus of _uniform_ continuity operator.

 7. The file `EffectfulForcing.Internal.AnotherCorrectnessProof` gives another
    proof of the correctness of the Church-encoded dialogue-tree translation,
    using a different logical relation.