Christian Urban - Research output - King's College London

Phone82584

WC2B 4PH
United Kingdom

437

Citations

15 Conference paper
7 Article
3 Chapter
1 Other chapter contribution
More
- 1 Special issue

15 results

Filter

2023
POSIX Lexing with Bitcoded Derivatives
Tan, C. & Urban, C., 18 Apr 2023, (Accepted/In press) 14th International Conference on Interactive Theorem Proving (ITP 2023). Naumowicz, A. & Thiemann, R. (eds.). p. 26:1-26:18 18 p. 26
Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Open Access
File
85 Downloads (Pure)
2017
Modelling Homogeneous Generative Meta-programming
Berger, M., Tratt, L. R. & Urban, C., 16 Jun 2017, (E-pub ahead of print) In: Leibniz International Proceedings in Informatics, LIPIcs. 74, 23 p.
Research output: Contribution to journal › Conference paper › peer-review

Open Access
File
3 Citations (Scopus)

85 Downloads (Pure)
2016
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 › peer-review

Open Access
File
14 Citations (Scopus)

339 Downloads (Pure)
2013
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 › peer-review
3 Citations (Scopus)
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 › peer-review
27 Citations (Scopus)
2012

Priority Inheritance Protocol Proved Correct
Urban, C., Zhang, X. & Wu, C., 2012, Proceedings of the 3rd Conference on Interactive Theorem Proving (ITP 2012). Beringer, L. & Felty, A. (eds.). 7406 ed. Springer, Vol. Lecture Notes in Computer Science. p. 217 - 232 16 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper

7 Citations (Scopus)
2011
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions (Proof-Pearl)
Wu, C., Zhang, X. & Urban, C., 2011, Proceedings of the 2nd Conference on Interactive Theorem Proving (ITP 2011). : Lecture Notes in Computer Science. p. 341-356 6 p. (Lecture Notes in Computer Science ; vol. 6898).
Research output: Chapter in Book/Report/Conference proceeding › Conference paper
15 Citations (Scopus)
Mechanizing the Metatheory of Mini-XQuery
Urban, C. & Cheney, J., 2011, Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings. Springer Berlin Heidelberg, Vol. 7086. p. 280 - 295 16 p. (Lecture Notes in Computer Science; vol. 7086).
Research output: Chapter in Book/Report/Conference proceeding › Conference paper
5 Citations (Scopus)
Quotients Revisited for Isabelle/HOL
Urban, C. & Kaliszyk, C., 2011, Proceedings of the ACM Symposium on Applied Computing (SAC 2011). p. 1639-1644 6 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper
24 Citations (Scopus)
2010
A New Foundation for Nominal Isabelle
Huffman, B. & Urban, C., 2010, Proceedings of the 1st Conference on Interactive Theorem Proving (ITP 2010): Lecture Notes in Computer Science. Springer, Vol. 6172. p. 35 - 50 16 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper
18 Citations (Scopus)
Nominal Unification Revisited
Urban, C., 2010, Proceedings of the 24th Workshop on Unification (UNIF 2010): Electronic Proceedings in Theoretical Computer Science. arXiv, Vol. 42. 11 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper
2008

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

3 Citations (Scopus)
Mechanizing the Metatheory of LF
Urban, C., Cheney, J. & Berghofer, S., 2008, Proceedings of the 23rd IEEE Symposium on Logic in Computer Science (LICS 2008): IEEE Computer Society. p. 45 - 56 12 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper

14 Citations (Scopus)
Nominal Inversion Principles
Berghofer, S. & Urban, C., 2008, Proceedings of 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08): Lecture Notes in Computer Science. Vol. 5170. p. 71 - 85 15 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference paper

8 Citations (Scopus)
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

9 Citations (Scopus)

Your message has successfully been sent.

Your message was not sent due to an error.