For every process *P* there exists a resource *ph *which defines a limit on the number of computational actions that* **P* can take. Before *P *can take an action, it must reduce the value of *ph* by the cost of the action. When *ph* reaches 0, *P *halts.

To side-step issues with consistency and safety, we assign to every *P,* with a resource *ph*, a behavioral type φ_{B} that enforces invariants on the conditions under which *ph* may be accessed. In particular:

*ph*is an exclusively owned resource; and_{ }

*ph*is a linear resource.

In addition, every *P *∈ [[φ_{B}]](v) has two names*, get* and *set*, by which it can modify the value of *ph**.** *To enforce linearity, we require that *get* and *set* are only used in alternation. To enforce exclusivity, we require that *ph** *is viewable only by its "owner" process,

*P.*This constraint is necessary to ensure that, for any given

*P*

_{1}| P_{2},*ph*is not siphoned off by a greedy

_{1}*P*

_{2}....

in addition to the valuation function v : V → ( Proc ), where V is the set of propositional variables used in the rec production. Below, we give an interpretation of the "bounded" behavioral type φ_{B }for each formulae generated by the production above. Where there exists no exceptionally interesting interpretation for φ_{B}, a description is given of the formula's semantic.

[[ true ]](v) = Proc

A process *P* satisfies *true* if *ph** _{ }*is accessed according to the linearity and exclusivity constraints defined by the bounded type φ

_{B}.

[[ 0 ]](v) = { P : P ≡ 0 }

...

A resource *P* satisfies the negation type *P* : ¬φ_{B} if either linearity or exclusivity are broken during the execution of *P.*

...

A process *P* satisfies the conjunction type *P* : φ & ψ if it satisfies both *P* : φ and *P* : ψ.

[[ φ | ψ ]](v) = { P : ∃P_{0}, P_{1}.P ≡ P_{0} | P_{1}, P_{0} ∈ [[φ]](v), P_{1} ∈ [[ψ]](v) }

A process *P* satisfies *P :* φ_{B }| ψ_{B} if *P* is the parallel composition of two separate, yet bounded, processes, *P*_{1 }: φ_{B} and *P** _{2} *: ψ

_{B}, respectively. Thus,

*ph*can be thought of as the composition of two mutually-exclusive sub-resources,

*ph*and

_{1}*ph*belonging to

_{2}*P*

_{1}and

*P*

_{2}....

A process *P* satisfies the elevation type *P* : a!(φ_{B}) if it exports a bounded process *P' :* φ_{B }with resources *ph*. Note that, because φ_{B} is a least relation, *P'* maintains ownership of its resource even as its communicated. If *P' *is not an owner, but a resource such as**ph*, the process *P* : a!(*b) is still well-typed. It represents an owner which is transferring ownership of *ph* to the receiving process.

[[ a?b.φ ]](v) = { P : ∃Q, P' .P ≡ Q | x(y).P' , x ∈ ((a))(v), ∀c.∃z.P' {z/y} ∈ [[φ{c/b}]](v) }

...

[[ rec X . φ ]](v) = ∪ { S ⊆ Proc : S ⊆ [[φ]](v{S/X}) }

A process *P* satisfies the greatest fix point if all future recursive calls preserve the satisfiability of φ_{B. }This effectively guarantees exclusivity and linearity of *ph _{X} *under recursion.

[[ ∀n : ψ . φ ]](v) = ∩_{x∈((@ψ))(v)} [[φ{x/n}]](v)

Similar to elevation, quantification has two interesting cases. In the first case, quantification expresses the conditions necessary to substitute an *owner* *x *: @ψ_{B} into the environment φ. If [[φ{x/n}]](v) := *true*{x/n} and [[*x]](v) ⊆ *true*{x/n}, we can infer that *x* is later expanded back into it's process form *X* : ψ_{B}. Furthermore, *true*{x/n} asserts that, if *ph _{X}* is later accessed, linearity and exclusivity are respected.

The In the second case, where the resource *x* ∈ @*b*, *is being substituted into φ, if [[φ{x/n}]](v) := *true*{x/n}, we can infer that linearity and exclusivity of *x** _{ }*is preserved under substitution.

...