Mechanically Verified Proofs from "Empowering Union and Intersection Types with Integrated Subtyping"

Preface

This is not the artifact that was evaluated during the OOPSLA 2018 Artifact Evaluation process, rather it is an improvement on that artifact. For archival purposes, the outdated artifact that was evaluated is provided in outdated_artifact.zip. However, the outdated artifact does not directly support the claims stated in the paper, and the section of the paper that discussed what claims it did support has been removed, so we strongly discourage referencing the outdated artifact. The artifact presented here, although it was not evaluated, has been developed to the same or higher quality than the one that was, and was made to directly support the claims in the paper.

Introduction 

This document gives an overview of the Coq formalization we have created for our paper. It formalizes every requirement and claim in Sections 3 - 5. It is meant to be read along with the paper and largely tries to follow the flow of the paper exactly, with the exception that for engineering reasons, the requirements of each section are all stated together, followed by the Lemmas and Theorems of that section.
In case you are not familiar with Coq's module system: we implemented this formalization as a library for people to use. A "Module Type" specifies a signature that a user needs to implement; "Parameter"s within that module type are the specific things a user needs to provide/proof. Once a user instantiated a module type in a module of their own, they can use that to instantiate our "Module"s, which provide the extended systems/proofs based on the user's input.
This file contains only the signatures of the various components of our proof, but for each file (.v), there is a link at the beginning of the section corresponding to that file that leads to the coqdoc for the full file including the actual proof code. The .v-files themselves are also included and can be used to verify the proofs in Coq. The files should be compiled in the order in which they appear in this file.
All of this was generated using coqdoc, whose approach to links in the face of modules is not the most helpful one. However, other syntax highlighting features depend on the same information as link generation, so the code should still be a lot more readable than without links. We made sure that links in standard HTML rendering (blue underlined) lead to where they should, and most of the links should get you at least closer to where the definition you wanted to was.
We prove an example of how to instantiate the module types of Sections 3 and 4 in Example.v.

Outline

The following outline of the proofs shows the items that correspond to something in the paper:

Paper Concept Index

The following table gives an outline of the parts of our paper and where to find their corresponding counterpart in this formalization:
Concept from PaperCorresponding Definitions/Lemmas/TheoremsComment
LiteralsLit in Section3_Requirements.vAlso an implicit parameter in many global definitions
TypesNotation T := UIType Lit defined almost everywhereUIType is defined in Section3_Requirements.v
Declarative Literal Subtyping RulesDRule and DPremise in Section3_Requirements.v
Declarative Subtypingdsub in Section3_Requirements.vBased on dsuba and dsubf in Section3_Requirements.v
Reductive Literal Subtyping RulesRRule and RPremise in Section3_Requirements.v
Reductive Subtypingrsub in Section3_Requirements.vBased on uisub, lsub, and rsubf in Section3_Requirements.v
Requirement 1: Syntax-DirectednessSyntaxDirectedness_Rules and SyntaxDirectedness_Premises in Section3_Requirements.v
Requirement 2: Well-Foundednessm, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit in Section3_Requirements.v
Requirement 3: Literal ReflexivityLiteralReflexivity in Section3_Requirements.v
Declarative Subtyping with Assumptionsdsuba in Section3_Requirements.v
Reductive Subtyping with Assumptionsrsubam in Section3_Requirements.vAlso includes Monotonicity, which makes the proof stronger than in the paper (see explanation at definition)
Requirement 4: R-to-D Literal ConversionRRuleToDProof in Section3_Requirements.v
Requirement 5: D-to-R Literal ConversionDRuleToRProof in Section3_Requirements.v
Requirement 6: Literal TransitivityLiteralTransitivity in Section3_Requirements.v
Decidability of Declarative Subtyping TheoremDecidabilityOfDeclarativeSubtyping in Section3_Proofs.v
Extension Axiomsextension in Section4_Requirements.v
Extended Subtypingesub in Section4_Requirements.vBased on dsubda and extension in Section4_Requirements.v
Integrator (DNFc)Integrate in Section4_Requirements.v
Intersector (⊓)intersect in Section4_Requirements.v
Requirement 7: Intersector CompletenessIntersectorCompleteness in Section4_Requirements.v
Requirement 8: Intersector SoundnessIntersectorSoundness in Section4_Requirements.v
Lemma 1: Integrated SoundnessIntegratedSoundness in Section4_Proofs.v
Requirement 9: Measure PreservationMeasurePreservation in Section4_Requirements.v
Lemma 2: Integrated DecidabilityIntegratedDecidability in Section4_Proofs.v
Requirement 10: Literal DerelictionLiteralDereliction in Section4_Requirements.v
Lemma 3: DerelictionDereliction in Section4_Proofs.v
Intersected Predicate (φ)intersected in Section4_Requirements.v
Integrated Predicate (dnfφ/dnfφ)Integrated and Integrated_int in Section4_Requirements.v
Requirement 11: Intersector IntegratedIntersectorIntegrated in Section4_Requirements.v
Lemma 4: Integrator IntegratedIntegratorIntegrated in Section4_Proofs.v
Requirement 12: Literal PromotionLiteralPromotion in Section4_Requirements.v
Lemma 5: PromotionPromotion in Section4_Proofs.v
Lemma 6: Integrated MonotonicityIntegratedMonotonicity in Section4_Proofs.vActually mostly proved together in integrated_assumptions' in Section4_Proofs.v
Lemma 7: Integrated AssumptionsIntegratedAssumptions in Section4_Proofs.v
Lemma 8: Integrated PromotionIntegratedPromotion in Section4_Proofs.v
Lemma 9: Integrated ReflexivityIntegratedReflexivity in Section4_Proofs.v
Lemma 10: D-to-I Literal ConversionDeclarativeToIntegratedLiteralConversion in Section4_Proofs.v
Lemma 11: Integrated TransitivityIntegratedTransitivity in Section4_Proofs.v
Lemma 12: Integrated CompletenessIntegratedCompleteness in Section4_Proofs.v
Decidability of Extended Subtyping TheoremDecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping in Section4_Proofs.v
Requirement 13: Intersected PreservationIntersectedPreservation in Section5.v
Intersector Composability TheoremModule Composition in Section5.vDefines its intersect and extension as described in the paper and satisfies the Intersector module type and hence all the Lemmas and Theorems above.

This page has been generated by coqdoc