Computer Science is a key discipline in the context of modern society. Despite its technological advances, Computer Science is still immature from the scientific point of view. Just think of the difficulties to certify --- functionally and in terms of resources used, for example --- the correctness of the compositions of software modules running within a distributed environment. Our background and our scientific inclinations will help us to contribute to an advancement of foundational knowledge about computing inside Past and current collaborations activities.

Our favourite method is to analyse aspects of mathematical abstractions who bought a central importance in the theory of computation, even after the birth of new computational models which are based on the physics of computational processes andwhich also urge to look with a new awareness issues such as the traditional distributed and asynchronous

computing. In general, these are problems of interaction between processes in space and time, where time and space are in turn reconsidered in a key computational. We work according to a vision that puts the construction of theories which help to explain the concept of "calculation" to the center of our research. We are focused on the foundational aspects of the technical concepts that we study, rather than to the solution of individual contingent problems. The belief is that the computational science, as such, has an absolute need for a revision of both its mathematical and, in a broad sense, philosophical bases.

• (2013-2015) "Linear Techniques For The Analysis Of Languages (LINTEL)" TO_Call1_2012_0085 with Paolini as principal investigator,
• (2012-2015) PRIN "Metodi Logici per il trattamento dell'informazione" with Berardi as local coordinator,
• (2012-2014) Royal Society’s joint project "Sharing and Sequentiality in Proof Systems with Locality" in collaboration with the University of Bath and Roversi  oversea coordinator,
• (2010-2012) INRIA’s equipe associeé "Contrôle des Ressources par Interprétations Sémantiques et Théorie de la démonstration Linéaire (CRISTAL)" with Ronchi Della Rocca as local coordinator,
• (2010-2012) CNRS Project International de Coopération Scientifique "Logique Lineaire et applications (PICS)" with Ronchi Della Rocca as local coordinator,
• (2007-2009) PRIN "Control and Certification of Resources" with Ronchi Della Rocca as local coordinator,
• MCTAAP 2008H49TEH_002 (2010-2012) with Berardi as local coordinator,
• (2004-2007) EU 6th framework programme with Berardi as local coordinator,
• (2004-2006) PRIN "Logical Foundations of Abstract Programming Languages (FOLLIA)" with Ronchi Della Rocca as national coordinator,
• (2000-2006) MCTAAP projects, with Berardi as local coordinator,
• (2002-2004) PRIN "From Proofs to Computation Through Linear Logic (PROTOCOLLO)" with Ronchi Della Rocca as national coordinator.

Dr. Mauro Piccolo

Dott.ssa Silvia Steila

Erika Debenedetti

Luca Fossati

Marco Gaboardi

Luigi Liquori

Michele Pagani

Alberto Pravato

Alexis Saurin

Luca Vercelli

Stefano Berardi

+ 39 011 670 6750

stefano@di.unito.it

Authors: Paolini L.; Piccolo M.; Roversi L.

A class of Recursive Permutations which is Primitive Recursive complete

Published in: THEORETICAL COMPUTER SCIENCE, Year: 2020

Authors: Armando Matos, Luca Paolini, Luca Roversi

The fixed point problem of a simple reversible language

Published in: THEORETICAL COMPUTER SCIENCE, Year: 2020

Authors: ter Beek, Maurice H.*; Damiani, Ferruccio; Gnesi, Stefania; Mazzanti, Franco; Paolini, Luca

On the expressiveness of modal transition systems with variability constraints

Published in: SCIENCE OF COMPUTER PROGRAMMING, Year: 2019

Authors: Damiani, Ferruccio; Lienhardt, Michael; Paolini, Luca

A formal model for Multi Software Product Lines

Published in: SCIENCE OF COMPUTER PROGRAMMING, Year: 2019

Authors: Paolini L.; Piccolo M.; Zorzi M.

QPCF: Higher-Order Languages and Quantum Circuits

Published in: JOURNAL OF AUTOMATED REASONING, Year: 2019

Authors: Damiani F.; Lienhardt M.; Paolini L.

Automatic refactoring of delta-oriented SPLs to remove-free form and replace-free form

Published in: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, Year: 2019

