10.2168/LMCS-12(3:2)2016
Eades III, Harley
Harley
Eades III
Stump, Aaron
Aaron
Stump
McCleeary, Ryan
Ryan
McCleeary
Dualized Simple Type Theory
episciences.org
2017
Computer Science - Logic in Computer Science
F.3.2
contact@episciences.org
episciences.org
2014-11-19T00:00:00+01:00
2016-09-27T12:35:52+02:00
2017-04-27
eng
Journal article
https://lmcs.episciences.org/2005
arXiv:1605.01083
1860-5974
PDF
1
Logical Methods in Computer Science ; Volume 12, Issue 3 ; 1860-5974
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.
Comment: 47 pages, 10 figures