Follow
Christian Urban
Title
Cited by
Cited by
Year
Multilevel proteomics reveals host perturbations by SARS-CoV-2 and SARS-CoV
A Stukalov, V Girault, V Grass, O Karayel, V Bergant, C Urban, DA Haas, ...
Nature 594 (7862), 246-252, 2021
5652021
Nominal unification
C Urban, AM Pitts, MJ Gabbay
Theoretical Computer Science 323 (1-3), 473-497, 2004
2662004
Nominal techniques in Isabelle/HOL
C Urban
Journal of Automated Reasoning 40, 327-356, 2008
2352008
Ancient Egyptian mummy genomes suggest an increase of Sub-Saharan African ancestry in post-Roman periods
VJ Schuenemann, A Peltzer, B Welte, WP Van Pelt, M Molak, CC Wang, ...
Nature communications 8 (1), 1-11, 2017
2032017
Nominal techniques in Isabelle/HOL
C Urban, C Tasson
Automated Deduction–CADE-20: 20th International Conference on Automated …, 2005
1522005
A protein-interaction network of interferon-stimulated genes extends the innate immune system landscape
P Hubel, C Urban, V Bergant, WM Schneider, B Knauer, A Stukalov, ...
Nature immunology 20 (4), 493-502, 2019
1452019
Ancient genomes reveal a high diversity of Mycobacterium leprae in medieval Europe
VJ Schuenemann, C Avanzi, B Krause-Kyora, A Seitz, A Herbig, S Inskip, ...
PLoS pathogens 14 (5), e1006997, 2018
1452018
Classical logic and computation
C Urban
University of Cambridge, 2000
1402000
αProlog: A Logic Programming Language with Names, Binding and α-Equivalence
J Cheney, C Urban
International Conference on Logic Programming, 269-283, 2004
1182004
Nominal logic programming
J Cheney, C Urban
ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5), 1-47, 2008
922008
Barendregt’s variable convention in rule inductions
C Urban, S Berghofer, M Norrish
Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007
862007
Strong normalisation of cut-elimination in classical logic
C Urban, GM Bierman
Fundamenta Informaticae 45 (1-2), 123-155, 2001
842001
General bindings and alpha-equivalence in Nominal Isabelle
C Urban, C Kaliszyk
Logical methods in computer science 8, 2012
792012
Nominal unification
C Urban, A Pitts, M Gabbay
Computer Science Logic: 17th International Workshop CSL 2003, 12th Annual …, 2003
692003
A head-to-head comparison of de Bruijn indices and names
S Berghofer, C Urban
Electronic Notes in Theoretical Computer Science 174 (5), 53-67, 2007
552007
A recursion combinator for nominal datatypes implemented in Isabelle/HOL
C Urban, S Berghofer
Automated Reasoning: Third International Joint Conference, IJCAR 2006 …, 2006
522006
Mechanising turing machines and computability theory in Isabelle/HOL
J Xu, X Zhang, C Urban
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
482013
2000-year-old pathogen genomes reconstructed from metagenomic analysis of Egyptian mummified individuals
J Neukamm, S Pfrengle, M Molak, A Seitz, M Francken, P Eppenberger, ...
BMC biology 18 (1), 1-18, 2020
452020
Interferon‐induced degradation of the persistent hepatitis B virus cccDNA form depends on ISG20
D Stadler, M Kächele, AN Jones, J Hess, C Urban, J Schneider, Y Xia, ...
EMBO reports 22 (6), e49568, 2021
442021
Mechanizing the metatheory of LF
C Urban, J Cheney, S Berghofer
ACM Transactions on Computational Logic (TOCL) 12 (2), 1-42, 2011
432011
The system can't perform the operation now. Try again later.
Articles 1–20