bibliographyTheoretical-03a.bib
@article{2318_1734164MatosPaoliniRoversiTCSICTCS18,
author = {Armando, Matos and Luca, Paolini and Luca, Roversi},
title = {The fixed point problem of a simple reversible language},
year = {2020},
journal = {THEORETICAL COMPUTER SCIENCE},
volume = {813},
abstract = {SRL is a total programming language with distinctive features: (i) every program that mentions n registers defines a bijection Zn→Zn, and (ii) the generation of the SRL-program that computes the inverse of that bijection can be automatic. Containing SRL a very essential set of commands, it is suitable for studying strengths and weaknesses of reversible computations. We deal with the fixed points of SRL-programs. Given any SRL-program P, we are interested in the problem of deciding if a tuple of initial register values of P exists which remains unaltered after its execution. We show that the existence of fixed points in SRL is undecidable and complete in Σ10. We show that such problem remains undecidable even when the number of registers mentioned by P is limited to 12. Moreover, if we restrict to the linear programs of SRL, i.e. to those programs where different registers control nested loops, then the problem is already undecidable for the class of SRL-programs that mention no more than 3712 registers. Last, we show that, except for trivial cases, finding if the number of fixed points has a given cardinality is also undecidable.},
keywords = {Reversible computing, Fixed points, Decidability},
url = {http://www.sciencedirect.com/science/article/pii/S0304397519306280},
doi = {https://doi.org/10.1016/j.tcs.2019.10.005},
pages = {143--154}
}
@article{2318_1734163PaoliniPiccoloRoversiTCS,
author = {Paolini, L. and Piccolo, M. and Roversi, L.},
title = {A class of Recursive Permutations which is Primitive Recursive complete},
year = {2020},
journal = {THEORETICAL COMPUTER SCIENCE},
volume = {813},
abstract = {We focus on total functions in the theory of reversible computational models. We define a class of recursive permutations, dubbed Reversible Primitive Permutations (RPP) which are computable invertible total endo-functions on integers, so a subset of total reversible computations. RPP is generated from five basic functions (identity, sign-change, successor, predecessor, swap), two notions of composition (sequential and parallel), one functional iteration and one functional selection. RPP is closed by inversion and it is expressive enough to encode Cantor pairing and the whole class of Primitive Recursive Functions.},
keywords = {Reversible computation, Unconventional computing models, Computable permutations, Primitive recursive functions, Recursion theory},
url = {http://www.sciencedirect.com/science/article/pii/S0304397519307558},
url = {https://doi.org/10.1016/j.tcs.2019.11.029},
doi = {10.1016/j.tcs.2019.11.029},
pages = {218--233}
}
@article{2318_1750054CurziRoversiTCSDICE18,
author = {Luca Roversi, Gianluca Curzi},
title = {A type-assignment of linear erasure and duplication},
year = {2020},
journal = {THEORETICAL COMPUTER SCIENCE},
volume = {837},
abstract = {We introduce LEM, a type-assignment system for the linear λ-calculus that extends second-order IMLL2, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, but in a purely linear setting. LEM enjoys both a mildly weakened cut-elimination, whose computational cost is cubic, and Subject reduction. A translation of LEM into IMLL2 exists such that the derivations of the former can exponentially compress the dimension of the derivations in the latter. LEM allows for a modular and compact representation of boolean circuits, directly encoding the fan-out nodes, by means of contraction, and disposing garbage, by means of weakening. It can also represent natural numbers with terms very close to standard Church numerals which, moreover, apply to Hereditarily Finite Permutations, i.e. a group structure that exists inside the linear λ-calculus.},
keywords = {Second-order multiplicative linear logic, Type-assignment, Linear -calculus, Cut-elimination (cost), Boolean circuits, Numerals, Hereditarily finite permutations},
url = {http://www.sciencedirect.com/science/article/pii/S0304397520302516},
doi = {https://doi.org/10.1016/j.tcs.2020.05.001},
pages = {26--53}
}
@article{PAOLINI2020218,
title = {A class of Recursive Permutations which is Primitive Recursive complete},
journal = {Theoretical Computer Science},
volume = {813},
pages = {218 - 233},
year = {2020},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2019.11.029},
url = {http://www.sciencedirect.com/science/article/pii/S0304397519307558},
author = {Luca Paolini and Mauro Piccolo and Luca Roversi},
keywords = {Reversible computation, Unconventional computing models, Computable permutations, Primitive recursive functions, Recursion theory},
abstract = {We focus on total functions in the theory of reversible computational models. We define a class of recursive permutations, dubbed Reversible Primitive Permutations (RPP) which are computable invertible total endo-functions on integers, so a subset of total reversible computations. RPP is generated from five basic functions (identity, sign-change, successor, predecessor, swap), two notions of composition (sequential and parallel), one functional iteration and one functional selection. RPP is closed by inversion and it is expressive enough to encode Cantor pairing and the whole class of Primitive Recursive Functions.}
}
@article{MATOS2020143,
title = {The fixed point problem of a simple reversible language},
journal = {Theoretical Computer Science},
volume = {813},
pages = {143 - 154},
year = {2020},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2019.10.005},
url = {http://www.sciencedirect.com/science/article/pii/S0304397519306280},
author = {Armando B. Matos and Luca Paolini and Luca Roversi},
keywords = {Reversible computing, Fixed points, Decidability},
abstract = {SRL is a total programming language with distinctive features: (i) every program that mentions n registers defines a bijection Zn→Zn, and (ii) the generation of the SRL-program that computes the inverse of that bijection can be automatic. Containing SRL a very essential set of commands, it is suitable for studying strengths and weaknesses of reversible computations. We deal with the fixed points of SRL-programs. Given any SRL-program P, we are interested in the problem of deciding if a tuple of initial register values of P exists which remains unaltered after its execution. We show that the existence of fixed points in SRL is undecidable and complete in Σ10. We show that such problem remains undecidable even when the number of registers mentioned by P is limited to 12. Moreover, if we restrict to the linear programs of SRL, i.e. to those programs where different registers control nested loops, then the problem is already undecidable for the class of SRL-programs that mention no more than 3712 registers. Last, we show that, except for trivial cases, finding if the number of fixed points has a given cardinality is also undecidable.}
}
@article{Paolini2018NGC,
author = {Paolini, Luca
and Piccolo, Mauro
and Roversi, Luca},
title = {On a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensions},
journal = {New Generation Computing},
year = {2018},
month = {July},
day = {01},
volume = {36},
number = {3},
pages = {233--256},
abstract = {Reversible computing is both forward and backward deterministic. This means that a uniquely determined step exists from the previous computational configuration (backward determinism) to the next one (forward determinism) and vice versa. We present the reversible primitive recursive functions (RPRF), a class of reversible (endo-)functions over natural numbers which allows to capture interesting extensional aspects of reversible computation in a formalism quite close to that of classical primitive recursive functions. The class RPRF can express bijections over integers (not only natural numbers), is expressive enough to admit an embedding of the primitive recursive functions and, of course, its evaluation is effective. We also extend RPRF to obtain a new class of functions which are effective and Turing complete, and represent all Kleene's {\$}{\$}{\backslash}upmu {\$}{\$} $\mu$ -recursive functions. Finally, we consider reversible recursion schemes that lead outside the reversible endo-functions.},
issn = {1882-7055},
doi = {10.1007/s00354-018-0039-1},
url = {https://doi.org/10.1007/s00354-018-0039-1}
}
@article{PaoliniPiccoloRoversi-ENTCS2016,
author = {Paolini, Luca and Piccolo, Mauro and Roversi, Luca},
title = {A Class of Reversible Primitive Recursive Functions},
volume = {322},
number = {18605},
pages = {227--242},
year = {2016},
doi = {10.1016/j.entcs.2016.03.016},
abstract = {Reversible computing is bi-deterministic which means that its execution is both forward and backward
deterministic, i.e. next/previous computational step is uniquely determined. Various approaches exist to catch its
extensional or intensional aspects and properties. We present a class RPRF of reversible functions which holds at bay
intensional aspects and emphasizes the extensional side of the reversible computation by following the style of
Dedekind-Robinson Primitive Recursive Functions. The class RPRF is closed by inversion, can only express bijections on
integers --- not only natural numbers ---, and it is expressive enough to simulate Primitive Recursive Functions, of course,
in an effective way.},
url = {http://dx.doi.org/10.1016/j.entcs.2016.03.016},
journal = {Electronic Notes in Theoretical Computer Science}
}
@article{Roversi01042016,
author = {Roversi, Luca},
title = {A deep inference system with a self-dual binder which is complete for linear lambda calculus},
volume = {26},
number = {2},
pages = {677-698},
year = {2016},
doi = {10.1093/logcom/exu033},
abstract = {We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVB that extends SBV by adding the self-dual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cut-elimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model $\beta$-reduction of linear $\lambda$-calculus inside the cut-free subsystem BVB of SBVB. The long-term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal and incremental extensions of SBV.},
url = {http://logcom.oxfordjournals.org/content/26/2/677.abstract},
journal = {Journal of Logic and Computation},
note = {Preliminary version at \url{https://arxiv.org/abs/1212.4483}}
}
@article{Canavese2015,
title = {Light combinators for finite fields arithmetic },
journal = {Science of Computer Programming },
volume = {111},
number = {3},
pages = {365 --- 394 },
year = {2015},
month = {November},
note = {},
issn = {0167-6423},
doi = {http://dx.doi.org/10.1016/j.scico.2015.04.001},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2015-SCICOJ/CanaveseCesenaOucharyPediciniRoversiSCICO215.pdf},
author = {Canavese, Daniele and Cesena, Emanuele and Ouchary, Rachid and Pedicini, Marco and Roversi, Luca},
keywords = {Lambda calculus},
keywords = {Finite fields arithmetic},
keywords = {Type assignments},
keywords = {Implicit computational complexity },
abstract = {Abstract This work completes the definition of a library which provides the
basic arithmetic operations in binary finite fields as a set of functional terms with very
specific features. Such a functional terms have type in Typeable Functional Assembly
(TFA). TFA is an extension of Dual Light Affine Logic (DLAL). DLAL is a type assignment
designed under the prescriptions of Implicit Computational Complexity (ICC), which
characterises polynomial time costing computations. We plan to exploit the functional
programming patterns of the terms in the library to implement cryptographic primitives
whose running-time efficiency can be obtained by means of the least hand-made tuning as
possible. We propose the library as a benchmark. It fixes a kind of lower bound on the
difficulty of writing potentially interesting low cost programs inside languages that can
express only computations with predetermined complexity. In principle, every known and
future (ICC) compliant programming language for polynomially costing computations should
supply a simplification over the encoding of the library we present, or some set of
combinators of comparable interest and difficulty. We finally report on the applicative
outcome that our library has and which is a reward we get by programming in the very
restrictive scenario that TFA provides. The term of TFA which encodes the inversion in
binary fields suggested us a variant of a known and efficient imperative implementation of
the inversion itself given by Fong. Our variant, can outperform Fong's implementation of
inversion on specific hardware architectures. }
}
@article{Pimentel+Ronchi+Roversi:2012-FI,
author = {{P}imentel, {E}laine and {Ronchi Della Rocca}, {S}imonetta and {R}oversi, {L}uca},
title = {{I}ntersection {T}ypes from a {P}roof-theoretic {P}erspective},
journal = {{F}undamenta {I}nformaticae},
year = {2012},
key = {Computer & Communication Sciences},
volume = {121},
issn = {0169-2968},
number = {1-4},
pages = {253---274},
month = dec,
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2012-FI/PimentelRonchiRoversi2012FI.pdf},
abstract = {In this work we present a proof-theoretical justification for the intersection type assignment
system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds
classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic
logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous
conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous
one, that can be applied among any sets of deductions of NJ. A term decoration of ISL
exists so that it matches both: the IT assignment system, when only the synchronous conjunction is
used, and the simple types assignment with pairs and projections, when the asynchronous conjunction
is used. Moreover, the proof of strong normalization property for ISL is a simple consequence
of the same property in NJ and hence strong normalization for IT comes for free.}
}
@article{Asperti+Roversi:2002-ToCL,
author = {Asperti, Andrea and Roversi, Luca},
title = {Intuitionistic Light Affine Logic},
journal = {ACM Trans. Comput. Logic},
issue_date = {January 2002},
volume = {3},
number = {1},
month = jan,
year = {2002},
issn = {1529-3785},
pages = {137--175},
numpages = {39},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2002-ToCL/AspertiRoversi2002ToCL.pdf},
doi = {10.1145/504077.504081},
acmid = {504081},
publisher = {ACM},
address = {New York, NY, USA},
abstract = {This paper is a structured introduction to Intuitionistic Light
Affine Logic (ILAL). ILAL has a polynomially costing normalization, and it
is expressive enough to encode, and simulate, all PolyTime Turing machines.
The bound on the normalization cost is proved by introducing the proof-nets
for ILAL. The bound follows from a suitable normalization strategy that
exploits structural properties of the proof-nets. This allows to have a
good catch on the meaning of the paragraph modality, which is a peculiarity
of light logics. The expressive power of ILAL is demonstrated in full
details. Such a proof gives a flavor of the non trivial task of programming
with resource limitations, using ILAL derivations as programs.}
}
@article{Roversi:2000-IJFCS,
author = {Roversi, Luca},
title = {Light Affine Logic as a Programming Language: a First Contribution },
journal = {International Journal of Foundations of Computer Science},
publisher = {World Scientific},
year = {2000},
month = {March},
volume = 11,
number = 1,
pages = {113 --- 152},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2000-IJFCS/Roversi2000IJFCS.pdf},
abstract = {This work is about an experimental paradigmatic functional
language for programming with P-TIME functions. The language is designed
from Intuitionistic Light Affine Logic. It can be typed automatically by a
type inference algorithm that deduces polymorphic types a la ML.}
}
@article{Pravato+Ronchi+Roversi:1999-MSCS,
author = {Pravato, Alberto and {Ronchi della Rocca}, Simonetta and Roversi, Luca},
title = {The call by value $\lambda$-calculus: a semantic investigation},
journal = {Mathematical Structures in Computer Science},
year = {1999},
volume = 9,
number = 5,
pages = {617 --- 650},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/1999-MSCS/PravatoRonchiRoversi1999MSCS.pdf},
abstract = {This paper is about a categorical approach for modeling the
pure (i.e., without constants) call-by-value lambda-calculus, defined by
Plotkin as a restriction of the call-by-name lambda-calculus. In particular,
the properties a category CC must enjoy to describe a model of call-by-value
lambda-calculus are given. The category CC is general enough to catch models
in Scott Domains and Coherence Spaces.}
}
@article{Ronchi-Roversi:1997-STUDIA-LOGICA,
author = {{Ronchi Della Rocca}, Simonetta and Roversi, Luca},
title = {Lambda calculus and Intuitionistic Linear Logic},
journal = {Studia Logica},
year = {1997},
volume = {59},
number = {3},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/1997-STUDIA-LOGICA/RonchiRoversi1997STUDIALOGICA.pdf}
}