Judgmental subtyping systems with intersection types and modal types


Introduction

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 (function, intersection, necessity modality, possibility modality), 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 [1] 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.


Coq developments

The proof scripts along with required libraries can be downloaded as a gzip'd tarball [coq.tar.gz] or a zip file [coq.zip]. Extracting the files creates a subdirectory coq, and you can compile the proof scripts by typing make or make coq. You can generate all the documents using coqdoc by typing make doc. We have tested all the proof scripts on Coq 8.3pl2 (October 2011) and 8.4beta (December 2011). (However the proof scripts do not compile on 8.2pl3.)

Subtyping system Proof script Documentation with proofs Documentation without proofs
Base subtyping systems Base.v HTML HTML
Subtyping systems based modal logic S4 SS4.v HTML HTML
Subtyping systems based on modal logic S5 SS5.v HTML HTML


References

  1. Frank Pfenning and Rowan Davies. A Judgmental Reconstruction of Modal Logic. Mathematical Structures in Computer Science 11(4):511-540, 2011.


Email us at .

Programming Language Laboratory
Department of Computer Science and Engineering
Pohang University of Science and Technology (POSTECH)
Republic of Korea