Courses Offered During the 1998-99
Academic Year
Logical Frameworks
(Prof. Benjamin Werner)
Algoritmi Distribuiti (Prof. Alessandro
Panconesi)
Programmazione con Vincoli (Prof. Francesca
Rossi)
Interpretazione Astratta (Dott. Francesco
Ranzato)
Computer Vision (Prof. Marcello Pelillo)
Logical Frameworks (Prof. Benjamin Werner)
Titolo del Corso: Logical Frameworks
docente: Benjamin Werner
email: Benjamin.Werner@inria.fr
durata: 20 ore
sede: Universita' di Bologna
periodo: 6--14 settembre 1999
Principles and practice of proofs in type theory: Coq
Mathematical logic is essentially the study of how mathematical
reasoning can be decomposed up to elementary steps; these steps deal
with the syntax of the expressions and are thus objective. Until a
little more than thirty years ago, the possibility of totaly
formalizing a non-trivial mathematical proof was purely "potential"
because of the size of the formalized proof. This situation changed
with the arrival of the computer and its ability to process large
symbolic expressions. This changed the view one had of the various
mathematical formalisms; one has not only to be exporessive, but also
well-suited for implementation (or in other words, "comfortable").
The version of type theory implemented in Coq has emerged from the
practice of formal proof. The aim of the course is one one hand to
present the formalism and some of its meta-theory, and on the other
hand to use the proof-system through exercices and examples.
Algoritmi Distribuiti (Prof. Alessandro Panconesi)
Titolo del Corso:
Algoritmi Distribuiti
docente: Alessandro Panconesi
email: ale@cs.unibo.it
Durata: 30 ore
sede: Universita' di Bologna
Periodo: dal 3 novembre 1999 al 17 dicembre 1999
In questo corso ci occuperemo principalmente di due questioni:
1. Fault-tolerance: in un sistema distribuito, dove un insieme
di processori indipendenti cooperano per un fine comune, e' possibile
completare correttamente il calcolo a dispetto del malfunzionamento di
alcune componenti?
2. Randomization vs. Determinism: l'uso dell'alea rende gli algoritmi
distribuiti piu' potenti?
Piu' in dettaglio, questo e' una lista di massima degli argomenti:
1. consensus: byzantine failures, crash failures, synchronous networks,
asynchronous networks, failure detectors, randomized protocols
2. wait-freedom
3. self-stabilization
4. distributed graph algorithms
Programmazione con Vincoli (Prof. Francesca Rossi)
Titolo del Corso: Programmazione con Vincoli
docente: Francesca Rossi
email: frossi@math.unipd.it
durata: 20 ore
sede: Padova
periodo: 20-21 Ottobre, 9-10 Novembre
Il corso vuole fornire i concetti fondamentali e le tecniche per
risolvere e programmare con i vincoli. Verranno prima presentate le
tecniche per manipolare varie classi di vincoli, e poi verra' definita
la programmazione logica con vincoli, anche usando dei sistemi reali
(CLP(R), clp(fd), ...).
Programma:
-- introduzione
-- problemi di vincoli
-- alcuni risolutori, semplificatori, ed ottimizzatori di vincoli
-- vincoli a dominio finito: alcuni risolutori incompleti
(consistenza sui nodi, sugli archi, e sui limiti) e algoritmi di ricerca
-- programmazione logica con vincoli: clausole e alberi di derivazione
-- programmare con vincoli: alcuni esempi e tecniche
Il libro di riferimento e' ''Programming with constraints: an
introduction'', di Marriott e Stuckey, MIT Press, 1998.
Interpretazione Astratta (Dott. Francesco Ranzato)
Titolo del Corso: Interpretazione Astratta
docente: Francesco Ranzato
email: franz@math.unipd,it
durata: 20 ore
sede: Padova
orario: 18, 19, 25, 28, 29 Ottobre 1999, ore 11-13 e 14:30-16:30
Schema di Programma:
- Principi di analisi statica dei programmi
- Interpretazione astratta come tecnica di analisi statica
- Fondamenti di interpretazione astratta
- Teoria dei domini astratti
* Reticoli di domini astratti
* Semantiche ottimali e/o complete indotte da domini astratti
* Operatori di trasformazione su domini astratti
* Esempi in programmazione funzionale e logica
- Temi e problemi di ricerca
Computer Vision (Prof. Marcello Pelillo)
Titolo del Corso: Computer vision
docente: Marcello Pelillo
email: pelillo@dsi.unive.it
durata: 20 ore
sede: Universita' di Venezia
orario: 4, 6, 8, 11, 13 Ottobre 1999, ore 15--19.
contenuto:
The objective of the course is to provide a gentle introduction to the
field of machine visual perception. We will discuss the problems
encountered when equipping a machine with the sense of sight, and
present the state-of-the-art techniques developed to solve them.
Special emphasis will be given to models and algorithms inspired by
the structure of biological visual systems.
1. Introduction
2. The eye and the visual cortex
3. Image formation
4. Edge/curve detection and grouping
5. Texture
6. Stereo
7. Object recognition and classification
References
[1] V. S. Nalwa, "A guided tour of computer vision". Addison-Wesley, 1993.
[2] S. Ullman, "High-level vision". MIT Press, 1996.
|
|
