Towards more efficient, usable and socially accepted file sharing with anonymity/deniability

This topic has captured my attention for quite some time now. So far the paper on breaking anonymity by learning a unique hitting set has appeared in the proceedings of CSR'09 (see publications page), the paper on Network Information Systems for Anonymity Networks will appear at CCS'09. My PhD thesis "World Libraries - Towards Efficiently Sharing Large Data Volumes in Open Untrusted Environments while Preserving Privacy" will be published soon.

Exact algorithms for hard problems

All the papers on exact algorithms for hard problems that I have been involved with in this group are neatly itemized on Daniel Mölle's Homepage. Most of them should also be available on our publications page.

Interactive Theorem Proving with Isabelle/Isar

Formal Integration Theory, with an application to probabilistic algorithms.
These are Isabelle/Isar theory texts. Beware, the main theory needs HOL/Complex images, the example even HOL4ExtraProb converted HOL4 sources from Sebastian Skalberg's import tool. A large part of these theories is available in a more up-to-date form on AFP.

TPHOLs 2004: Formalizing Integration Theory, with an Application to Probabilistic Algorithms

Diploma Thesis (pdf):

Very old undergraduate papers in german

Hauptseminararbeit zum Pi-Kalkül:

Proseminararbeit zu Higher Order Logic: