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.
*********************************************************************
*********************************************************************