externals

Ordering

Visibility

abstract class ExternalConditionRule extends CheckingRule
the abstract type of rules that realize a side condition for a particular key

object CallByValue
helper object for identifier
object EqualityLock extends ExtensionalityRule
K |- Unlock(s) = Unlock(t): T ---> |- s = t : LockType(K,T)
object InferLockTerm extends InferenceRule
K |- t:T ---> |- LockTerm(K,t) : LockType(K,T)
object InferLockType extends InferenceRule
K |- T:type ---> |- LockType(K,T): type
object InferUnlock extends InferenceRule
G |- t: LockType(K,T) and K=Key(p,n,s) in G and p(a,b) ---> U: T
object Key extends TernaryConstantScala
convenience operator to bundle k,a,b into a single object Key(k, a, b)
object LockTerm extends FouraryConstantScala
LockTerm(k,a,b,t) is the term \mathcal{L}^k_{a,b}[t] from the paper for a term t We also write LockTerm(K,t) if K=Key(k,a,b) is known.
object LockType extends FouraryConstantScala
LockType(k,a,b,T) is the term \mathcal{L}^k_{a,b}[T] from the paper for a type T We also write LockType(K,T) if K=Key(k,a,b) is known.
object Locks
helper objects for identifiers
object TypingLock extends TypingRule
K |- Unlock(t): T ---> |- LockType(K,T)
object Unlock extends UnaryConstantScala
Unlock(t) is the term \mathcal{U}^k_{a,b}[T] from the paper for a terms t: LockType(k,a,b,T) The additional arguments used in the paper are not actually needed in the internal syntax.
object UnlockLock extends ComputationRule
Unlock(LockTerm(K,t) = t
object ValRule extends ExternalConditionRule
Key(Val, tm, tp) checks whether tm is Val N is an abstraction of of the form free(_)

Packages