Remaining Work for the Paper
Here are the tasks we need to complete for the paper:
-
(Max) Define the cast-calculus syntax, typing and equational theory (CBPV) -
(Max) Give a semantics for the terms of the cast calculus in a concrete term model (where we construct Dyn
as a set) -
(Max) Define the cast-calculus inequational theory
Abstract categorical models:
-
(Max) Show that we can interpret the inequational axioms in any extensional model of GTT (should be straightforward) -
(Eric) Finish describing the step-by-step construction of an extensional model from a double CBPV model w/ bisimilarity
Concrete extensional model (terms + inequational theory):
-
(Eric) Build a specific double CBPV model w/ bisimilarity (predomains/error domains, lift monad, dyn, etc.) and apply the abstract construction of an extensional model -
(Eric) Sketch the proof of adequacy for the above extensional model
Edited by ericgio