Authors: MANZONETTO GIULIO, PAGANI MICHELE, RONCHI DELLA ROCCA SIMONETTA

New Semantical Insights Into Call-by-Value λ-Calculus.

Published in: FUNDAMENTA INFORMATICAE, Year: 2019

Authors: Luca Paolini, Mauro Piccolo, Luca Roversi

On a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensions

Published in: NEW GENERATION COMPUTING, Year: 2018

Authors: A. Bucciarelli, D. Kesner, S. Ronchi Della Rocca

Inhabitation for non-idempotent intersection types

Published in: LOGICAL METHODS IN COMPUTER SCIENCE, Year: 2018

Authors: Paolini, Luca; Piccolo, Mauro; RONCHI DELLA ROCCA, S.

Essential and relational models

Published in: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, Year: 2017

Authors: Berardi, Stefano; de’ Liguoro, Ugo

Non-monotonic Pre-fix Points and Learning

Published in: FUNDAMENTA INFORMATICAE, Year: 2017

Authors: Giulio Guerrieri; Luca Paolini; Simona Ronchi Della Rocca

Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus

Published in: LOGICAL METHODS IN COMPUTER SCIENCE, Year: 2017

Authors: Berardi, Stefano; Steila, Silvia

Ramsey's theorem for pairs and K colors as a sub-classical principle of arithmetic

Published in: JOURNAL OF SYMBOLIC LOGIC, Year: 2017

Authors: Berardi, Stefano; Tatsuta, Makoto

Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proof system

Published in: LECTURE NOTES IN COMPUTER SCIENCE, Year: 2017

Authors: Marco Gaboard; Luca Paolini; Mauro Piccolo

On the reification of semantic linearity

Published in: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, Year: 2016

Authors: Erika De Benedetti, Simona Ronchi Della Rocca

A type assignment for lambda-calculus complete both for FPTIME and strong normalization

Published in: INFORMATION AND COMPUTATION, Year: 2016

Authors: Luca Bernardinello; Felice Cardone; Lucia Pomello

L’eredità di Carl Adam Petri: dagli automi alla comunicazione

Published in: MONDO DIGITALE, Year: 2016

Authors: Alessi, Fabio; Cardone, Felice

Tiered objects

Published in: FUNDAMENTA INFORMATICAE, Year: 2016

Authors: Canavese, D.; Cesena, E.; Ouchary, R.; Pedicini, M.; Roversi, L.

Light combinators for finite fields arithmetic

Published in: SCIENCE OF COMPUTER PROGRAMMING, Year: 2015

Authors: Stefano, Berardi; Silvia, Steila

An intuitionistic version of Ramsey Theorem and its use in Program Termination

Published in: ANNALS OF PURE AND APPLIED LOGIC, Year: 2015

Authors: Berardi, Stefano; Oliva, Paulo; Steila, Silvia

An analysis of the Podelski–Rybalchenko termination theorem via bar recursion

Published in: JOURNAL OF LOGIC AND COMPUTATION, Year: 2015

Authors: Cardone, Felice

Continuity in Semantic Theories of Programming

Published in: HISTORY AND PHILOSOPHY OF LOGIC, Year: 2015

Authors: Simonetta, Ronchi Della Rocca; Virgil, Mogbil

Development on Implicit Computational Complexity (DICE 2013)

Published in: INFORMATION AND COMPUTATION, Year: 2016

Authors: Shkaravska, O.; Ronchi Della Rocca, S.; van Eekelen, M.

Special Issue on Foundational and Practical Aspects of Resource Analysis (FOPARA) 2009 & 2011

Published in: SCIENCE OF COMPUTER PROGRAMMING, Year: 2015

Authors: Luca Paolini; Mauro Piccolo; Luca Roversi

A certified study of a reversible programming language

Published in: 21st International Conference on Types for Proofs and Programs (TYPES 2015), Year: 2018

Authors: Cardone, Felice

Le direzioni della ricerca logica in Italia: Logica e Informatica

Published in: Le direzioni della ricerca logica in Italia, Year: 2015

Authors: Paolini, Luca; Roversi, Luca; Zorzi, Margherita

