Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

 Roversi:2007-WALT-FULL (Technical report) Author(s) Luca Roversi Title « Weak Affine Light Typing: Intensional expressivity, Polytime soundness and completeness » Number 103/07 Institution Dipartimento di Informatica, Torino Year 2007 Address C.so Svizzera, n.185 --- 10149 Torino --- Italy URL http://arxiv.org/abs/0712.4222v2
 Abstract Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of lambda-terms in System F. 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. WALT is poly-time complete since it can represent any poly-time Turing machine. WALT weakens, namely generalizes, the notion of stratification of deductions common to some Light Systems --- we call as such those logical systems, derived from Linear logic, to characterize FP, the set of Polynomial functions --- . A weaker stratification allows to define a compositional embedding of the Quasi-linear fragment QlSRN of Safe recursion on notation (SRN) into WALT. QlSRN is SRN, which is a recursive-theoretical system characterizing FP, where only the composition scheme is restricted to linear safe variables. So, the expressivity of WALT is stronger, as compared to the known Light Systems. In particular, using the types, the embedding puts in evidence the stratification of normal and safe arguments hidden in QlSRN: the less an argument is impredicative, the deeper, in a formal, proof-theoretical sense, gets its representation in WALT.

 BibTeX code

@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},
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

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