Linguaggi di programmazione
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.
Settori ERC
- PE6_3 Software engineering, programming languages and systems
- PE6_4 Theoretical computer science, formal methods, automata
Etichette libere
- Linguaggi dichiarativi
- Linguaggi funzionali
- Linguaggi logici con vincoli
- Linguaggi logico-funzionali
- Programmazione con vincoli
- Linguaggi concorrenti
- Semantica formale dei linguaggi di programmazione
- Interpretazione astratta
Componenti
In base alla circolare d'Amministrazione n. 33/1998 si responsabilizzano le persone in indirizzo a verificare la correttezza dei dati inseriti e ad effettuare le dovute comunicazioni di variazione alla Direzione Risorse Umane e Affari generali (DARU) per assicurare il costante aggiornamento dei dati nel tempo, trasmettendo (esclusivamente per posta elettronica) l'esito delle verifiche effettuate agli indirizzi di seguito riportati:
- per il personale tecnico amministrativo: ta.tempoindeterminato@uniud.it
- per il personale docente: docenti@uniud.it