episciences.org_2005_1635000912
1635000912
episciences.org
raphael.tournoy+crossrefapi@ccsd.cnrs.fr
episciences.org
Logical Methods in Computer Science
1860-5974
04
27
2017
Volume 12, Issue 3
Dualized Simple Type Theory
Harley
Eades III
Aaron
Stump
Ryan
McCleeary
We propose a new bi-intuitionistic type theory called Dualized Type Theory
(DTT). It is a simple type theory with perfect intuitionistic duality, and
corresponds to a single-sided polarized sequent calculus. We prove DTT strongly
normalizing, and prove type preservation. DTT is based on a new propositional
bi-intuitionistic logic called Dualized Intuitionistic Logic (DIL) that builds
on Pinto and Uustalu's logic L. DIL is a simplification of L by removing
several admissible inference rules while maintaining consistency and
completeness. Furthermore, DIL is defined using a dualized syntax by labeling
formulas and logical connectives with polarities thus reducing the number of
inference rules needed to define the logic. We give a direct proof of
consistency, but prove completeness by reduction to L.
04
27
2017
2005
arXiv:1605.01083
10.2168/LMCS-12(3:2)2016
https://lmcs.episciences.org/2005