Recent Talks
Nominal Isabelle

Handy Information
People in Logic
Programming Languages

Christian Urban

E-mail christian.urban at kcl ac uk

Address Department of Informatics, King's College London, Bush House, 30 Aldwych, London WC2B 4BG, UK. My office is 7.07 on the 7th floor, North Wing, of the Bush House.

Isabelle Programming Tutorial (draft of a 200-page tutorial on Isabelle programming)

Current Position I am a lecturer in the Department of Informatics at King's College London. This is similar to a position of an assistant professor in other places. In 2011, I was also offered a lectureship here, an associate professorship here, and full professorships here and here. I thank all people involved for their efforts.

Past Positions In April 2006, I was awarded an Emmy-Noether fellowship, which I held at the TU Munich until September 2011. Between September 2008 and February 2009, I was an invited research scientist 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 funded by two scholarships from the German Academic Exchange Service (DAAD).

Skolem Award 2015 Together with Christine Tasson, I was awarded a Thoralf Skolem Award, a ten-year test-of-time award from CADE, for our paper on Nominal Techniques in Isabelle/HOL from 2005. This award was given also to Nicolaas de Bruijn and Nachum Derschowitz, amongst others.

Research Interests theorem provers, verification, programming languages, compilers, algorithms, proof theory, type systems, concurrency, lambda calculus, unification, regular expressions, computability, complexity, functional and logic programming.

Teaching I usually enjoy teaching. At King's my students nominated me for the Teaching Excellence Award in 2012, 2015, 2016 and 2017, and for the best MSc Project supervisor in 2015. In 2014 I received both prizes for Best UG Project Supervisor and for Best MSc Project Supervisor in the NMS Faculty.

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'09 (organiser), WMM'09 (PC chair), TPHOLs'09 (PC co-chair), Automatheo'10 (member of PC), ITP'10 (member of PC), UNIF'10 (invited speaker), WMM'10 (invited speaker), IDW'10 (co-organiser), CPP'11 (member of PC), RTA'11 (member of PC), LFMTP'11 (member of PC), ITP'14 (member of PC), MKM'15 (member of PC), ITP'15 (PC co-chair), ITP'16 (member of PC) LSFA'17 (member of PC) ITP'17 (member of PC)

ITP'15 took place in Nanjing organised by Xingyuan Zhang and me

Current PhD Fahad Ausaf
Former RAs Chunhan Wu, Cezary Kaliszyk, Julien Narboux

If I am not teaching or not doing research, I am sometimes in the lavender fields of London.

Nominal Isabelle I currently work on Nominal Isabelle 2. This is joint work with Dr Stefan Berghofer, Dr Markus Wenzel, Dr Cezary Kaliszyk, Dr Tjark Weber and the Isabelle-team in Munich. Many of the theoretical 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. It also includes a list of projects that use Nominal Isabelle. Users of Nominal Isabelle had their papers appearing at LICS, POPL, FOSSACS, SOS, TPHOLs, CPP, SEFM, the Haskell Symposium and in the Journal of Automated Reasoning.
Myhill-Nerode and Regular Expressions Out of frustration of having to teach reasoning in theorem provers with worn-out examples like fib and even/odd, we implemented a large part of regular language theory in Isabelle/HOL. This implementation gives rise to much more interesting examples, as shown here and here. It turns out that formalisations of automata theory are a huge pain in theorem provers, especially in those that are based on HOL. We therefore went against the mainstream and used in our formalisation regular expressions exclusively, because they are much more convenient for formal reasoning. The results we formalised include: the Myhill-Nerode theorem, the closure of regular languages under complementation, finiteness of derivatives of regular expressions and a surprising result about Subseq, which according to this blog should be better known. We also answered a question from the same blog about "proving Reg-exp-langs [being] closed under complementation without using equiv to DFA's"....yes we can! This is joint work with Prof. Xingyuan Zhang and his student Chunhan Wu from the PLA University of Science and Technology in Nanjing. My funding for this work came from the Chinese-German Research Centre.
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. Maribel Fernandez and her student improved the nominal unification algorithm to be quadratic. Prof. Daniel Friedman and his group use nominal unification in their alpha-Kanren system implemented in Scheme. This work has also found its way into Clojure as the core.logic.nominal package. 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 been used in 2007 by Prof. Claude Kirchner and his students for proving consistency of 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, written around 1996, is a conservative extension of Java and a precursor of Scala. My implementation illustrates the technique of success continuations in proof search.

Time-stamp: <- 2017-09-15 11:24:51 by Christian Urban> [Validate this page.]