Logic and Semantics at IoC

Who We Are

We are a research group in the Software Department of the Institute of Cybernetics (IoC), the leading computer science research institution of Estonia. We pursue "Theory B": logic, semantics and theory of programming.

The current members of the logic and semantics group are:

• Tarmo Uustalu, group leader
• Silvio Capobianco
• James Chapman
• Denis Firsov
• Wolfgang Jeltsch
• Keiko Nakata
• Andri Saar
• Boriss Šelajev
• Elmo Todurov
• Andres Toom (main position at IB Krates)

We collaborate with Varmo Vene of the University of Tartu and Peeter Laud of Cybernetica. Danel Ahman, who was an intern with us for a short while, became a Cambridge student.

Our further colleagues are Jaan Penjam, Hellis Tamm and Enn Tõugu with their students.

Former members of the group include Mohamed El-Zawawy (back in Cairo), Adam Eppendahl (now in Malaysia), Ando Saabas (at Skype) and Olha Shkaravska (moved on to Nijmegen).

What We Do

We have been and are pursuing research in a number of directions. Here are some:

• dependently typed programming;
• coinductive big-step semantics and constructive logic;
• program logics and type systems, in particular for safety and program analyses used in optimizations; proof-transforming and type-deriving compilation;
• directed containers;
• relative monads;
• comonads and distributive laws as means to structure dataflow computation and other paradigms of context-dependent computation;
• partiality from non-termination as a monadic effect;
• structural proof theory of bi-intuitionistic logic;
• the coproduct of monads as a means to combine monadic effects;
• categorical shortcut deforestation;
• categorical structured recursion and corecursion, recursive coalgebras,
• inductive and coinductive types in typed lambda calculi, Mendler-style structured (co)recursion, a.k.a. type-based termination, a.k.a. circular proofs.

We run a regular research seminar, the Theory Seminar (TSEM).

Our collaboration partners include Nottingham, Minho, Nijmegen, Udine, LMU Munich.

We participated in the European FP6 IST project MOBIUS, the major proof-carrying code project of the Old World. We contributed to Types, the network of Europe's type theorists, and APPSEM II, an applied semantics network. At this moment, we are working on the FP7 ICT project HATS on trustworthy highly adaptive software. We are part of the COST action FoVeOOS on verification of object-oriented software.

At home, we are part of the Centre of Excellence in Computer Science (EXCS), one of the seven Estonian CoEs 2008-2015.

We were the organizing team behind these international events: APPSEM 2004, AFP 2004, TFP/ICFP/GPCE 2005, IFIP WG 2.8 Meeting #22, MPC/AMAST 2006, EffTT 2007, NWPT 2008, COST IC0701 2009 Winter School.

This year 2012 we are the hosts of ETAPS, Europe's premier forum for software science.

We are active supporters of EWSCS, an international winter school series in TCS, and the biannual Estonian Theory Days. The latest editions were EWSCS 2011, the Theory Days at Tõrve and the Theory Days at Kubija.

Coming up now is EWSCS 2012 (26 Feb.-2 March 2012).

We like to receive guests. Last year 2011 Marc Pantel (INP Toulouse), Marc Bezem (U. i Bergen), Einar Broch Johnsen, Rudolf Schlatte, Ingrid Chieh Yu (U. i Oslo), Paul Levy (U. of Birmingham), Celia Picard (U. Toulouse 3), Alberto Pardo (U. de la República, Montevideo), Dominic Orchard (U. of Cambridge), Karl Palmskog (KTH), James Brotherston (Imperial College), Andreas Abel (LMU München) visited us.

Interested in Working Here or Visiting?

We are always interested in good students of all levels. If you are from Tallinn or Tartu and would like write a term paper or a MSc or PhD thesis with us, just get in touch. The cool computer science happens here.

We are also interested in PhD students and postdocs from abroad. If this sounds exciting, please enquire. Sometime positions can be set up at a very short notice.

If you'd like to visit and give a seminar talk, email us.