| 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 | 523 | 2021 |
| Nominal unification C Urban, AM Pitts, MJ Gabbay Theoretical Computer Science 323 (1-3), 473-497, 2004 | 264 | 2004 |
| Nominal techniques in Isabelle/HOL C Urban Journal of Automated Reasoning 40, 327-356, 2008 | 233 | 2008 |
| 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 | 197 | 2017 |
| Nominal techniques in Isabelle/HOL C Urban, C Tasson Automated Deduction–CADE-20: 20th International Conference on Automated …, 2005 | 152 | 2005 |
| 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 | 141 | 2018 |
| Classical logic and computation C Urban University of Cambridge, 2000 | 140 | 2000 |
| 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 | 139 | 2019 |
| αProlog: A Logic Programming Language with Names, Binding and α-Equivalence J Cheney, C Urban International Conference on Logic Programming, 269-283, 2004 | 114 | 2004 |
| Nominal logic programming J Cheney, C Urban ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5), 1-47, 2008 | 90 | 2008 |
| Barendregt’s variable convention in rule inductions C Urban, S Berghofer, M Norrish Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007 | 85 | 2007 |
| Strong normalisation of cut-elimination in classical logic C Urban, GM Bierman Fundamenta Informaticae 45 (1-2), 123-155, 2001 | 85 | 2001 |
| General bindings and alpha-equivalence in Nominal Isabelle C Urban, C Kaliszyk Logical methods in computer science 8, 2012 | 79 | 2012 |
| Nominal unification C Urban, A Pitts, M Gabbay Computer Science Logic: 17th International Workshop CSL 2003, 12th Annual …, 2003 | 69 | 2003 |
| A recursion combinator for nominal datatypes implemented in Isabelle/HOL C Urban, S Berghofer Automated Reasoning: Third International Joint Conference, IJCAR 2006 …, 2006 | 53 | 2006 |
| 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 | 52 | 2007 |
| 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 | 48 | 2013 |
| 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 | 44 | 2020 |
| Mechanizing the metatheory of LF C Urban, J Cheney, S Berghofer ACM Transactions on Computational Logic (TOCL) 12 (2), 1-42, 2011 | 43 | 2011 |
| Quotients revisited for Isabelle/HOL C Kaliszyk, C Urban Proceedings of the 2011 ACM Symposium on Applied Computing, 1639-1644, 2011 | 39 | 2011 |
James CheneyProfessor, Laboratory for Foundations of Computer Science, University of EdinburghVerified email at inf.ed.ac.uk
