Weekend 1

Difficulty motivating myself to delve into the details. I must find a better approach, or else Felix will invest in a cattle prod. I don't know if I want to have to explain scorch marks to my manager at Sun. "It's nothing. I walked into a door. An... electric door."

Worked out some more intuition into CS (core selftype) systems of constraints. The "context" construct in types (B{A} = A if B=selftype, B{A} = B otherwise) is used as conditional, so U_x <= VA_x if x = true, and U_x <= VB_x if x = false. These types are made incompatible; there is no T such that T <= VA_x and T <= VB_x. Constraint solutions for true and false are given, then used to construct a CS-solution from a SAT-solution for boolean formulae. Because false maps to selftype and true maps to record types, the reverse mapping is trivial (selftype |-> false; anything other type T |-> true).

ADDENDUM:
I wrote this Sunday night, but apparently forgot to hit Publish Post, so this is going up Monday night.
I am currently starting on my Monday work.