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.Outline
The following outline of the proofs shows the items that correspond to something in the paper:- Section 3: Formalizing Traditional Union and Intersection Subtyping
- Literals (Lit; in many cases an (implicit) parameter)
- Types (Notation T := UIType Lit)
- Declarative Subtyping with Assumptions (dsuba)
- Reductive Subtyping with Assumptions (rsubam; see explanation at definition)
- Declarative Literal Subtyping Rules (DRule and DPremise)
- Declarative Subtyping (dsub based on dsuba and dsubf)
- Reductive Literal Subtyping Rules (RRule and RPremise)
- Reductive Subtyping (rsub based on uisub, lsub, and rsubf)
- Requirements
- Requirement 1: Syntax-Directedness (SyntaxDirectedness_Rules and SyntaxDirectedness_Premises)
- Requirement 2: Well-Foundedness (m, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit)
- Requirement 3: Literal Reflexivity (LiteralReflexivity)
- Requirement 4: R-to-D Literal Conversion (RRuleToDProof)
- Requirement 5: D-to-R Literal Conversion (DRuleToRProof)
- Requirement 6: Literal Transitivity (LiteralTransitivity)
- Decidability of Declarative Subtyping Theorem (DecidabilityOfDeclarativeSubtyping)
- Section 4: Empowering Unions and Intersections
- Integrator DNFc (Integrate)
- Integrated Predicate dnfφ/dnfφ∩ (Integrated and Integrated_int)
- Extension Axioms (extension)
- Extended Subtyping (esub)
- Intersector (⊓) (intersect)
- Intersected Predicate (φ) (intersected)
- Requirements
- Requirement 7: Intersector Completeness (IntersectorCompleteness)
- Requirement 8: Intersector Soundness (IntersectorSoundness)
- Requirement 9: Measure Preservation (MeasurePreservation)
- Requirement 10: Literal Dereliction (LiteralDereliction)
- Requirement 11: Intersector Integrated (IntersectorIntegrated)
- Requirement 12: Literal Promotion (LiteralPromotion)
- Proofs
- Lemma 1: Integrated Soundness (IntegratedSoundness)
- Lemma 2: Integrated Decidability (IntegratedDecidability)
- Lemma 3: Dereliction (Dereliction)
- Lemma 4: Integrator Integrated (IntegratorIntegrated)
- Lemma 5: Promotion (Promotion)
- Lemma 6: Integrated Monotonicity (IntegratedMonotonicity)
- Lemma 7: Integrated Assumptions (IntegratedAssumptions)
- Lemma 8: Integrated Promotion (IntegratedPromotion)
- Lemma 9: Integrated Reflexivity (IntegratedReflexivity)
- Lemma 10: D-to-I Literal Conversion (DeclarativeToIntegratedLiteralConversion)
- Lemma 11: Integrated Transitivity (IntegratedTransitivity)
- Lemma 12: Integrated Completeness (IntegratedCompleteness)
- Decidability of Extended Subtyping Theorem (DecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping)
- Section 5: Composability
- Requirement 13: Intersected Preservation (IntersectedPreservation)
- Intersector Composability Theorem (Module Composition)
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 Paper | Corresponding Definitions/Lemmas/Theorems | Comment |
---|---|---|
Literals | Lit in Section3_Requirements.v | Also an implicit parameter in many global definitions |
Types | Notation T := UIType Lit defined almost everywhere | UIType is defined in Section3_Requirements.v |
Declarative Literal Subtyping Rules | DRule and DPremise in Section3_Requirements.v | |
Declarative Subtyping | dsub in Section3_Requirements.v | Based on dsuba and dsubf in Section3_Requirements.v |
Reductive Literal Subtyping Rules | RRule and RPremise in Section3_Requirements.v | |
Reductive Subtyping | rsub in Section3_Requirements.v | Based on uisub, lsub, and rsubf in Section3_Requirements.v |
Requirement 1: Syntax-Directedness | SyntaxDirectedness_Rules and SyntaxDirectedness_Premises in Section3_Requirements.v | |
Requirement 2: Well-Foundedness | m, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit in Section3_Requirements.v | |
Requirement 3: Literal Reflexivity | LiteralReflexivity in Section3_Requirements.v | |
Declarative Subtyping with Assumptions | dsuba in Section3_Requirements.v | |
Reductive Subtyping with Assumptions | rsubam in Section3_Requirements.v | Also includes Monotonicity, which makes the proof stronger than in the paper (see explanation at definition) |
Requirement 4: R-to-D Literal Conversion | RRuleToDProof in Section3_Requirements.v | |
Requirement 5: D-to-R Literal Conversion | DRuleToRProof in Section3_Requirements.v | |
Requirement 6: Literal Transitivity | LiteralTransitivity in Section3_Requirements.v | |
Decidability of Declarative Subtyping Theorem | DecidabilityOfDeclarativeSubtyping in Section3_Proofs.v | |
Extension Axioms | extension in Section4_Requirements.v | |
Extended Subtyping | esub in Section4_Requirements.v | Based on dsubda and extension in Section4_Requirements.v |
Integrator (DNFc) | Integrate in Section4_Requirements.v | |
Intersector (⊓) | intersect in Section4_Requirements.v | |
Requirement 7: Intersector Completeness | IntersectorCompleteness in Section4_Requirements.v | |
Requirement 8: Intersector Soundness | IntersectorSoundness in Section4_Requirements.v | |
Lemma 1: Integrated Soundness | IntegratedSoundness in Section4_Proofs.v | |
Requirement 9: Measure Preservation | MeasurePreservation in Section4_Requirements.v | |
Lemma 2: Integrated Decidability | IntegratedDecidability in Section4_Proofs.v | |
Requirement 10: Literal Dereliction | LiteralDereliction in Section4_Requirements.v | |
Lemma 3: Dereliction | Dereliction 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 Integrated | IntersectorIntegrated in Section4_Requirements.v | |
Lemma 4: Integrator Integrated | IntegratorIntegrated in Section4_Proofs.v | |
Requirement 12: Literal Promotion | LiteralPromotion in Section4_Requirements.v | |
Lemma 5: Promotion | Promotion in Section4_Proofs.v | |
Lemma 6: Integrated Monotonicity | IntegratedMonotonicity in Section4_Proofs.v | Actually mostly proved together in integrated_assumptions' in Section4_Proofs.v |
Lemma 7: Integrated Assumptions | IntegratedAssumptions in Section4_Proofs.v | |
Lemma 8: Integrated Promotion | IntegratedPromotion in Section4_Proofs.v | |
Lemma 9: Integrated Reflexivity | IntegratedReflexivity in Section4_Proofs.v | |
Lemma 10: D-to-I Literal Conversion | DeclarativeToIntegratedLiteralConversion in Section4_Proofs.v | |
Lemma 11: Integrated Transitivity | IntegratedTransitivity in Section4_Proofs.v | |
Lemma 12: Integrated Completeness | IntegratedCompleteness in Section4_Proofs.v | |
Decidability of Extended Subtyping Theorem | DecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping in Section4_Proofs.v | |
Requirement 13: Intersected Preservation | IntersectedPreservation in Section5.v | |
Intersector Composability Theorem | Module Composition in Section5.v | Defines 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