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
StatePublished - Jan 1 2016

Fingerprint

Type Theory
Intuitionistic Logic
Labeling
Inference Rules
Completeness
Admissible Rule
Logic
Sequent Calculus
Polarity
Preservation
Simplification
Duality

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

Dualized simple type theory. / Eades, Harley; Stump, Aaron; McCleeary, Ryan.

In: Logical Methods in Computer Science, Vol. 12, No. 3, 01.01.2016.

Research output: Contribution to journalArticle

Eades, Harley ; Stump, Aaron ; McCleeary, Ryan. / Dualized simple type theory. In: Logical Methods in Computer Science. 2016 ; Vol. 12, No. 3.
@article{cbc9c783f5e64da7bb3be0b2b57abf3f,
title = "Dualized simple type theory",
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.",
keywords = "Bi-intuitionistic logic, Coinduction, Completeness, Consistency, Dual, Exclusion, Kripke model, Sequent calculus, Simple type theory, Subtraction",
author = "Harley Eades and Aaron Stump and Ryan McCleeary",
year = "2016",
month = "1",
day = "1",
doi = "10.2168/LMCS-12(3:2)2016",
language = "English (US)",
volume = "12",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "3",

}

TY - JOUR

T1 - Dualized simple type theory

AU - Eades, Harley

AU - Stump, Aaron

AU - McCleeary, Ryan

PY - 2016/1/1

Y1 - 2016/1/1

N2 - 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.

AB - 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.

KW - Bi-intuitionistic logic

KW - Coinduction

KW - Completeness

KW - Consistency

KW - Dual

KW - Exclusion

KW - Kripke model

KW - Sequent calculus

KW - Simple type theory

KW - Subtraction

UR - http://www.scopus.com/inward/record.url?scp=85003548398&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85003548398&partnerID=8YFLogxK

U2 - 10.2168/LMCS-12(3:2)2016

DO - 10.2168/LMCS-12(3:2)2016

M3 - Article

AN - SCOPUS:85003548398

VL - 12

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 3

ER -