bibliographyTheoretical-04a.bib
@inproceedings{paoliniRoversiZorzi18TLLA,
author = {Paolini, Luca and Roversi, Luca and Zorzi, Margherita},
year = {2019},
title = {Quantum Programming Made Easy},
editor = {Ehrhard, Thomas and Fern\'andez, Maribel and Paiva, Valeria de and Tortora de Falco, Lorenzo },
booktitle = {{\rm Proceedings Joint International Workshop on}
Linearity \& Trends in Linear Logic and Applications,
{\rm Oxford, UK, 7-8 July 2018}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {292},
publisher = {Open Publishing Association},
pages = {133-147},
doi = {10.4204/EPTCS.292.8},
abstract = {We introduce the functional language IQu ("Haiku")
which, under the paradigm "quantum data & classical control"
and in accordance with the model QRAM, allows to define and
manipulate quantum circuits also by means of intermediate and
partial measurement. Idealized Algol is the reference for the
design of IQu. We extend the type system of Idealized Algol
for typing both quantum-registers, i.e. the stores of quantum
states, and quantum-circuits. The types for quantum-registers
do not make any reference to linear logic formulas and are
parametric on the dimension of the quantum-registers they
are type of. IQu operates on quantum circuits as they were
classical data so no restriction exists on their duplication.
Concerning programming, we show the potential effectiveness of
IQu by encoding well known quantum algorithms in it.}
}
@inproceedings{CanaveseCesenaOucharyPediciniRoversi:FOPARA13,
author = {Canavese, Daniele and Cesena, Emanuele and Ouchary, Rachid and Pedicini, Marco and Roversi, Luca},
title = {{Can a light typing discipline be compatible with an
efficient implementation of finite fields inversion?}},
booktitle = {{Foundational and Practical Aspects of Resource Analysis (subtitle:
3rd International Workshop on Foundational and Practical Aspects of Resource
Analysis, FOPARA 2013)}},
volume = {8552},
series = {{LNCS}},
pages = {38 -- 57},
year = {2014},
editor = {Dal Lago, U. and Pe\~na, R.},
publisher = {Springer},
isbn = {978-3-319-12465-0},
issn = {0302-9743},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2014-FOPARA13/CanaveseCesenaOucharyPediciRoversi2013FOPARA.pdf},
abstract = {We focus on the fragment TFA of lamba-calculus which is known to contain only terms
which normalize in polynomial time. Inside TFA we translated BEA, a well known, imperative
and fast algorithm which calculates the multiplicative inverse of binary finite fields. The translation suggests how to categorize the operations of BEA in sets which drive the design of a variant
that we called DCEA. On several common architectures we show that these two algorithms have
comparable performances, while on UltraSPARC and ARM architectures the variant we synthesized from a purely functional source can go considerably faster than BEA.
},
xxcopyrightspringer = {http://www.springer.de/comp/lncs/index.html}
}
@inproceedings{CesenaPediciniRoversi:FOPARA11,
author = {Cesena, Emanuele and Pedicini, Marco and Roversi, Luca},
title = {{Typing a Core Binary-Field Arithmetic in a Light Logic}},
booktitle = {{Foundational and Practical Aspects of Resource Analysis (subtitle:
2nd International Workshop on Foundational and Practical Aspects of Resource
Analysis, FOPARA 2011)}},
volume = {7177},
series = {{LNCS}},
pages = {19 -- 35},
isbn = {978-3-642-32495-6},
year = {2012},
editor = {Pe\~na, R. and van Eekelen, M. and Shkaravska, O.},
publisher = {Springer},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-DLAL-FF/10dot1007-978-3-642-32495-6_2.pdf},
abstract = {We design a library for binary-field arithmetic and we supply a
core application programming interface (API) completely developed in a formal
system we introduce: Typeable Functional Assembly (TFA) which essentially is the
system Dual Light Affine Logic (DLAL) introduced by Baillot and Terui and extended
with a fix-point formula. TFA is a light type assignment system, in the sense that
substructural rules on types of linear logic allow just to type functional programs
with polynomial evaluation cost. As a consequence, we show the core of a functional
programming setting for binary-field arithmetic with built-in polynomial
complexity.
},
copyrightspringer = {http://www.springer.de/comp/lncs/index.html}
}
@inproceedings{Roversi+Vercelli:2010-DICE10,
author = {Roversi, Luca and Vercelli, Luca},
title = {{Safe Recursion on Notation into a Light Logic by Levels}},
booktitle = {{Proceedings of the Workshop on Developments in Implicit Computational complexity (DICE 2010)}},
volume = {23},
series = {{Electronic Proceedings in Theoretical Computer Science}},
pages = {63 -- 77},
publisher = {On-line},
year = {2010},
month = {March},
issn = {2075-2180},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2010-DICE/RoversiVercelli2010DIC
E.pdf},
abstract = {We embed Safe Recursion on Notation (SRN) into Light Affine Logic by Levels (LALL),
derived from the logic ML4. LALL is an intuitionistic deductive system, with a polynomial time
cut elimination strategy. The embedding allows to represent every term t of SRN as a family of
nets in LALL. Every net in the family simulates t on arguments whose bit length is bounded by
the index of the net. The embedding is based on two crucial features. One is the recursive type
in LALL that encodes Scott binary numerals, i.e. Scott words, as nets. Scott words represent
the arguments of t in place of the more standard Church binary numerals. Also, the embedding
exploits the "fuzzy" borders of paragraph boxes that LALL inherits from ML4 to "freely"
duplicate the arguments, especially the safe ones, of t. Finally, the type of the net depends
on the number of composition and recursion schemes used to define t, namely the structural
complexity of t. Moreover, the size of the net is a polynomial in the index of the net in the
family, whose degree depends on the structural complexity of t. So, this work makes
closer both the predicative recursive theoretic principles SRN relies on, and the proof
theoretic one, called stratification, at the base of Light Linear Logic.
}
}
@inproceedings{RoversiVercelli:2010-FOPARA09,
author = {Roversi, Luca and Vercelli, Luca},
title = {{A structural and local criterion for polynomial time computations}},
booktitle = {{Foundational and Practical Aspects of Resource Analysis (subtitle: 1st International Workshop on Foundational and Practical Aspects of Resource Analysis, FOPARA 2009)}},
year = {2010},
volume = {6324},
pages = {66 -- 81},
editor = {van Eekelen, M. and Shkaravska, O.},
series = {LNCS},
publisher = {Springer},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2009-FOPARA/RoversiVercelli2009FOPARA.pdf},
issn = {0302-9743},
copyrightspringer = {http://www.springer.de/comp/lncs/index.html}
}
@unpublished{Pim+Ron+Rov:ITRS08,
author = {Pimentel, Elaine and Ronchi Della Rocca, Simona and Roversi, Luca},
title = {{I}ntersection {T}ypes from a proof-theoretic perspective},
year = {2008},
note = {Presented at the 4th Workshop on Intersection Types and Related Systems (ITRS '08) -- Torino (Italy)},
month = {March},
url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2008-ITRS/PMR-ITRS08.pdf},
abstract = {In this work we present a proof-theoretical justification for IT by means of the logical system Intersection Synchronous Logic (ISL). ISL builds equivalence classes of deductions of the implicative and conjunctive fragment of 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}
}
@inproceedings{Pim+Ron+Rov:SD-05,
author = {Pimentel, Elaine. and Ronchi Della Rocca, Simona and Roversi, Luca},
booktitle = {Proc. of STRUCTURES AND DEDUCTION - ICALP Workshop, Lisbon July 16-17},
title = {Intersection Types: a proof-theoretical approach},
month = {July},
year = {2005},
pages = {189 -- 204},
issn = {1430-211X},
url = {http://www.ki.inf.tu-dresden.de/~paola/SD05/SD05-Proc.pdf},
note = {Presented at the workshop Structures and Deduction (SD'05)},
abstract = {It is well known that derivations in
Intersection Types (IT) form
a strict subset of deductions in Intuitionistic Logic (LJ) -- up
to term decorations -- in the sense that IT imposes a
meta-theoretical restriction on proofs: conjunction can be
introduced only between derivations that are synchronized with
respect to the implication.
The goal of this work is to present a proof-theoretical
justification for IT. In particular, we discuss the relationship
between the intersection connective and the intuitionistic
conjunction. For this purpose, we define a new logical system
called Intersection Synchronous Logic (ISL), that proves
properties of sets of deductions of the implication-conjunction
fragment of LJ.
The main idea behind ISL is the decomposition of the
intuitionistic conjunction into two connectives, one with
synchronous and the other with asynchronous behavior.
Also in the present work, we prove that ISL enjoys both the
strong normalization and sub-formula properties as well as that
the Intersection Type assignment can be viewed as standard term
decoration of ISL.}
}