`Travelled to:`

1 × Estonia

1 × France

1 × Italy

1 × Japan

1 × Poland

1 × Taiwan

2 × Austria

2 × Germany

2 × USA

`Collaborated with:`

J.Cheney S.Berghofer C.Kaliszyk B.Zhu C.Tasson ∅ G.M.Bierman M.Norrish A.M.Pitts M.Gabbay M.Berger L.Tratt

`Talks about:`

isabell (4) nomin (4) elimin (3) hol (3) cut (3) normalis (2) revisit (2) program (2) equival (2) strong (2)

## Person: Christian Urban

### DBLP: Urban:Christian

### Contributed to:

### Wrote 13 papers:

- ESOP-2011-UrbanK
- General Bindings and α-Equivalence in Nominal Isabelle (CU, CK), pp. 480–500.
- SAC-2011-KaliszykU #higher-order
- Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
- LICS-2008-UrbanCB
- Mechanizing the Metatheory of LF (CU, JC, SB), pp. 45–56.
- RTA-2008-UrbanZ #proving
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof (CU, BZ), pp. 409–424.
- CADE-2007-UrbanBN
- Barendregt’s Variable Convention in Rule Inductions (CU, SB, MN), pp. 35–50.
- IJCAR-2006-UrbanB #combinator #data type #higher-order #recursion
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
- CADE-2005-UrbanT #higher-order
- Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.
- TLCA-2005-UrbanC #prolog
- Avoiding Equivariance in αProlog (CU, JC), pp. 401–416.
- ICLP-2004-CheneyU #logic programming #named #programming language #prolog
- αProlog: A Logic Programming Language with Names, Binding and α-Equivalence (JC, CU), pp. 269–283.
- CSL-2003-UrbanPG
- Nominal Unificaiton (CU, AMP, MG), pp. 513–527.
- TLCA-2001-Urban #normalisation
- Strong Normalisation for a Gentzen-like Cut-Elimination Procedure (CU), pp. 415–430.
- TLCA-1999-UrbanB #logic #normalisation
- Strong Normalisation of Cut-Elimination in Classical Logic (CU, GMB), pp. 365–380.
- ECOOP-2017-BergerTU #generative #metaprogramming #modelling
- Modelling Homogeneous Generative Meta-Programming (MB, LT, CU), p. 23.