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 (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.
Esimene seminar toimub N 13.9.
| Aeg | Teema | Ettekandja |
|---|---|---|
| N 6.9. | Kübi 52. aastapäeva aktus | |
| K 12.9. kl 14 |
Formalization of graph theory in HOL: the Maxflow-Mincut theorem | N Veltri (U Firenze) |
| N 13.9. | Verification of redecoration for infinite triangular matrices in Coq | C Picard (U Toulouse 3) |
| N 20.9. | Verification of static class invariants in object-oriented programs R. Leino, P. Müller, Modular verification of static class invariants, Proc. FM 2005 |
Boriss Š |
| N-P 27.-30.9. | Teooriapäevad Lilastes | |
| N 4.10. | Concrete process categories | Wolfgang J |
| N 18.10. | A short walk into randomness | Silvio C |
| R 23.11. kl 14 |
Overview of formalized developments context-free grammars | Denis F |
| T 27.11. kl 11 |
Automatic code generation in certified system development: a model-driven specification and verification approach | A Dieumegard (INP Toulouse) |
| N 29.11. | Stop when you are almost full: adventures in constructive termination | D Vytiniotis (MSR Cambridge) |
| T 4.12. kl 11 |
System L syntax for sequent calculi | P-L Curien (U. Paris 7) |
| N 6.12. | A classical lozenge | P-L Curien (U. Paris 7) |
| N 20.12. kl 11 |
Towards more refined notions of computation: the global state example | D Ahman (U of Edinburgh) |
| N 3.1. | Certified normalization of CFGs | Denis F |
| T 15.1 kl 11 |
Deductive program verification with Why3 | J-C Filliatre (U Paris Sud 11) |
| N 31.1. | Coinductive big-step semantics for concurrency | Tarmo U |
| R-P 1.-3.2. | Teooriapäevad Otepääl | |
| T 5.2. kl 11 |
Introduction to restriction categories | R Cockett (U of Calgary) |
| N 7.2. | Overview of formalized developments for regexps | Denis F |
| T 12.2. kl 11 |
Introduction to restriction categories | R Cockett (U of Calgary) |
| N 14.2. | Introduction to restriction categories | R Cockett (U of Calgary) |
| T 19.2. kl 11 |
Introduction to restriction categories | R Cockett (U of Calgary) |
| N 21.2. | Introduction to restriction categories | R Cockett (U of Calgary) |
| T 26.2. kl 14 |
Eesti Vabariigi 95. aastapäeva aktus | |
| N 28.2. | Dynamic software updating G. Stoyle, M. Hicks, G. Bierman, P. Sewell, I. Neamtiu, Mutatis mutandis: safe and predictable dynamic software updating, TOPLAS 2007 |
Elmo T |
| R 1.3. kl 14 |
Dynamic software updating (ctd) | Elmo T |
| P-R 3.-8.3. | EWSCS 2013 | |
| N 11.4. | Extending dynamic logic for reasoning about intermediate states | Boriss Š |
| N 18.4. | Update monads: cointerpreting directed containers | Tarmo U |
| N 16.5. | Timely dynamic updating of multithreaded programs M. Hicks, I. Neamtiu. Safe and timely updates to multi-threaded programs, PLDI 2009 |
Elmo T |
| N 30.5. | On the axiom of univalence Talks by Steve Awodey at TYPES 2013 |
Niccolò V |
| E 3.6. kl 14 |
Correctness-by-construction in stringology | B Watson (Stellenbosch U) |
| T 18.6. kl 14 |
Categorical semantics for linear logic | Wolfgang J |
| N 20.6. | Combining linear and temporal logic | Wolfgang J |
| N 27.6. | Techniques for proof compression | B Woltzenlogel Paleo (TU Wien) |
| N 4.7. | Copatterns: programming infinite structures by observations | A Abel (LMU München) |