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
3802021
Nominal unification
C Urban, AM Pitts, MJ Gabbay
Theoretical Computer Science 323 (1-3), 473-497, 2004
2612004
Nominal techniques in Isabelle/HOL
C Urban
Journal of Automated Reasoning 40 (4), 327-356, 2008
2212008
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
1652017
Nominal techniques in Isabelle/HOL
C Urban, C Tasson
International Conference on Automated Deduction, 38-53, 2005
1472005
Classical logic and computation
C Urban
University of Cambridge, 2000
1362000
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
1112018
αProlog: A Logic Programming Language with Names, Binding and α-Equivalence
J Cheney, C Urban
International Conference on Logic Programming, 269-283, 2004
1092004
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
1012019
Nominal logic programming
J Cheney, C Urban
ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5), 1-47, 2008
902008
Barendregt’s variable convention in rule inductions
C Urban, S Berghofer, M Norrish
International Conference on Automated Deduction, 35-50, 2007
832007
Strong normalisation of cut-elimination in classical logic
C Urban, GM Bierman
Fundamenta Informaticae 45 (1-2), 123-155, 2001
812001
Nominal unification
C Urban, A Pitts, M Gabbay
International Workshop on Computer Science Logic, 513-527, 2003
682003
General bindings and alpha-equivalence in Nominal Isabelle
C Kaliszyk, C Urban
Logical methods in computer science 8, 2012
582012
A recursion combinator for nominal datatypes implemented in Isabelle/HOL
C Urban, S Berghofer
International Joint Conference on Automated Reasoning, 498-512, 2006
512006
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
462007
Mechanizing the metatheory of LF
C Urban, J Cheney, S Berghofer
ACM Transactions on Computational Logic (TOCL) 12 (2), 1-42, 2011
442011
Mechanising turing machines and computability theory in Isabelle/HOL
J Xu, X Zhang, C Urban
International Conference on Interactive Theorem Proving, 147-162, 2013
422013
Quotients revisited for Isabelle/HOL
C Kaliszyk, C Urban
Proceedings of the 2011 ACM Symposium on Applied Computing, 1639-1644, 2011
382011
A formalisation of the Myhill-Nerode theorem based on regular expressions
C Wu, X Zhang, C Urban
Journal of automated reasoning 52 (4), 451-480, 2014
35*2014
The system can't perform the operation now. Try again later.
Articles 1–20