INTUITIONISTIC TREE SEQUENT CALCULUS AND INTUITIONISTIC LAMBDA-RHO-CALCULUS (Proof Theory, Computation Theory and Related Topics)
直祐 松田 · Kyoto University Research Information Repository (Kyoto University) · 2015
In [8], the author gave a subsystem of the $\lambda\rho$ -calculus [7], and showed that the subsystem corresponds to intuitionistic logic.The proof was given with the intuitionistic tree sequent calculus [4,6].In this paper, we give a observation to these two proof systems, and show there is a close connection between them.