This is the formalisation accompanying the report
Semantics of Recursive Types. Each box is a Coq source file;
click it to read the file rendered with
Alectryon
(coqdoc frontend). Each small diff node on an
edge shows the unified diff between the two files it connects, rendered
with diff2html.
flowchart TD
stlc["stlc.v"]
later["stlc_rec_later.v"]
later_prog["stlc_rec_later_prog.v"]
later_dc["stlc_rec_later_dc.v"]
indexed["stlc_rec_indexed.v"]
indexed_exist["stlc_rec_indexed_exist.v (admitted)"]
appel["stlc_rec_appel.v"]
appel_fp["stlc_rec_appel_fp.v"]
appel_fp2["stlc_rec_appel_fp2.v"]
stlc --> d_later([diff]) --> later
later --> d_later_dc([diff]) --> later_dc
later --> d_later_prog([diff]) --> later_prog
later_dc --> d_indexed([diff]) --> indexed
indexed --> d_indexed_exist([diff]) --> indexed_exist
later_dc --> d_appel([diff]) --> appel
appel --> d_appel_fp([diff]) --> appel_fp
appel --> d_appel_fp2([diff]) --> appel_fp2
classDef diff fill:#fde68a,stroke:#d97706,color:#1f2937,font-size:11px;
class d_later,d_later_dc,d_later_prog,d_indexed,d_indexed_exist,d_appel,d_appel_fp,d_appel_fp2 diff;
click stlc href "sources/stlc.html" "stlc.v" _blank
click later href "sources/stlc_rec_later.html" "stlc_rec_later.v" _blank
click later_prog href "sources/stlc_rec_later_prog.html" "stlc_rec_later_prog.v" _blank
click later_dc href "sources/stlc_rec_later_dc.html" "stlc_rec_later_dc.v" _blank
click indexed href "sources/stlc_rec_indexed.html" "stlc_rec_indexed.v" _blank
click indexed_exist href "sources/stlc_rec_indexed_exist.html" "stlc_rec_indexed_exist.v" _blank
click appel href "sources/stlc_rec_appel.html" "stlc_rec_appel.v" _blank
click appel_fp href "sources/stlc_rec_appel_fp.html" "stlc_rec_appel_fp.v" _blank
click appel_fp2 href "sources/stlc_rec_appel_fp2.html" "stlc_rec_appel_fp2.v" _blank
click d_later href "diffs/stlc_rec_later.html" "stlc.v -> stlc_rec_later.v" _blank
click d_later_dc href "diffs/stlc_rec_later_dc.html" "stlc_rec_later.v -> stlc_rec_later_dc.v" _blank
click d_later_prog href "diffs/stlc_rec_later_prog.html" "stlc_rec_later.v -> stlc_rec_later_prog.v" _blank
click d_indexed href "diffs/stlc_rec_indexed.html" "stlc_rec_later_dc.v -> stlc_rec_indexed.v" _blank
click d_indexed_exist href "diffs/stlc_rec_indexed_exist.html" "stlc_rec_indexed.v -> stlc_rec_indexed_exist.v" _blank
click d_appel href "diffs/stlc_rec_appel.html" "stlc_rec_later_dc.v -> stlc_rec_appel.v" _blank
click d_appel_fp href "diffs/stlc_rec_appel_fp.html" "stlc_rec_appel.v -> stlc_rec_appel_fp.v" _blank
click d_appel_fp2 href "diffs/stlc_rec_appel_fp2.html" "stlc_rec_appel.v -> stlc_rec_appel_fp2.v" _blank