notes

Non-Atomic Variables var1: [t1 -> v1; t2 -> v2] where var1 is the name of the variable, tx are timestamps, and vx are the values of the variable at those timestamps. Note that t(n+1) must be greater than t(n) Domains Domains are separate spheres of execution. Each thread would have their own Domain, for instance. Frontier Domains have a frontier, which establishes which variables it can see at which timestamp. [Read More]

Unification Algorithm type term = | Var of string | Term of string * term list You either have a type variable with a name, or a type constructor with a name and a list of arguments. Unification takes a list of term pairs which have to be made matching. Unification returns a list of substitutions, where a substitution is a pair of a string and a term, aka the variable name that should be substituted with the term. [Read More]