@techreport{Roversi:2007-WALT-FULL,
  number = {103/07},
  month = {December},
  author = {Roversi, Luca},
  url = {http://arxiv.org/abs/0712.4222v2},
  title = {{W}eak {A}ffine {L}ight {T}yping: {I}ntensional expressivity,
           {P}olytime soundness and completeness},
  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 in
              \textsf{System F}. \textsf{WALT} is poly-time sound: if a
              $\lambda$-term $M$ has type in WALT, $M$ can be evaluated with a
              polynomial cost in the dimension of the derivation that gives it a
              type. In particular, the evaluation can proceed under any strategy
              of a rewriting relation, obtained as a mix of both
              call-by-name/call-by-value $\beta$-reductions. \textsf{WALT} is
              poly-time complete since it can represent any poly-time Turing
              machine. \textsf{WALT} \textit{weakens}, namely
              \textit{generalizes}, the notion of stratification of deductions
              common to some \textsf{Light Systems} --- we call as such those
              logical systems, derived from Linear logic, to characterize
              \textsf{FP}, the set of Polynomial functions --- . A weaker
              stratification allows to define a compositional \textit{embedding}
              of the \textit{Quasi}-linear fragment \textsf{QlSRN} of Safe
              recursion on notation (\textsf{SRN}) into \textsf{WALT}.
              \textsf{QlSRN} is \textsf{SRN}, which is a recursive-theoretical
              system characterizing \textsf{FP}, where only the composition
              scheme is restricted to \textit{linear safe variables}. So, the
              expressivity of \textsf{WALT} is stronger, as compared to the
              known \textsf{Light Systems}. In particular, using the types, the
              \textit{embedding} puts in evidence the stratification of normal
              and safe arguments hidden in \textsf{QlSRN}: the less an argument
              is impredicative, the deeper, in a formal, proof-theoretical
              sense, gets its representation in \textsf{WALT}.},
  institution = {Dipartimento di Informatica, Torino},
  year = {2007},
}

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