Open Access System for Information Sharing

Login Library

 

Article
Cited 0 time in webofscience Cited 0 time in scopus
Metadata Downloads

Judgmental Subtyping Systems with Intersection Types and Modal Types SCIE SCOPUS

Title
Judgmental Subtyping Systems with Intersection Types and Modal Types
Authors
Seo, JPark, S
Date Issued
2013-12
Publisher
Springer
Abstract
We study how to extend modal type systems based on intuitionistic modal logic S4 or S5 with a subtyping system based on intersection types. In the presence of four type constructors , and , the traditional approach using a binary subtyping relation does not work well because of lack of orthogonality in subtyping rules and presence of a transitivity rule. We adopt the idea from the judgmental formulation of modal logic (Pfenning and Davies in Math Struct Comput Sci 11(4):511-540, 2001) and use subtyping judgments whose definitions express those notions internalized into type constructors directly at the level of judgments. The resultant judgmental subtyping systems admit cut rules similarly to a sequent calculus for intuitionistic logic and play a key role in designing and verifying the relational subtyping systems based on the binary subtyping relation. We use the proof assistant Coq to prove the admissibility of the cut rules and the equivalence between the two kinds of subtyping systems. The lesson from our study is that by using subtyping judgments instead of the binary subtyping relation, we can overcome the limitation usually associated with the syntactic approach to formulating subtyping systems.
Keywords
LOGIC
URI
https://oasis.postech.ac.kr/handle/2014.oak/14756
DOI
10.1007/S00236-013-0186-2
ISSN
0001-5903
Article Type
Article
Citation
Acta Informatica, vol. 50, no. 7-8, page. 359 - 380, 2013-12
Files in This Item:
There are no files associated with this item.

qr_code

  • mendeley

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Related Researcher

Researcher

박성우PARK, SUNGWOO
Dept of Computer Science & Enginrg
Read more

Views & Downloads

Browse