Dr Christian Urban Academics Lecturer in Computer Science MSc Programme Board Chair. Emmy-Noether Fellow of the German Research Council. Research subject areas Computer science Contact details +44 020 7848 2584 christian.urban@kcl.ac.uk
Priority Inheritance Protocol Proved Correct Zhang, X., Urban, C. & Wu, C., 1 Jan 2020, In : JOURNAL OF AUTOMATED REASONING. 64, 1, p. 73-95 23 p. Research output: Contribution to journal - Article. DOIs: https://doi.org/10.1007/s10817-019-09511-5 Modelling Homogeneous Generative Meta-programming Berger, M., Tratt, L. R. & Urban, C., 16 Jun 2017, In : Leibniz International Proceedings in Informatics, LIPIcs. 74, 23 p. Research output: Contribution to journal - Conference paper. DOIs: https://doi.org/10.4230/LIPIcs.ECOOP.2017.5 POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) Ausaf, F., Dyckhoff, R. & Urban, C., 7 Aug 2016, Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Springer LNCS: Springer International Publishing, p. 69-86 17 p. (Lecture Notes in Computer Science ; vol. 9807). Research output: Chapter in Book/Report/Conference proceeding - Conference paper. DOIs: https://doi.org/10.1007/978-3-319-43144-4_5 Mechanising Turing machines and computability theory in Isabelle/HOL Xu, J., Zhang, X. & Urban, C., 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 7998 LNCS. p. 147-162 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7998 LNCS). Research output: Chapter in Book/Report/Conference proceeding - Conference paper. DOIs: https://doi.org/10.1007/978-3-642-39634-2_13 A formalisation of the myhill-nerode theorem based on regular expressions Wu, C., Zhang, X. & Urban, C., 25 Jan 2014, In : JOURNAL OF AUTOMATED REASONING. 52, 4, p. 451-480 30 p. Research output: Contribution to journal - Article. DOIs: https://doi.org/10.1007/s10817-013-9297-2 A formal model and correctness proof for an access control policy framework Wu, C., Zhang, X. & Urban, C., 2013, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 8307 . p. 292-307 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8307 LNCS). Research output: Chapter in Book/Report/Conference proceeding - Conference paper. DOIs: https://doi.org/10.1007/978-3-319-03545-1_19 General Bindings and Alpha-Equivalence in Nominal Isabelle Urban, C. & Kaliszyk, C., 2012, In : Logical methods in computer science. 8, 2, 35 p., 14. Research output: Contribution to journal - Article. DOIs: https://doi.org/10.2168/LMCS-8(2:14)2012 Nominal Logic Programming Cheney, J. & Urban, C., 1 Aug 2008, In : ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS. 30, 5, p. 1 - 47 47 p., 26. Research output: Contribution to journal - Article. DOIs: https://doi.org/10.1145/1387673.1387675 Revisiting Cut-Elimination: One Difficult Proof is Really a Proof Urban, C. & Zhu, B., 2008, Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008): Lecture Notes in Computer Science. Vol. 5117. p. 409 - 424 16 p. Research output: Chapter in Book/Report/Conference proceeding - Conference paper Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle Chapman, P., McKinna, J. & Urban, C., 2008, of 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC'08): Lecture Notes in Artificial Intelligene. Vol. 5144. p. 38 - 52 Research output: Chapter in Book/Report/Conference proceeding - Conference paper View all publications