Arvutiteaduse teooriaseminar (sügis 2009-kevad 2010)
Arvutiteaduse teooriaseminar on Küberneetika Instituudi loogika ja semantika rühma teadlaste
lahtine seminar, kuhu on oodatud kõik huvilised, sh
kraadiõppurid, IT-firmade töötajad jne, ning kus
eesmärgiks on sundimatus õhkkonnas mõõdukas
tempos tutvuda uute suundadega, aga ka klassikaga teoreetilise
arvutiteaduse alalt, peamiselt programmeerimisteooriast.
Aktiivse osalemise eest võivad kraadiõppurid saada
punktid aines TTÜ arvutiteaduse
instituudi aines
ITT9070/71 Arvutiteaduse teooriaseminar (5.0 AP, 8.0 EAP).
Jooksev info seminari kohta levib listis tsem(at)lists.ioc.ee,
mille tellimiseks saata tuleb saata käsk subscribe tsem
Eesnimi Perenimi aadressile sympa(at)lists.ioc.ee.
Aeg: üldjuhul neljapäevad kl 14-15.30.
Koht: Küberneetika Maja (Akadeemia tee 21), B-korpus,
ruum B101.
Sügissemestri esimene teooriaseminar toimub T 27.10.2009.
Ajakava
Aeg | Teema | Ettekandja |
N 3.9. |
Kübi 49. aastapäev |
|
N 17.9. |
TTÜ 91. aastapäev |
|
R-P 2.-4.10. |
Teooriapäevad Mäetagusel |
|
T 27.10. kl 14 |
Universes of data |
P Morris (U of Nottingham) |
N 29.10. |
Eraldamisloogikast
J C Reynolds, Separation logic, LICS 2002 |
A Saar |
N 5.11. |
Using grammatical aspects in language engineering |
A Breslav (U of Tartu/SPbSU ITMO) |
N 12.11. |
Program repair as sound optimization of broken programs |
Tarmo U |
N 19.11. |
Type theory should eat category theory for lunch and have monads for
breakfast |
James C |
N 26.11. |
Owicki-Griesi paralleelprogrammide loogikast
S Owicki, D Gries, Verifying properties of parallel programs: an axiomatic approach, Commun of ACM, 1976 |
A Saar |
K 2.12. kl 14 |
Refinement of fault-tolerant control systems in the B method |
E Troubitsyna (Åbo Akademi) |
N 3.12. kl 13 |
Type systems for pointer and live stack-heap analyses and program
optimization and correction |
M El-Zawawy |
T 8.12. kl 14 |
A Coq formalization of an analysis and optimization of While |
G Fedyukovich |
N 10.12. |
Monads and adjunctions on categories and functors |
James C |
K 16.12. kl 14 |
Solving extended regular constraints symbolically |
M Veanes (Microsoft Research) |
T 22.12. kl 13 |
Owicki-Griesi loogika Stirlingi variandist
C Stirling, A generalization of Owicki-Gries's Hoare logic for a concurrent While language, Theor Comput Sci, 1998 |
A Saar |
N 7.1. kl 14 |
Domain-specific embedded languages using dependent
types and partial evaluation |
E Brady (U of St Andrews) |
N 7.1. kl 16 |
Time flies like an applicative functor |
C McBride (U of Strathclyde) |
N 21.1. |
Securing class initialization |
Keiko N |
N 4.2. |
From reactions to observations: the directed bigraphical model |
D Grohmann (U di Udine) |
R-P 5.-7.2. |
Teooriapäevad Andul (semantika) |
|
N 11.2. |
A categorical model of the fusion calculus |
M Miculan (U di Udine) |
P-R 28.2-5.3. |
15. Eesti Arvutiteaduse Talvekool |
|
T 9.3. kl 14 |
Automated fault detection for Autosub6000:
What we've achieved in a year |
Juhan E (U of Birmingham) |
N 11.3. |
Lõtvadest mälumudelitest
F Zappa Nardelli et al. Relaxed memory models must be rigorous. Proc of (EC)2 '09, 2009 |
Andri S |
N 8.4. kl 16 |
Lazy modules |
Keiko N |
R 9.4. kl 14 |
Proof search and counter-model construction for bi-intuitionistic propositional logic |
L Pinto (U do Minho) |
N 6.5. |
Verifying simple imperative programs with the Coq proof assistant |
A Toom |
N 13.5. kl 16 |
Resumptions, weak bisimilarity and big-step semantics for interactive input-output:
an exercise in mixed induction-coinduction |
Tarmo U |
N 20.5. |
A security types preserving compiler in Haskell |
A Pardo (U de la República) |
N 27.5. |
Mixing induction and coinduction in Agda |
T Altenkirch (U of Nottingham) |
N 3.6. |
Some minimality results on biresidual and biseparable automata |
Hellis T |
R-P 11.-13.6. |
Teooriapäevad Elvas (krüptoloogia) |
|
N 19.8. |
Termination for concurrent processes |
R Demangeon |
Varasemad aastad
Tarmo Uustalu
Viimane uuendus 16.8.2010