[TYPES/announce] 3 years research assistant position in TCS, LMU Munich

[Martin Hofmann]

A position for a research assistant in a DFG project is
available.

Project title: Pointers as an abstract data type:
complexity-theoretic and programming-language aspects (PURPLE)

Investigators: Martin Hofmann and Ulrich Schöpp

Duration: 36 months

Start date: as soon as possible but not later than June 2011.

Remuneration: German scale 13 TV-L (38k-54k EUR according to age,
experience, family status)

Background: PhD in theoretical informatics with some topical overlap,
see project description. Candidates with an excellent Diploma or
Master in this area are also encouraged to apply; in this case
the project work may lead to a PhD.

Location: The project will be carried out at the Institute for
Informatics of Ludwig-Maximilians-Universität Munich, Germany.
LMU is an equal opportunities employer.

Applications should be sent by E-Mail to Sigrid Roden
roden at tcs.ifi.lmu.de as a single PDF file containing in particular CV,
research statement, and the names of two potential referees. There is
no deadline. Applications will be assessed on an on-going basis until
the position is filled.

Questions about the position can be directed to the investigators
{mhofmann, schoepp}@tcs.ifi.lmu.de.

Project description:

In programming languages and logics, graphs and similar data
structures are often treated as structured data rather than
bit-sequences or words. This means that elements of abstract data
structures are often accessed using pointers, which support only a
restricted set of operations, such as lookup, update and test for
equality. The concrete representation of pointers remains
hidden. Traditional computability and complexity theory, on the other
hand, rely on concrete representations of data.

In this project we want to explore the expressivity of abstract
pointer concepts in the sense of complexity theory. In particular we
aim at a separation of programming language versions of LOGSPACE and
PTIME. For example, we conjecture that the PTIME-complete problem of
Horn-satisfiability cannot be solved with a constant number of
abstract pointers, even in the presence of non-determinism or an
oracle for reachability.

Additionally, we want to contribute to the formal specification and
verification of programs with abstract pointers. For instance, we
would like to ascribe rigorous meaning to preconditions like `It makes
no guarantees as to the iteration order of the set ...' in the
specification of the HashSet class in java.util.

For further background reading, we refer to:

- Project proposal to Deutsche Forschungsgemeinschaft (DFG):
  http://www2.tcs.ifi.lmu.de/~schoepp/Docs/purple_antrag.pdf

- Martin Hofmann und Ulrich Schöpp. Pure Pointer Programs with
Iteration.  ACM Transactions on Computational Logic, 2010.

- Martin Hofmann und Ulrich Schöpp. Pointer Programs and Undirected
Reachability. Logic in Computer Science (LICS), 2009.  Extended
version: Electronic Colloquium on Computational Complexity (ECCC)
15(090), 2008