##
Complexity of Model-Checking Call-by-Value Programs

### Takeshi Tsukada

In this talk, we study the complexity of the reachability problem
(a typical and practically important instance of the model-checking
problem) for simply-typed call-by-value programs with recursion, Boolean
values, and non-deterministic branch, and show the following results.
(1) The reachability problem for order-3 programs is nonelementary.
Thus, unlike in the call-by-name case, the order of the input program
does not serve as a good measure of the complexity. (2) Instead, the
depth of types is an appropriate measure: the reachability problem for
depth-n programs is n-EXPTIME complete. In particular, the previous
upper bound given by the CPS translation is not tight. The algorithm
used to prove the upper bound result is based on a novel intersection
type system, which we believe is of independent interest.