Skip to content

Latest commit

 

History

History
86 lines (72 loc) · 11.4 KB

Correspondence.md

File metadata and controls

86 lines (72 loc) · 11.4 KB

Correspondence with the paper

The README.agda is the entry, which gives the overview of our Agda formalisation.

Roughly, the paper presents several small QTASs in Section 3 and two main calculi in Section 3, 4 and 5.

The several systems are formalized in root folder and two calculi have several own projection folder.

We have tried our best to match the notation from Agda code with the paper, so the Agda script is readable to people with some experience in proof assistant. However, we prove the details about each theorem shown in the paper, to help better review this artifact.

Bidirectional typing, let-argument-go-first and the corresponding QTASs

Figure Agda File Location Comments (if any)
Fig. 1 Bidirectional typing of STLC _⊢b_#_⦂_ AllOrNothing.agda Our formorlisation is different from classic bidirecitonal type system (shown in Fig.1), we add a App2 rule and change Lit rule to a inference mode, to better connect to QTASs, which is explained in paper line 420.
Fig. 2 Let arguments go first _~_⊢_⇒_ Application.agda Lit and Var shown in paper are syntactic sugar when application stack is empty, while in Agda we show in expanded version.
Fig. 3. STLC with all-or-nothing counters _⊢d_#_⦂_ AllOrNothing.agda
Fig. 4. STLC with application counters _⊢d_#_⦂_ Application.agda
Fig. 5. All-in-one QTAS _⊢d_#_⦂_ AllInOne.agda we have the same judgment defined in STLC/Decl.agda
Fig. 6 Typing derivation ex-derivation STLC/Decl.agda
Fig. 7 Elaboration rules _⊢1_⦂_⟶_ STLC/Annotatability.agda _⊢2_⦂_⟶_ and _⊢3_⦂_⟶_ are two other versions of elaboration rules
Theorem Agda File Location Comments (if any)
Theorem 3.1 (Soundness) sound, sound-inf, sound-chk AllOrNothing.agda sound is the general form, the theorem shown on the paepr are corollaries.
Theorem 3.2 (Completeness) complete, complete-inf, complete-chk AllOrNothing.agda like above
Theorem 3.3 (Soundness) sound Applicatoin.agda
Theorem 3.4 (Completeness) complete Applicatoin.agda
Theorem 3.5 (Completeness) complete, complete' AllInOne.agda
Theorem 3.6 (Weak Annotatability) complete STLC/Annotatability.agda
Theorem 3.7 (Strong Annotatability) annotatability, annotatability' STLC/Annotatability.agda
Theorem 3.7 (Strong Annotatability) (Other ver.) annotatability2, annotatability2', annotatability3, annotatability3' STLC/Annotatability.agda As claimed in paper line 650: "Rules EApp2 and EApp3 provide two different alternative annotatability strategies/guidelines"

The STLC Calculus

Figure Agda File Location Comments (if any)
Fig. 8. Syntax (part 1) Type, Term and Env STLC/Common.agda constructs shared by two systems: QTAS and its algorithmic formulation
Fig. 8. Syntax (part 2) Context and GenericConsumer STLC/Algo.agda contructs specific to Algo. system
Fig. 9. Algorithmic typing and matching _⊢_⇒_⇒_ and _⊢_≈_ STLC/Algo.agda
line 544 example ex2-derivation STLC/Decl.agda
Theorem Agda File Location Comments (if any)
Lemma 4.1 (Typing Implies Matching) ⊢to≈ STLC/Algo/Properties.agda
Lemma 4.2 (A Full Type Context) ⊢context-full-type STLC/Algo/Properties.agda
Lemma 4.3 (General Subsumption) subsumption-0 STLC/Algo/Properties.agda subsumption is the general form
Lemma 4.4 (Decidability of Tatching) ≈dec' STLC/Algo/Decidable.agda ≈dec is the general form
Lemma 4.5 (Decidability of Typing) ⊢dec' STLC/Algo/Decidable.agda ⊢dec is the general form
Corollary 4.6 (Soundness of Typing) sound-inf0 and sound-chk0 STLC/Soundness.agda sound-inf and sound-chk are the general form
Corollary 4.7 (Completeness of Typing) complete-inf and complete-chk STLC/Completeness.agda complete is the general form

The C& Calculus

Figure Agda File Location Comments (if any)
Fig. 10 Syntax (Part 1) Type, Constant, Env Record/PreCommon.agda
Fig. 10 Syntax (Part 2) Term, Record Record/Common.agda Term and records are mutually defined
Fig. 10 Syntax (Part 3) CCounter, Counter Record/Decl.agda check counter and counters
Fig. 10 Syntax (Part 4) Context, GenericConsumer Record/Algo.agda
Fig. 11 QTAS typing _⊢_#_⦂_, _⊢r_#_⦂_ Record/Decl.agda r stands for records
Fig. 11 QTAS subtyping _≤_#_ Record/Decl.agda
Example (line 1023 and 1053) ex-overloading Record/Decl.agda
Fig. 12 Algo. Typing _⊢_⇒_⇒_, _⊢r_⇒_⇒_ Record/Algo.agda
Fig. 12 Algo. Subtyping ⊢_≤_⇝_ Record/Algo.agda
Theorem Agda File Location Comments (if any)
Lemma 5.1 (Reflexivity of Subtyping (Infinity) ≤refl∞ Record/Decl.agda
Lemma 5.2 (Transitivity of Subtyping) ≤trans Record/Decl/Properties.agda
Lemma 5.3 (A full type context) typing ⊢id-0 Record/Algo/Properties.agda
Lemma 5.4 (A full type context) subtyping ≤id-0 Record/Algo/Properties.agda
Lemma 5.5 (Typing implies subtyping) ⊢to-≤ Record/Algo/Properties.agda
Lemma 5.6 (General Subsumption) subsumption-0 Record/Algo/Properties.agda
Corollary 5.7 (Soundness of Typing) sound-inf-0, sound-chk-0, sound-r Record/Soundness.agda
Corollary 5.8 (Completeness of Typing) complete-inf, complete-chk, complete-r Record/Completeness.agda
Theorem 5.9 (Strong Annotatability) annotatability, annotatability', annotatability-r Record/Annotatability/Elaboration.agda
Theorem 5.10 (Type preservation after erasure) preserve, preserve-r TypeSound/Main.agda
Theorem 5.11 (Preservation of TAS) preserve, preserve-r TypeSound/Target.agda
Theorem 5.12 (Progress of TAS) progress, progress-r TypeSound/Target.agda
Lemma 5.13 (Determinism of Typing) ⊢unique, ⊢r-unique Record/Algo/Uniqueness.agda
Lemma 5.14 (Determinism of Subtyping) ≤unique Record/Algo/Uniqueness.agda
Theorem 5.15 (Decidability of Typing) ⊢dec-0, ⊢r-dec Record/Algo/Decidable.agda
Theorem 5.16 (Decidability of Subtyping) ≤dec-0 Record/Algo/Decidable.agda
Corollary 5.17 (Decidability of the QTAS) qtas-dec-0 Record/Dec.agda