DUALIZED SIMPLE TYPE THEORY

Harley D. Eades; Aaron D. Stump; Ryan McCleeary

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

Back

Journal article

Open access

Peer reviewed

DUALIZED SIMPLE TYPE THEORY

Harley D. Eades, Aaron D. Stump and Ryan McCleeary

Logical methods in computer science, Vol.12(3), 2

01/01/2016

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

Files and links (1)

url

https://doi.org/10.2168/LMCS-12(3:2)2016View

Published (Version of record) Open Access

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.

Computer Science

Logic

Technology

Computer Science, Theory & Methods

Science & Technology

Science & Technology - Other Topics

Details

Title: Subtitle: DUALIZED SIMPLE TYPE THEORY
Creators: Harley D. Eades - Augusta University
Aaron D. Stump - University of Iowa
Ryan McCleeary - University of Iowa
Resource Type: Journal article
Publication Details: Logical methods in computer science, Vol.12(3), 2
DOI: 10.2168/LMCS-12(3:2)2016
ISSN: 1860-5974
eISSN: 1860-5974
Publisher: Logical Methods Computer Science E V
Number of pages: 47
Language: English
Date published: 01/01/2016
Academic Unit: Computer Science
Record Identifier: 9984259421602771

Metrics

14 Record Views

See more details