BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Urban:Christian

Contributed to:

ESOP 20112011
SAC 20112011
LICS 20082008
RTA 20082008
CADE 20072007
IJCAR 20062006
CADE 20052005
TLCA 20052005
ICLP 20042004
CSL 20032003
TLCA 20012001
TLCA 19991999
ECOOP 20172017

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.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.