Courses Offered During the 1995-96
Academic Year
Course Details (in Italian and
English)
Titolo del Corso: Abstract Interpretation
Docente: Gilberto File`
Responsabile: Gilberto File` (gilberto@zenone.math.unipd.it)
Periodo: 4 Marzo -- 5 Giugno 1996
Orario: lunedi, martedi e mercoledi 11:20--12:10, Aula P50
Dipartimento di Matematica, Via Belzoni 7 Padova.
Scopo del Corso
Lo scopo del corso \`e introdurre gli studenti alla teoria
dell'interpretazione astratta introdotta nel 1977 da P. e R. Cousot e
fondata sulla nozione di connessione di Galois tra
reticoli. L'interpretazione astratta \`e una metodologia generale per
il disegno di tecniche che inferiscano automaticamente propriet\`a di
programmi. La metodologia \`e generale sia perch\`e si applica a
diversi paradigmi di programmazione (imperativo, funzionale, logico,
constraint ecc.) e sia perch\`e viene usata per inferire moltissimi
tipi di informazioni sui programmi. Informazioni che variano da
propriet\`a di correttezza fino ad informazioni sui valori calcolati
che permettono al compilatore di produrre codice ottimizzato.
La teoria verr\`a illustrata con esempi basati su semantiche di tipo
diverso, in particolare denotazionale ed operazionale di linguaggi di
complessit\`a crescente. Il corso quindi introduce allo studio della
semantica dei linguaggi di Programmazione con un'ottica
particolarmente pragmatica e comparativa ed arriva gradualmente ad
esaminare anche problemi di ricerca recentissimi nell'ambito del
disegno di domini astratti.
Programma
- Esempi di Interpretazione astratta:
- Ottimizzazione di un programma imperativo;
- Semantiche standard e non standard delle grammatiche libere da contesto;
- La teoria dell'interpretazione astratta: reticoli completi,
connessioni di Galois e operatori di upper closures;
- Gli esempi rivisitati;
- Semantiche standard e non standard della programmazione logica;
- Domini astratti per l'ottimizzazione della programmazione logica:
Pos, Def e Sharing;
- Disegno di domini astratti: prodotto ridotto, complementazione,
raffinamenti e loro inversione;
- Applicazioni;
Titolo del Corso: Introduzione agli Algoritmi Paralleli
Docente: Andrea Pietracaprina (andrea@artemide.dei.unipd.it)
Responsabile: Gilberto File` (gilberto@zenone.math.unipd.it)
Periodo: 4 Marzo -- 5 Giugno 1996
Orario: Lunedi, Martedi e Mercoledi 9:40--11:10 Aula P20 (3rd floor)
Dipartimento di Matematica, Via Belzoni 7 Padova
Contenuti
Il corso intende fornire gli elementi di base necessari per il
progetto e l'analisi di algoritmi paralleli. Il corso \`e
concettualmente suddiviso in quattro parti. Nella prima parte si
considera il modello shared memory (PRAM) illustrando le principali
tecniche e algoritmi noti in letteratura. La seconda parte \`e
dedicata al calcolo parallelo su reti e descrive le principali
architetture congiuntamente ad algoritmi notevoli e tecniche di
routing. Nella terza parte si introducono alcuni modelli
computazionali recentemente proposti in letteratura, discutendone la
loro validit\`a e il loro utilizzo per lo sviluppo di
algoritmi. Infine, la quarta parte si concentra su aspetti pi\`u
pratici del calcolo parallelo presentando le caratteristiche di alcune
macchine attualmente esistenti. Inoltre sono previste delle prove di
laboratorio dove si utilizzer\`a il sistema PVM (Parallel Virtual
Machine) per l'implementazione di algoritmi paralleli su una rete di
PC. La struttura dettagliata del corso \`e la seguente.
- Introduzione al calcolo parallelo.
- Il modello PRAM (Shared Memory):
- Tecniche algoritmiche di Base: Prefix, Pointer Jumping,
Divide-and-Conquer, Pipelining, Accelerated Cascading.
- Algoritmi Fondamentali: List Ranking, Searching, Merging,
Sorting, Algoritmi su Grafi.
- Cenni di Complessit\`a: Lower bound, P-Completeness
- Architetture parallele (Distributed Memory):
- Tecniche di Routing.
- Algoritmi fondamentali (Prefix, Sorting e FFT) su
array, mesh-of-trees e reti ipercubiche.
- Grafi a espansione, Concentratori e Superconcentratori (cenni).
- BSP e LogP (Bridging Models): Prefix, Broadcast, Sorting
e Algoritmi su Matrici.
- Macchine parallele esistenti.
- Sistema PVM.
Requisiti per superare il corso
Durante il corso verranno assegnati alcuni homework da svolgere
individualmente per assimilare il materiale proposto. Si richiede
inoltre che gli studenti si suddividano in gruppi (idealmente due/tre
studenti per gruppo) a ciascuno\ dei quali verr\`a assegnato un
progetto da svolgere utilizzando il sistema PVM sulla rete di PC messa
a disposizione dal Dipartimento. Inoltre, gli studenti del corso di
laurea dovranno sostenere un esame finale orale, mentre gli studenti
di dottorato dovranno presentare una tesina su un argomento attinente
al corso (alcuni argomenti verranno suggeriti durante il corso). Il
giudizio finale sar\`a basato 30\% sugli homework, 30\% sul progetto e
il restante 40\% sulla prova finale.
Materiale Bibliografico
Per la parte riguardante gli algoritmi PRAM si utilizzer\`a il libro
di J\`aJ\`a \cite{Jaja92}, mentre per quella riguardante le
architetture si utilizzer\`a il libro di Leighton
\cite{leighton92-1}. Entrambi i libri sono disponibili nella
biblioteca del Dipartimento di Matematica e in quella del Dipartimento
di Elettronica e Informatica. Il materiale relativo agli altri
argomenti verr\`a distribuito di volta in volta.
ibitem[J{\'a}J92]{Jaja92}
J.~J{\'a}J{\'a}.
ewblock {\em An Introduction to Parallel Algorithms}.
ewblock Addison Wesley, Reading MA, 1992.
ibitem[Lei92]{leighton92-1}
F.T. Leighton.
ewblock {\em Introduction to Parallel Algorithms and Architectures: Arrays
$ullet$ Trees $ullet$ Hypercubes}.
ewblock Morgan Kaufmann, San Mateo, CA, 1992.
Titolo del Corso: Graph Theory
Docente: Ajai Kapoor
Responsabile: Conforti (conforti@hilbert.math.unipd.it)
Periodo: 12 Marzo 1996 -- 4 Aprile 1996
Orario: martedi, mercoledi 14:40-17:30, Aula P160
Dipartimento di Matematica, via Belzoni 7, Padova
Course Outline
This is an introductory course on Graph Theory. The text of Bondy and
Murty "Graph Theory with Applications" will provide the main source
for the course. The topics covered will include Eulerian Tours,
Hamilton Cycles, Matchings, Edge colorings, Vertex coloring,
Max. cliques, Flows, shortest paths and the relationships between
these problems.
Some of the problems listed are "well understood" in the sense that
there exist "good characterizations" for them and not surprisingly
there exist polynomial time algorithms to solve the problems. Others
are harder and not surprisingly are NP-hard. This interplay between
mathematical "good characterization" and complexity theory will be a
theme for the course.
There will be some homework assignments and one take home exam at the
end of the course.
Titolo del Corso: Robust Distributed Computing
Docente: Kenneth P. Birman, Dept. of Computer Science, Cornell University
Responsabile: Ozalp Babaoglu
Periodo: 20 Maggio -- 24 Maggio 1996
Orario:
20/5 Seminario 2 ore 10-12, 14-16
21/5 Seminario 1 ore 10-12, 14-16
22/5 Seminario 2 ore 10-12, 14-16
23/5 Seminario 1 ore 10-12, 14-16
24/5 Seminario 1 ore 10-12, 14-16
del Dipartimento di Matematica, Bologna
Course Description
As distributed computing systems have entered into wider use, they
have also been applied in increasingly "critical" environments, where
a loss of availability, inconsistency, poor performance, or a security
breakdown may have very serious consequences. The World Wide Web is
accelerating the trend by presenting potential computer users with a
very simple (and in many ways simplistic) model of how their
enterprises can exploit distributed computing. Today, it is no
exageration to say that if there is any way to move an application
into a distributed setting, someone is trying to do so. More and
more, the financial security, health and safety of our society will
depend on the ability of these technologies to support the resulting
critical uses.
This course will review the major distributed computing technologies,
including the Web, with a strong focus on reliability issues. Our
investigation will motivate the use of a variety of techniques for
replicating critical data and sharing work in distributed settings,
and we will study these in some detail. At the same time, we will
review work on distributed systems security, transactional management
of persistent data, the use of time in distributed systems, system
management, and the various models of consistency that have been
proposed.
Although broad in coverage, this course will not be extremely "deep"
in a technical sense. We will try to be as rigorous but won't have
time to dig into the very subtle issues that arise in many of the
topics upon which the course touches. The level is thus very suitable
for a graduate student who will pursue a career in the commercial
sector, or as an introduction to the area for a graduate student who
may than want to take other courses that treat some of the same topics
in much greater detail. Our treatment will be thorough enough to give
the participant a good understanding of the practical tools currently
available for making distributed systems "robust".
This course closely parallels a new textbook, preprints of which will
be available to students. Each lecture will include specific
references to the sections of the textbook that the student can read
to find additional detail. Because of the short amount of time
available, there will be no required homework, programming exercises,
or exams.
Titolo del Corso: Algoritmi Randomizzati
Docente: Giuseppe F. Italiano (italiano@dsi.unive.it)
Responsabile: Giuseppe F. Italiano
Sede: Venezia (Mestre)
Orario: 10:00 -- 14:00 (AULA A)
10/6 (Lun)
17/6 (Lun)
24/6 (Lun)
1/7 (Lun)
Contenuto
La prima parte del corso presentera' fondamenti di teoria della
probabilita' e analisi probabilistiche che ricorrono in applicazioni
algoritmiche. La seconda parte si concentrera' su alcune delle aree di
applicazione degli algoritmi randomizzati, in particolare: strutture
dati, algoritmi su grafi, algoritmi paralleli e distribuiti. Si
assume una familiarieta' con l'analisi di algoritmi e la teoria della
probabilita', come puo' essere acquisita nei corsi di laurea con
indirizzi informatici.
Titolo del Corso: Reti Neurali
Docente: Marcello Pelillo (pelillo@dsi.unive.it)
Responsabile: Giuseppe F. Italiano
Sede: Venezia (Mestre)
Orario: 14:00-18:00 (AULA A)
10/6 (Lun)
17/6 (Lun)
24/6 (Lun)
25/6 (Mar)
Titolo del Corso: Linear Logic for the Computer Scientist
Docente: Maurizio Martelli (DISI, Univ. di Genova)
Responsabile: Gilberto File` (gilberto@zenone.math.unipd.it)
Periodo: 8--10 Luglio 1996
Sede: Dipartimento di Matematica, Via Belzoni 7 Padova
Orario:
Lun. 8: ore 15:00 -- 18:00 aula P80
Mart. 9: ore 15:00 -- 18:00 aula da decidere
Merc. 10: ore 11:00 -- 13:00 aula da decidere
Contenuti
Linear Logic (LL) was developed by J.Y. Girard as part of his
investigation into the semantics of intuitionistic logic. LL has
taken on, after that, a life of its own and many conferences and
papers have been devoted to it. Part of this success is due to the
fact that central notion in LL is the "state" (more than the notion of
"truth" as in classical logic) and it is sometimes described as being
"resource sensitive" because it is capable of modeling process states,
events and resources. This aspects of LL makes it one of the most
interesting proposals for giving to the notion of computation an
overall logical setting, as witnessed by the work of Miller on Forum,
a specification language based on Higher Order Linear Logic.
In this brief course I would like to present some of the ideas lying
behind LL that I found particularly stimulating as a person working in
programming languages and their semantics. It is not a specialized
course on LL for Logic experts, but a presentation of LL by a computer
scientist that, exposed to it, will try to communicate to the audience
the new insight that this piece of work in logic gives to the field of
computer science and to programming.
Titolo del Corso: Proof Theory and Logic Programming
Docente: Dale Miller (University of Pennsylvania)
Responsabile: Gilberto File` (gilberto@zenone.math.unipd.it)
Periodo: 15--19 Luglio 1996
Sede: Dipartimento di Matematica, Via Belzoni 7 Padova
Orario: Lun 15 -- Ven 19: ore 11:00 -- 13:00 aula P80
Contenuti
Goal-directed proof search can be used as a guide in
designing logic programming languages. After formalizing a notion of
goal-directed proof search in sequent calculus, we present several
examples of logic programming languages, including hereditary Harrop
formulas (the foundation of lambda Prolog) and a new system called
Forum. Forum is a particular presentation of all of linear logic in
which goal-directed proof search is complete. It modularly extends
Prolog, lambda Prolog, and the LO system of Andreoli and Pareschi. We
shall present several examples of specifications written in these
languages and make use of meta-theoretic properties of logic to
analyze them. In particular, we shall describe how these logics make
it possible to specify computations using abstractions and
concurrency.
OUTLINE
-Lecture 1 (15 July 1996) Linear Logic and Sequent Calculus
-Introduction and overview to course
-Sequent calculus
-Permutations of linear logic connectives
-Show how left and right rules match up via cut elimination
-The cut-elimination theorem for linear logic
-Present proof rules with bounded and unbounded contexts
-Proof systems for intuitionistic and classical logic
-Lecture 2 (16 July 1996) Horn clauses
-Sequent calculus presentation for first-order quantification
-Permutations and cut-elimination for quantifiers
-Goal-directed proof search in a single-conclusion setting
-Various presentations of propositional Horn clauses
-Add quantification to Horn clauses
-Proof theory for first-order Horn clauses
-Similarity of par, -o encoding with SLD-resolution
-Lecture 3 (17 July 1996) Hereditary Harrop Formulas
-Definition of the order of formulas
-First-order hereditary Harrop formulas
-Abstract data types
-Program equivalence
-Lecture 4 (18 July 1996) Lolli and Intuitionistic Linear Logic
-Discuss general design issues explicitly
-Presentations of Lolli
-Definable logical connectives
-Kripke Model result for hereditary Harrop formulas and for Lolli
-Input-Output proof system for splitting contexts
-Multiset rewriting
-Lecture 5 (19 July 1996) Forum and all of Linear Logic
-LO as a logic programming language
-Design goal: put Lolli and LO together
-Andreoli's presentation of focused proofs
-State uniformity for full sequent calculus
-Examples: concurrency and imperative programming features
-Meta-level specifications of sequent calculus
|
|
