Programming Languages

Cluster

Theoretical Computer Science

Group's website

http://clp.dimi.uniud.it

Description

The group operates within the area of the programming languages. The group's mission is to develop both new implementations of the languages and automatic tools supporting programming in all its stages (such as design, writing, analysis, debugging, verification and certification).

The group dealt extensively with declarative languages (especially with functional languages, constraint logic languages and functional logic languages), thereby developing:

new implementations of constraint solvers;
support for concurrent programming (with programming extensions on transactional memory in functional languages;

as well as new theories and support tools/prototypes for:

designing software systems (with tools assisting UML modelling);
software debugging (with tools for detecting non-compliance with specifications in coding);
product analysis (by tools for automatically synthesising certain properties);
verification of requirements (by tools for automatically validating certain properties), and
certification of properties (by tools for assisting the user in the automatic demonstration of complex properties).

The group has ongoing international collaborations with several partners, mainly with the New Mexico State University, the Universitat Politècnica de València, the INRIA Sophia Antipolis, the IT University (Copenhagen) and the University of Southern Denmark (Odense); as well as several well-established national collaborations.

Research subjects

Concurrent programming on software transactional memory.
Abstract Verification and Diagnosis for logic languages with time constraints.
Automated Synthesis of high-level specifications for Haskell and Curry.
Development of tools for automated manipulation of declarative languages based on semantics
Automated Verification of UML diagrams with OCL constraints.
Foundational aspects, implementation of solvers and applications in several application contexts.
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.