Intuitionistic ancestral logic.

In this article we define pure intuitionistic Ancestral Logic($iAL$), extending pure intuitionistic First-Order Logic ($iFOL$). This logic is a dependently typed abstract programming languagewith computational functionality beyond $iFOL$ given by its realizer for the transitive closure, TC. We derive this operator from the natural type theoretic definition of TC using intersection. We show that pr...