Roadmap first publication
My thesis is split (mainly) in two parts: firstly theory and secondly implementation. The first paper will be about a formal semantics combining the two concepts of the Ownership and Borrowing System and refinements. To be able to publish, I have to do the following:
-
Choose which class of formal semantics I want to use -
Axiomatic→ rarely used -
Denotational → should be okay, but maybe not super amenable to CFGs -
Operational → probably the best, but not sure, yet -
Other→ too obscure
-
-
Find a formal semantics for OBS → Polonius -
Find a formal semantics for refinements -
Liquid types → probably too focused on functional languages -
FRSC → probably good since it introduces refinements for imperative languages and dependent functions (?)
-
-
Translate the formal semantics to the chosen semantics, if needed -
Polonius uses a Datalog model → translation to operational semantics should be straightforward -
Liquid types are denotational (?) -
FRSC uses SSA, thus a variant of operational semantics (?)
-
-
Create a combined formal semantics -
Prove consistency