Skip to content

Latest commit

 

History

History
46 lines (27 loc) · 1.62 KB

readme.md

File metadata and controls

46 lines (27 loc) · 1.62 KB
Raw

Revisiting Iso-Recursive Subtyping (Artifact)

Abstract

This bundle contains the Coq formulation associated with the paper "Revisiting Iso-Recursive Subtyping". This document explains how to run the Coq formulations.

Getting Started

We strongly recommend you to install Coq proof assistant by opam2.

  1. Install Coq(=8.13). The proof is built under the version of Coq is 8.13. In Ubuntu-like system, you can install Coq by typing these commands in terminal.

     >> opam install opam-depext
 >> opam-depext coq
 >> sudo apt-get install m4
 >> opam pin add coq 8.13.0

  2. Install metalib. In terminal, type

     >> git clone https://github.com/plclub/metalib.git
 >> cd metalib/Metalib
 (Replace `omega` library by `lia` library since Metalib only supports coq 8.10 in Feb 2022)
 >> make
 >> make install

  3. Now to compile our Coq proof where a makefile is provided. In command line, cd to the src directory and then build the whole project.

     >> cd path_to_src
 >> make clean
 >> make

Guide

The repo contains three sub-folders:

  • OOPSLA: This is the Coq proof for our OOPSLA'20 paper, the paper-to-proofs correspondence guide can be found at the paper.

  • Journal: This is the Coq proof for the extension version, the paper-to-proofs correspondence guide can be found at the paper.

  • SASyLF: This is the SASyLF proof of double unfolding rules provided by John T. Boyland. It uses SASyLf, a proof assistant that using HOAS (higher order abstract syntax) technique while our Coq proof uses locally nameless.