Skip to content

Latest commit

 

History

History
27 lines (21 loc) · 1.03 KB

README.md

File metadata and controls

27 lines (21 loc) · 1.03 KB
Raw

MiniJl for FTfJP 2019

Submission for FTfJP-2019: decidable tag-based semantic subtyping for a subset of the Julia language.

  • paper directory contains the paper. Run make withing this directory to build a pdf.

  • Mechanization directory contains Coq code relevant to the paper. Run make within the directory to compile it.

    • Mechanization/MiniJl has all the definitions and proofs related to tag-based semantic subtyping presented in the paper.

    • Mechanization/FullAtomicJl has all the definitions and proofs related to the alternative tag-based semantic subtyping discussed in Sec. 5. (Almost the same as MiniJl but with atomic normal form.)

    • Mechanization/AtomicJl has only the definitions and proofs of FullAtomicJl that concern the equivalence of declarative and reductive definitions of subtyping, without the connection to semantic subtyping.