Quantum programming made easy

Published in: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 

titoloEvento: 2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018

Year: 2019

Authors: Ter Beek M.H.; Damiani F.; Lienhardt M.; Mazzanti F.; Paolini L.

Static analysis of featured transition systems

Published in: ACM International Conference Proceeding Series, 

titoloEvento: 23rd International Systems and Software Product Line Conference, SPLC 2019

Year: 2019

Authors: ter Beek M.H.; Damiani F.; Gnesi S.; Mazzanti F.; Paolini L.

Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints

Published in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 

titoloEvento: 15th International Conference on Integrated Formal Methods, IFM 2019

Year: 2019

Authors: FAGGIAN CLAUDIA, RONCHI DELLA ROCCA SIMONETTA

Lambda Calculus and Probabilistic Computation.

Published in: Logic in Computer science, 

titoloEvento: Logic in Computer Science

Year: 2019

Authors: Lienhardt, Michael; Damiani, Ferruccio; Donetti, Simone; Paolini, Luca

Multi software product lines in the wild

Published in: ACM International Conference Proceeding Series, 

titoloEvento: 12th International Workshop on Variability Modelling of Software-Intensive Systems, VaMoS 2018

Year: 2018

Authors: Matos, Armando B.; Paolini, Luca; Roversi, Luca

The fixed point problem for general and for linear SRL programs is undecidable

Published in: CEUR Workshop Proceedings, 

titoloEvento: 19th Italian Conference on Theoretical Computer Science, ICTCS 2018

Year: 2018

Authors: Berardi, Stefano; Tatsuta, Makoto*

Intuitionistic podelski-rybalchenko theorem and equivalence between inductive definitions and cyclic proofs

Published in: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 

titoloEvento: 14th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2018 Colocated with ETAPS 2018

Year: 2018

Authors: Luca Paolini; Margherita Zorzi

qPCF: A language for quantum circuit computations

Published in: 14th Annual Conference on Theory and Applications of Models of Computation, TAMC 2017, 

titoloEvento: 14th Annual Conference on Theory and Applications of Models of Computation, TAMC 2017

Year: 2017

Authors: Damiani Ferruccio; Michael LIENHARDT; Luca Paolini

A Formal Model for Multi SPLs

Published in: Fundamentals of Software Engineering. FSEN 2017, 

titoloEvento: 7th International Conference on Fundamentals of Software Engineering, FSEN 2017

Year: 2017

Authors: Berardi, Stefano; Tatsuta, Makoto

Equivalence of inductive definitions and cyclic proofs under arithmetic

Published in: Proceedings - Symposium on Logic in Computer Science, 

titoloEvento: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017

Year: 2017

Authors: Paolini, Luca; Piccolo, Mauro; Roversi, Luca

A Class of Reversible Primitive Recursive Functions

Published in: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 

titoloEvento: ICTCS2015

Year: 2016

Authors: ter Beek, Maurice H.; Damiani, Ferruccio; Gnesi, Stefania; Mazzanti, Franco; Paolini, Luca

From Featured Transition Systems to Modal Transition Systems with Variability Constraints

Published in: Software Engineering and Formal Methods, 

titoloEvento: 13th International Conference on Software Engineering and Formal Methods, SEFM 2015

Year: 2015

Authors: BERARDI, Stefano

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness

Published in: 24th EACSL Annual Conference on Computer Science Logic,, 

titoloEvento: CSL 2015

Year: 2015

Authors: Bucciarelli A.; Kesner D.; Ronchi Della Rocca S.

Observability for Pair Pattern Calculi

Published in: Typed Lambda Calculus and Applications, 

titoloEvento: Typed Lambda Calculus and Applications

Year: 2015

Authors: Guerrieri, Giulio; Paolini, Luca; Ronchi Della Rocca, S.

Standardization of a Call-By-Value Lambda-Calculus

Published in: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 

titoloEvento: Typed Lambda Calculus and Applications

Year: 2015

Authors: Cardone, Felice

Computers and the Mechanics of Communication

Published in: Evolving Computability, 

titoloEvento: 11th Conference on Computability in Europe, CiE 2015

Year: 2015