Linguaggi di programmazione

Cluster di dipartimento

Informatica teorica

Sito web del gruppo

http://clp.dimi.uniud.it

Descrizione

Il gruppo si colloca all’interno dell’area dei linguaggi di programmazione. La missione del gruppo è quella di sviluppare sia nuove implementazioni dei linguaggi che strumenti automatici di supporto alla programmazione in tutte le sue fasi (quali progetto, scrittura, analisi, debugging, verifica e certificazione).

Il gruppo si è occupato ampiamente di linguaggi dichiarativi (specialmente linguaggi funzionali, logici con vincoli e logico-funzionali) sviluppando

nuove implementazioni di risolutori di vincoli;
supporto alla programmazione concorrente (con estensioni per la programmazione su memoria transazionale in linguaggi funzionali)

nonché teorie e strumenti/prototipi di supporto

al progetto di sistemi software (con strumenti di assistenza alla modellazione UML);
al debugging del software (con strumenti per rilevare la non-conformità del codice rispetto alle specifiche);
all’analisi del prodotto (con strumenti per sintetizzare automaticamente determinate proprietà);
alla verifica dei requisiti (con strumenti per validare automaticamente determinate proprietà) e
alla certificazione di proprietà (con strumenti per assistere l’utente nella dimostrazione automatica di proprietà complesse).

Il gruppo ha collaborazioni internazionali con diverse sedi, principalmente con la New Mexico State University, l’Universitat Politècnica de València, l’INRIA Sophia Antipolis, la IT University (Copenhagen) e la University of Southern Denmark (Odense); oltre a diverse collaborazioni nazionali consolidate.

Linee di ricerca

Programmazione concorrente su software transactional memory.
Verifica e Diagnosi Astratta (strumenti per la verifica e il debugging basati sull’interpretazione astratta) per linguaggi logici con vincoli temporizzati.
Sintesi Automatica di Specifiche di alto livello per Haskell e Curry.
Sviluppo di strumenti per la manipolazione automatica di linguaggi dichiarativi basati sulla semantica al fine di diminuire lo sforzo della fase di testing, sia in termini di tempo che di costi.
Verifica Automatica di Diagrammi UML con vincoli OCL.
Aspetti fondazionali, implementazione di risolutori e applicazioni in diversi contesti applicativi.
Studio di teorie minimali degli insiemi/multi-insiemi adatte ad essere inserite in linguaggi logici con vincoli, nonché studio dei limiti intrinsici nell'uso della negazione costruttiva, e dei limiti intrinsici nelle proposte di coinductive logic programming
Tecniche ibride per il calcolo di un modello stabile sviluppo di risolutori per problemi di soddisfacibilità (SAT), di calcolo del modello stabile (ASP), e di risoluzione di vincoli (CP) su domini finiti che sfruttano il parallelismo delle schede video programmmabili (GPGPU)
Progetto dell'allocazione ottima delle sirene dell'acqua alta di Venezia, affrontati alcuni problemi di area bioinformatica, realizzato configuratori di prodotto, ottimizzatori energetici, e generatori di codici di correzione per impianti industriali
Proprietà dei pattern-matching automata che danno un modello della Logica Combinatoria Lineare
Estensioni del lambda-calcolo con discipline di tipi dotati di un’intersezione non simmetrica, i cui tipi principali permettono di derivare la semantica della Geometria delle Interazioni per la logica combinatoria lineare in modo diretto.
Implementazione di ambienti interattivi che possano assistere gli utilizzatori di metodi logico-formali per la certificazione e lo sviluppo di software.
Teorie soggiacenti ai Logical Frameworks sono dei linguaggi di programmazione fortemente tipati che combinano due modalità computazionali tra loro duali: la riduzione e il pattern-matching.
Teorie fondazionali in logica costruttiva, che hanno recentemente ricevuto molta attenzione anche nel contesto della Geometria Algebrica, dando origine alle Homotopy Type Theory.