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

 Roversi:2008-WALT-SRN-COMPL (Technical report) Author(s) Luca Roversi Title « Weak Affine Light Typing is complete with respect to Safe Recursion on Notation » Number 104/08 Institution Dipartimento di Informatica, Torino Year 2008 Address C.so Svizzera, n.185 --- 10149 Torino --- Italy URL http://arxiv.org/abs/0804.0660
 Abstract Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of $\lambda$-terms of 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. 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. WALT weakens, namely generalizes, the notion of stratification of deductions'', common to some Light Systems --- those logical systems, derived from Linear logic, to characterize the set of Polynomial functions --- . A weaker stratification allows to define a compositional embedding of Safe recursion on notation (SRN) into WALT. It turns out that the expressivity of WALT is strictly stronger than the one of the known Light Systems. The embedding passes through the representation of a subsystem of SRN. It is obtained by restricting the composition scheme of SRN to one that can only use its safe variables linearly. On one side, this suggests that SRN, in fact, can be redefined in terms of more primitive constructs. On the other, the embedding of SRN into 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 WALT. Moreover, the embedding highlights a stratification structure of the normal and safe arguments, normally hidden inside the world of SRN-normal/safe variables: the less an argument is polyomially impredicative'', the deeper, in a formal, proof-theoretical sense, it is represented inside WALT. Finally, since WALT is SRN-complete it is also polynomial-time complete since SRN is.

 BibTeX code

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

 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)