Completely annotated lambda terms (such as are arrived at via the
straightforward encodings of various types from System F) contain
much redundant type information. Consequently, the completely
annotated forms are almost never used in practice, since partially
annotated forms can be defined which still allow syntax directed
type checking. An additional optimization that is used in some proof
and type systems is to take advantage of the context of occurrence of
terms to further elide type information using bidirectional
type checking rules. While this technique is generally effective, we
show that there exist bidirectional terms which exhibit asymptotic
increases in the size of their type decorations when
\emph{sequentialized} into a \emph{named-form} calculus (a common
first step in compilation). In this paper, we introduce a
refinement of the bidirectional type system based on \emph{strict}
logic which allows additional type decorations to be eliminated, and
show that it is well-behaved under sequentialization.