Dualized simple type theory

DOI10.2168/LMCS-12(3:2)2016MaRDI QIDQ2974773zbMATH OpenFDO

Authors Harley III Eades, Aaron Stump, Ryan McCleeary

Publication date 11 April 2017

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.01083

zbMATH Keywords

consistencydualcompletenesscoinductionsequent calculussimple type theorybi-intuitionistic logicKripke modelexclusionsubtraction

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Type theory (03B38)

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.

Recommendations

• A term assignment for polarized bi-intuitionistic logic and its strong normalization
• scientific article; zbMATH DE number 1612555
• A Cut-Free Sequent Calculus for Bi-intuitionistic Logic
• On the unity of duality
• Natural deduction for bi-intuitionistic logic

Cites work

• scientific article; zbMATH DE number 3689368 (Why is no real title available?)
• scientific article; zbMATH DE number 1231584 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 742720 (Why is no real title available?)
• scientific article; zbMATH DE number 1479632 (Why is no real title available?)
• scientific article; zbMATH DE number 2090723 (Why is no real title available?)
• A Formulae-as-Types Interpretation of Subtractive Logic
• A connection-based characterization of bi-intuitionistic validity
• A logic stronger than intuitionism
• A term assignment for polarized bi-intuitionistic logic and its strong normalization
• Computer Science Logic
• Copatterns, programming infinite structures by observations
• Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
• Dual Calculus with Inductive and Coinductive Types
• Ott: Effective tool support for the working semanticist
• Pragmatic and dialogic interpretations of bi-intuitionism. I
• Process types as a descriptive tool for interaction. Control and the pi-calculus
• Proof analysis in modal logic
• Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents
• Semi-Boolean algebras and their applications to intuitionistic logic with dual operations
• Some Syntactical Observations on Linear Logic
• Subtractive logic
• Term Rewriting and Applications
• The duality of computation
• Typed Lambda Calculi and Applications

Cited in

(3)

• Dual Calculus with Inductive and Coinductive Types
• Simple Types in Type Theory: Deep and Shallow Encodings
• 2-Dimensional Directed Type Theory

Describes a project that uses

Uses Software

• Ott

This page was built for publication: Dualized simple type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974773)