Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
e45lee authored Mar 4, 2024
1 parent 9e54428 commit a68d573
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,8 @@ The artifact consists of the Coq proofs for our paper, based on the [POPLMark 08
Article 21 (December 2023), 52 pages.](https://doi.org/10.1145/3618003)
5. System Fq (in [ExtendedBase](ExtendedBase)), modelling a qualifier system over an arbitrary initial qualifier lattice.

Additionally, we give a mechanized proof of the crux of [Galatos' result](https://link.springer.com/article/10.1007/s11225-023-10063-4) in [LatticeReflTrans.v](LatticeReflTrans.v) formed by extracting the relevant parts
of the proof of reflexivity and transitivity of the subqualification relation
in System Fq.
Additionally, we give a mechanized proof of the crux of [Negri's result](https://link.springer.com/content/pdf/10.1007/s000120200012.pdf) in [LatticeReflTrans.v](LatticeReflTrans.v) formed by extracting the relevant parts
of the proof of reflexivity and transitivity of the subqualification relation in System Fq.

## Getting Started -- Building Locally

Expand Down

0 comments on commit a68d573

Please sign in to comment.