Skip to content

Commit

Permalink
README: fix more broken links
Browse files Browse the repository at this point in the history
  • Loading branch information
@pmbittner
pmbittner committed Jul 5, 2024
1 parent d921f5d commit cb8b25d
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ In particular, our library provides,
The library is organized as follows:

- The [src/Framework](src/Framework) directory contains the definitions of our formal framework, defined in Section 4 in our paper.
- [VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics.
- [VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics.
- Soundness and completeness are defined in the [Properties](src/Framework/Properties) sub-directory.
- Definitions for expressiveness and configuration equivalence are in the [Relation](src/Framework/Relation) sub-directory.
- Theorems for proofs for free (Section 4.4) are within the [Proof](src/Framework/Proof) sub-directory, including several additional interesting theorems, which did not fit into the paper.
Expand Down Expand Up @@ -341,7 +341,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
| | Gruler's Language | `Gruler` | [src/Lang/Gruler.agda](src/Lang/Gruler.agda) | |
| | Option Calculus | `WFOC`, `OC` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | In contrast to the paper, WFOC duplicates the artifact constructor to enforce the existence of a top-level artifact. |
| | Feature Structure Trees | `FST` | [src/Lang/FST.agda](src/Lang/FST.lagda.md) | |
| | Clone-and-Own (List of Variants) | `VariantList` | [src/Lang/VariantList.agda](src/Lang/VariantList.agda) | |
| | Clone-and-Own (List of Variants) | `VariantList` | [src/Lang/VariantList.lagda.md](src/Lang/VariantList.lagda.md) | |
| Definition 4.1 | Indexed Set | `IndexedSet` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | |
| Definition 4.3 | Indexed Set Inclusion ⋿ | `_∈_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | |
| | Subset ⊑ | `_⊆_`, `_⊆[_]_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | In contrast to `_⊆_`, `_⊆[_]_` requires an explicit mapping between the indices of the two indexed sets which can be useful information. |
Expand All @@ -354,8 +354,8 @@ The following table shows where each of the definitions, theorems, and proofs fr
| Definition 4.10 | Semantic Domain | `VMap` | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. |
| Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | |
| Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | |
| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md) | |
| | | `VariabilityLanguage` | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. |
| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | |
| | | `VariabilityLanguage` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. |
| Definition 4.15 | Complete(𝐿) | `Complete` | [src/Framework/Properties/Completeness.lagda.md](src/Framework/Properties/Completeness.lagda.md) | |
| Definition 4.16 | Sound(𝐿) | `Sound` | [src/Framework/Properties/Soundness.lagda.md](src/Framework/Properties/Soundness.lagda.md) | |
| Definition 4.17 | ⪰ | `_≽_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | |
Expand Down Expand Up @@ -389,7 +389,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
| Corollary 5.13 | Sound(OC) | `OC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Theorem 5.14 | ¬Complete(OC) | `OC-is-incomplete` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | |
| Theorem 5.15 | 2CC ≻ OC | `2CC≻WFOC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.agda](src/Lang/FST.agda) | |
| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.lagda.md](src/Lang/FST.lagda.md) | |
| Theorem 5.17 | OC ⋡ FST | `WFOC⋡FST` | [src/Translation/Lang/FST-to-OC.lagda.md](src/Translation/Lang/FST-to-OC.lagda.md) | |
| Theorem 5.18 | FST ⋡ OC | `FSTL⋡WFOCL` | [src/Translation/Lang/OC-to-FST.agda](src/Translation/Lang/OC-to-FST.agda) | |
| Corollary 5.19 | FST ⋡ 2CC | `FST⋡2CC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | |
Expand Down

0 comments on commit cb8b25d

Please sign in to comment.