@techreport{Roversi:2008-WALT-SRN-COMPL,
  number = {104/08},
  month = {April},
  author = {Roversi, Luca},
  url = {http://arxiv.org/abs/0804.0660},
  title = {{W}eak {A}ffine {L}ight {T}yping is complete with respect to {S}afe
           {R}ecursion on {N}otation},
  address = {C.so Svizzera, n.185 --- 10149 Torino --- Italy},
  abstract = {Weak affine light typing (\textsf{WALT}) assigns light affine
              linear formulae as types to a subset of $\lambda$-terms of
              \textsf{System F}. \textsf{WALT} is poly-time sound: if a
              $\lambda$-term $M$ has type in \textsf{WALT}, $M$ can be evaluated
              with a polynomial cost in the dimension of the derivation that
              gives it a type. The evaluation proceeds under any strategy of a
              rewriting relation which is a mix of both call-by-name and
              call-by-value $\beta$-reductions. \textsf{WALT} \textit{weakens},
              namely \textit{generalizes}, the notion of
              ``\textit{stratification of deductions}'', common to some
              \textsf{Light Systems} --- those logical systems, derived from
              Linear logic, to characterize the set of Polynomial functions ---
              . A weaker stratification allows to define a compositional
              \textit{embedding} of Safe recursion on notation (\textsf{SRN})
              into \textsf{WALT}. It turns out that the expressivity of
              \textsf{WALT} is strictly stronger than the one of the known
              \textsf{Light Systems}. The embedding passes through the
              representation of a subsystem of \textsf{SRN}. It is obtained by
              restricting the composition scheme of \textsf{SRN} to one that can
              only use its safe variables \textit{linearly}. On one side, this
              suggests that \textsf{SRN}, in fact, can be redefined in terms of
              more primitive constructs. On the other, the \textit{embedding} of
              \textsf{SRN}\ into \textsf{WALT} enjoys the two following
              remarkable aspects. Every datatype, required by the embedding, is
              represented from scratch, showing the strong structural
              proof-theoretical roots of \textsf{WALT}. Moreover, the embedding
              highlights a stratification structure of the normal and safe
              arguments, normally hidden inside the world of
              \textsf{SRN}-normal/safe variables: the less an argument is
              ``polyomially impredicative'', the deeper, in a formal,
              proof-theoretical sense, it is represented inside \textsf{WALT}.
              Finally, since \textsf{WALT} is \textsf{SRN}-complete it is also
              polynomial-time complete since \textsf{SRN} is.},
  institution = {Dipartimento di Informatica, Torino},
  year = {2008},
}

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)