A lungo le macchine di calcolosono state realizzate e concepite in relazione a meccaniche di calcolo analogiche, non digitali. L'idea di calcolo digitale è relativamente recente e origina dalla obbiettivo di identificare la nozione di algoritmo, ossia l'essenza delle procedure di calcolo introdotte dall'umanità nello sviluppo della matematica.

Tra le proprietà comuni ai passi compiuti negli algoritmi ricordiamo: la loro non ambiguità, la finitezza della loro azione, la terminazione in tempo finito di ogni passo, l’effettività dell'esecuzione. La formalizzazione di questi passi avanzata da Turing nel 1936 identifica la macchina digitale ed ha generato una vivida competizione tra macchine digitali e analogiche per la computazione automatica durata qualche decennio. Negli anni 60 il modello di calcolo digitale ha preso il sopravvento, in virtù della possibilità di eseguire tutti i procedimenti di calcolo concepiti in millenni di matematica, della naturalezza scientifica dell'approccio e della solidità teorica che ha contraddistinto la soluzione. Tuttavia, oggi molti modelli computazionali alternativi stanno sfidando questa egemonia in modo decisivo: quantistici, reversibili, probabilistici, ma anche analogica.

I nostri interessi vertono prevalentemente, non solo, allo studio dei fondamenti teorici e delle implementazioni concrete dei modelli matematici del calcolo in termini logici, categoriali, combinatori, algebrici, analitici. Una aspetto fondante dell'approccio che ci interessa è l'individuazione del classico computer digitale come nucleo su cui sviluppare, con soluzione di continuità, le computazioni innovative sopra citate. Questo approccio è foriero di soluzioni ibride volte a facilitare il passaggio e l'uso pratico dei computer emergenti.

Infatti, a dispetto dei progressi tecnologici che la pongono come una disciplina chiave nell'ambito della società moderna, l'informatica, dal punto di vista scientifico, è ancora immatura. Basti pensare alla difficoltà di certificare la correttezza, sia funzionale, sia in termini di risorse utilizzate, di composizioni di moduli software eseguiti in ambito distribuito. Grazie al nostro retroterra ed alle nostre inclinazioni scientifiche miriamo anche a contribuire ad un avanzamento della conoscenza fondazionale dell'informatica, grazie anche ad un substrato di collaborazioni ed attività passate ed attive.

Il nostro metodo favorito è analizzare gli aspetti matematici di astrazioni che hanno acquistato una rilevanza centrale nella teoria della computazione, anche in seguito alla nascita di nuovi modelli basati sulla fisica dei processi di calcolo (calcolo quantistico o reversibile), i quali hanno anche condotto alla necessità di guardare con una nuova consapevolezza problematiche classiche come il calcolo distribuito ed asincrono. In generale, si tratta di problemi di interazione tra processi nello spazio e nel tempo, dove spazio e tempo sono a loro volta ripensati in una chiave computazionale. Lavoriamo con una visione che pone la costruzione di teorie che aiutino a spiegare il concetto di “calcolo”, portandolo al centro dell'attività di ricerca. Siamo focalizzati sugli aspetti fondazionali dei concetti tecnici che studiamo, piuttosto che alla soluzione di singoli problemi. La convinzione è che l’informatica, come “scienza del calcolo”, abbia un'assoluta necessità di una rielaborazione delle sue basi sia matematiche sia, in un senso ampio, filosofiche.

• (2023-oggi) Viviana Bono. PRIN - ClasstAIs, con Tor Vergata, Sapienza e Psicologia Unito.

• (2023-oggi) Luca Roversi. Progetto "HPC-KTT - HPC Key Technologies and Tools national lab"  
  
  
• (2023-oggi) Luca Roversi, Luca Paolini. Progetto Indam.
  Titolo. "Computazione, infinito e reversibilità"
  Partecipanti esterni
  (Verona) Peter Schuster, Margherita Zorzi (PI), Giulio Fellin
• (2016-oggi) (Berardi, de' Liguoro) The European research network on types for programming and verification (EUTypes)
• (2014-oggi) Cardone, Paolini, Roversi membri del "Center for Logic, Language, and Cognition",
• (2013-2015)"Linear Techniques For The Analysis Of Languages (LINTEL) TO_Call1_2012_0085 con responsabile Paolini,
• (2012-2015)PRIN "Metodi Logici per il trattamento dell'informazione" con coordinatore locale Berardi,
• (2012-2014) Royal Society’s joint project  in collaborazione con la University of Bath e coordinatore locale Roversi, "Sharing and Sequentiality in Proof Systems with Locality"
• (2010-2012) INRIA’s equipe associeé " con coordinatrice locale Ronchi Della Rocca, "Contrôle des Ressources par Interprétations Sémantiques et Théorie de la démonstration Linéaire (CRISTAL)
• (2010-2012) CNRS Project International de Coopération Scientifique "Logique Lineaire et applications (PICS)" con coordinatrice locale Ronchi Della Rocca,
• (2007-2009) PRIN "Control and Certification of Resources" con coordinatrice nazionale Ronchi Della Rocca,
• MCTAAP 2008H49TEH_002 (2010-2012) con coordinatore locale Berardi,
• (2004-2007) EU 6th framework programme con coordinatore locale Berardi,
• (2004-2006) PRIN "Logical Foundations of Abstract Programming Languages (FOLLIA)" con coordinatrice nazionale Ronchi Della Rocca,
• (2000-2006) MCTAAP projects, con coordinatore locale Berardi,
• (2002-2004) PRIN "From Proofs to Computation Through Linear Logic (PROTOCOLLO)" con coordinatrice nazionale Ronchi Della Rocca.

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