Harley Eades III ; Aaron Stump ; Ryan McCleeary - Dualized Simple Type Theory

lmcs:2005 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 3 - https://doi.org/10.2168/LMCS-12(3:2)2016
Dualized Simple Type TheoryArticle

Authors: 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.


    Volume: Volume 12, Issue 3
    Published on: April 27, 2017
    Accepted on: August 15, 2016
    Submitted on: November 19, 2014
    Keywords: Computer Science - Logic in Computer Science,F.3.2

    Consultation statistics

    This page has been seen 1872 times.
    This article's PDF has been downloaded 576 times.