Dualized simple type theory

Harley Eades, Aaron Stump, Ryan McCleeary

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
JournalLogical Methods in Computer Science
Volume12
Issue number3
DOIs
Publication statusPublished - Jan 1 2016

    Fingerprint

Keywords

  • Bi-intuitionistic logic
  • Coinduction
  • Completeness
  • Consistency
  • Dual
  • Exclusion
  • Kripke model
  • Sequent calculus
  • Simple type theory
  • Subtraction

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this