Nederlandse Vereniging voor Theoretische Informatica ==================================================== We are happy to invite you for the Theory Day 2011 of the NVTI. The Dutch Asssociation for Theoretical Computer Science (NVTI) supports the study of theoretical computer science and its applications. NVTI Theory Day 2011 Friday March 4, 2011, 9:30-16:40 Hoog Brabant, Utrecht (close to Central Station) We have an interesting program with excellent speakers from The Netherlands and abroad, covering important streams in theoretical computer science. Below you will find the abstracts. Speakers: Jos Baeten (TU/e) S. Muthu Muthukrishnan (Rutgers University, USA) Hans Bodlaender (UU) Tobias Nipkow (TU Muenchen, Germany) It is possible to participate in the organized lunch, for which registration is required. Please register with Ms Caroline Waij (cpwaij@few.vu.nl or 020-5983563) no later than one week before the meeting (February 25, 2011). The costs of 15 Euro can be paid at the location. We just mention that in the direct vicinity of the meeting room there are plenty of nice lunch facilities as well. The NVTI theory days are sponsored (financially or in kind) by NWO (Netherlands Organisation for Scientific Research), Elseviers Science, CWI (Dutch Center of Mathematics and Computer Science), CTIT (Center for Telematics and Information Technology, Twente), and the Dutch research schools IPA (Institute for Programming Research and Algorithmics) and SIKS (Dutch research school for Information and Knowledge Systems). Please find the full program and abstracts of the lectures below. Kind regards, Femke van Raamsdonk, NVTI secretary. ********************************************************************* ********************************************************************* 9.30-10.00: Arrival with Coffee 10.00-10.10: Opening 10.10-11.00: Speaker: Jos Baeten (TU/e) Title: Computations and Interaction 11.00-11.30: Coffee/Tea 11.30-12.20: Speaker: S. Muthu Muthukrishnan (Rutgers University, USA) Title: Algorithmic Theory of Massive Data Streams 12.20-12.40: Speaker: Yvette Tuin (NWO) 12.40-14.10: Lunch (see above for registration) 14.10-15.00: Speaker: Hans Bodlaender Title: Kernelization: Analysis of Preprocessing 15.00-15.20: Coffee/Tea 15.20-16.10: Speaker: Tobias Nipkow (TU Muenchen, Germany) Title: Teaching Semantics with a Proof Assistant or No more LSD trip proofs 16.10-16.40: Business meeting NVTI ********************************************************************* ********************************************************************* Abstracts of the talks of NVTI Theory Day of March 4, 2011 ********************************************************************* ********************************************************************* 10.10-11.00 Speaker: Jos Baeten (TU/e) Title: Computations and Interaction Abstract: We enhance the notion of a computation of the classical theory of computing with the notion of interaction. In this way, we enhance a Turing machine as a model of computation to a Reactive Turing Machine that is an abstract model of a computer as it is used nowadays, always interacting with the user and the world. The result is a new theory of computing, that takes interaction into consideration from the start, that subsumes all old results of the theory of computing, extending these to a more general setting in some cases, showing they do not extend in other cases. This theory can be taught to first-year students of computer science, providing them with a solid basis for computer science as before, but at the same time providing a solid basis for later courses on formal methods and model checking. At the end of the talk, I present my definition of the science of computer science, thus providing food for discussion afterwards. This is joint work with Bas Luttik and Paul van Tilburg ********************************************************************* ********************************************************************* 11.30-12.20 Speaker: S. Muthu Muthukrishnan (Rutgers University, USA) Title: Algorithmic Theory of Massive Data Streams Abstract: In many applications, data now arrives in massive streams, and we need to process them in a space, time and communication efficient way. The standard notions of efficiency --- even the golden goal of linear space and time --- are no longer suitable for such applications, and in the past few years, we have had to develop a theory of algorithms that work with sublinear resources: sublinear space, or sublinear per item processing time or sublinear number of bits communicated between multiple machines that process data streams. In this talk, I will survey this theory and discuss new emerging directions. ********************************************************************* ********************************************************************* 14.10-15.00 Speaker: Hans Bodlaender Title: Kernelization: Analysis of Preprocessing Abstract: A common approach when solving computationally hard (e.g., NP-complete) problems in practice is to start with a preprocessing phase, where the input is transformed to an equivalent, and usually smaller input. E.g., for many graph problems, preprocessing where vertices of degree zero or one are removed, is possible. With help of techniques from the area of fixed parameter tractability, we can analyse how effective such preprocessing can be, i.e., give bounds on resulting instances after polynomial time preprocessing. This talk surveys several recent results from this area of kernelization, including kernels for some specific problems, meta-results, and lower bound techniques. ********************************************************************* ********************************************************************* 15.20-16.10 Speaker: Tobias Nipkow (TU Muenchen, Germany) Title: Teaching Semantics with a Proof Assistant or No more LSD trip proofs The gulf between many computer science students and rigorous proofs is well known and much lamented. Teachers are frequently confronted with student ``proofs'' that look more like LSD trips than coherent chains of logic. In this talk I will present a new Programming Language Semantics course that bridges the gulf with the help of a proof assistant, Isabelle. During the first quarter of the semester the students are introduced to machine-checked proofs. The rest of the course covers a wide spectrum of topics centered around a simple imperative language: operational semantics, compilation, types, program analysis and Hoare logic. At the end of my talk I will give a (predictably positive) evaluation of the approach. ********************************************************************* *********************************************************************