Links
Home
Publications
Teaching
Recent Talks
My Research Group

Handy Information
People in Logic
Programming Languages
Miscellaneous

Christian Urban

E-mail urbanc at in tum de

Address Institute for Computer Science at the TU Munich (IV), Boltzmannstrasse 3, D-85748 Garching, Germany.

Telephone +49 89 289 17885

Isabelle Documentation Project (contains now a draft of a 200-page tutorial on Isabelle programming)
Submit a paper to the Special Issue on Binding, Substitution and Naming in the Journal of Automated Reasoning.
Current Position I have been awarded an Emmy-Noether fellowship to head an independent research group in the Computer Science Department at the TU Munich. This group co-operates with the Theorem Proving Group chaired by Prof. Tobias Nipkow and is accommodated by the institute of Prof. Manfred Broy.

Past Positions Between September 2008 and February 2009, I was an invited research fellow in the Department of Computer Science in Princeton. In 2004/05 I was an Alexander-von-Humboldt fellow in Munich and from 2000 until 2004 I was awarded a Research Fellowship in Cambridge. Before that I did my PhD in Cambridge.

Research Interests theorem provers, semantics of programming languages, proof theory, type systems, concurrency, lambda calculus, unification, computability, complexity, functional and logic programming.

Conferences UNIF'06 (member of PC), LFMTP'07 (member of PC), LFMTP'08 (PC co-chair), WMM'08 (member of PC), LSFA'08 (invited speaker), TAASN'09 (member of PC), LSFA'09 (member of PC), IDW (organiser), WMM'09 (PC chair), TPHOLs'09 (PC co-chair), ITP'10 (member of PC)

Nominal Isabelle I currently work on Nominal Isabelle. This is joint work with Dr Stefan Berghofer, Dr Markus Wenzel and the Isabelle-team in Munich. Many ideas originate from the nominal logic project - a wonderful project headed by Prof. Andrew Pitts. The aim of my work is to make formal reasoning involving binders as simple as on paper and the hope is to lure masses to automated theorem proving. My funding for this work was provided in 2004 and 2005 by a research fellowship from the Alexander-von-Humboldt foundation. During this time I was a visitor in the group of Prof. Helmut Schwichtenberg. Since 2006 this work is supported by an Emmy-Noether fellowship. There is a webpage and a mailing list about Nominal Isabelle.
Nominal Unification and Alpha-Prolog Nominal unification is one outcome of my involvement in the nominal logic project in Cambridge. Another is the logic programming language alpha-Prolog (joint work with Dr James Cheney), which uses nominal unification - click for details here. The nominal unification algorithm has been formally verified in Isabelle. This was possible since this unification algorithm is formulated in a simple first-order language (unlike other algorithms for higher-order unification). Prof. Daniel Friedman and his group use nominal unification in their alpha-Kanren system implemented in Scheme. My funding for this work was provided through a research fellowship from Corpus Christi College, Cambridge.
Classical Logic I was Ph.D. student in the University of Cambridge Computer Laboratory and for three years called Gonville and Caius College my home. I was very lucky to have Dr Gavin Bierman as supervisor. My research in Cambridge was also very much influenced by Prof. Martin Hyland. Some details on my thesis "Classical Logic and Computation" are elsewhere, including a Java Applet that 'visualises' some of the results from the thesis. I completed the writing of the thesis in Marseille in the group of Prof. Jean-Yves Girard. My study in Cambridge was funded by two scholarships from the German government; my year in Marseille by a TMR-fellowship from the EU. My PhD was also one starting point for the EPSRC Project on the Semantics of Classical Proofs. The strong normalisation result in the PhD has recently been used by Prof. Claude Kirchner and his students to prove consistency for their superdeduction system lemuridae.
Forum I implemented Forum, a programming language based on classical linear logic, as my M.Phil. thesis. This was joint work with Dr Roy Dyckhoff. Details can be found here and here. During my M.Phil study I spent one month in Philadelphia invited by Prof. Dale Miller.
G4ip An implementation of G4ip using the imperative language Pizza can be found here. Pizza is a conservative extension of Java. The implementation illustrates the technique of success continuations.
Junge Informatik.

Last modified: Thu Dec 17 08:31:07 CET 2009 [Validate this page.]