Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Homepage of Christian Urban
[go: Go Back, main page]
Links
Home
Publications
Teaching
Recent Talks

Handy Information
People in Logic
Programming Languages
Miscellaneous






Christian Urban

Note that I have received a fellowship from the Alexander-von-Humboldt Foundation and moved to Munich.

E-mail urban at mathematik uni-muenchen de

Address Mathematisches Institut der LMU, Theresienstr. 39, D-80333 Muenchen, Germany
Current Position I have research fellowship from the Alexander-von-Humboldt foundation.

Research Interests semantics of programming languages, proof theory, type systems, linear logic, concurrency, lambda calculus, theorem assistants, unifciation, computability, complexity, functional and logic programming.
Nominal Logic I work on a nominal theorem assistant inspired by FreshML - a wonderful project headed by Prof. Andrew Pitts. Nominal unification is one outcome of this work. Another is the logic programming language alpha-Prolog - click for details here. The nominal unification algorithm has been formally verified in Isabelle. The funding for this work was provided through a research fellowship from Corpus Christi College, Cambridge. I continue this work as a Alexander-von-Homboldt fellow at the LMU in Munich.
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 thesis in Marseille. My study in Cambridge was funded by two scholarships from the German government; my year in Marseille by a TMR-fellowship from the EC. I still work on this topic within the project Semantics of Classical Proofs.
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.

Last modified: Thu Sep 30 22:44:41 UTC 2004 [Validate this page.]