Christian Urban

Publication Activity (10 Years)

Years Active: 1998-2023
Publications (10 Years): 9

Top Topics

Regular Expressions

Pattern Matching

Deterministic Finite Automata

Top Venues

J. Autom. Reason.

Arch. Formal Proofs

Publications

Christian Urban
POSIX Lexing with Derivatives of Regular Expressions. J. Autom. Reason. 67 (3) (2023)
Chengsong Tan, Christian Urban
POSIX Lexing with Bitcoded Derivatives. ITP (2023)
Xingyuan Zhang, Christian Urban, Chunhan Wu
Priority Inheritance Protocol Proved Correct. J. Autom. Reason. 64 (1) (2020)
Xingyuan Zhang, Christian Urban
Selected Extended Papers of ITP 2015: Preface. J. Autom. Reason. 62 (4) (2019)
Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten
Universal Turing Machine. Arch. Formal Proofs 2019 (2019)
Martin Berger, Laurence Tratt, Christian Urban
Modelling Homogeneous Generative Meta-Programming. ECOOP (2017)
Martin Berger, Laurence Tratt, Christian Urban
Modelling homogeneous generative meta-programming. CoRR (2016)
Fahad Ausaf, Roy Dyckhoff, Christian Urban
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). ITP (2016)
Fahad Ausaf, Roy Dyckhoff, Christian Urban
POSIX Lexing with Derivatives of Regular Expressions. Arch. Formal Proofs 2016 (2016)
Chunhan Wu, Xingyuan Zhang, Christian Urban
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. J. Autom. Reason. 52 (4) (2014)
Jian Xu, Xingyuan Zhang, Christian Urban
Mechanising Turing Machines and Computability Theory in Isabelle/HOL. ITP (2013)
Chunhan Wu, Xingyuan Zhang, Christian Urban
A Formal Model and Correctness Proof for an Access Control Policy Framework. CPP (2013)
Xingyuan Zhang, Christian Urban, Chunhan Wu
Priority Inheritance Protocol Proved Correct. ITP (2012)
Maribel Fernández, Christian Urban
Preface: Theory and Applications of Abstraction, Substitution and Naming. J. Autom. Reason. 49 (2) (2012)
Christian Urban, Cezary Kaliszyk
General Bindings and Alpha-Equivalence in Nominal Isabelle Log. Methods Comput. Sci. 8 (2) (2012)
Chunhan Wu, Xingyuan Zhang, Christian Urban
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). ITP (2011)
Chunhan Wu, Xingyuan Zhang, Christian Urban
The Myhill-Nerode Theorem Based on Regular Expressions. Arch. Formal Proofs 2011 (2011)
Christian Urban, Cezary Kaliszyk
General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP (2011)
James Cheney, Christian Urban
Mechanizing the Metatheory of mini-XQuery. CPP (2011)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12 (2) (2011)
Cezary Kaliszyk, Christian Urban
Quotients revisited for Isabelle/HOL. SAC (2011)
Brian Huffman, Christian Urban
A New Foundation for Nominal Isabelle. ITP (2010)
Christian Urban
Nominal Unification Revisited UNIF (2010)
Andreas Abel, Christian Urban
Preface. Electron. Notes Theor. Comput. Sci. 228 (2009)
Christian Urban, Bozhi Zhu
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. RTA (2008)
Christian Urban, Julien Narboux
Formal SOS-Proofs for the Lambda-Calculus. LSFA (2008)
Christian Urban
Nominal Techniques in Isabelle/HOL. J. Autom. Reason. 40 (4) (2008)
Peter Chapman, James McKinna, Christian Urban
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus (2008)
Julien Narboux, Christian Urban
Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. Electron. Notes Theor. Comput. Sci. 196 (2008)
Stefan Berghofer, Christian Urban
Nominal Inversion Principles. TPHOLs (2008)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the Metatheory of LF CoRR (2008)
James Cheney, Christian Urban
Nominal logic programming. ACM Trans. Program. Lang. Syst. 30 (5) (2008)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the Metatheory of LF. LICS (2008)
Christian Urban, Stefan Berghofer, Michael Norrish
Barendregt's Variable Convention in Rule Inductions. CADE (2007)
Stefan Berghofer, Christian Urban
A Head-to-Head Comparison of de Bruijn Indices and Names. Electron. Notes Theor. Comput. Sci. 174 (5) (2007)
Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban
Categorical proof theory of classical propositional calculus. Theor. Comput. Sci. 364 (2) (2006)
Christian Urban, Stefan Berghofer
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR (2006)
James Cheney, Christian Urban
Nominal Logic Programming CoRR (2006)
Christian Urban, Christine Tasson
Nominal Techniques in Isabelle/HOL. CADE (2005)
Christian Urban, James Cheney
Avoiding Equivariance in Alpha-Prolog. TLCA (2005)
Christian Urban, Michael Norrish
A formal treatment of the barendregt variable convention in rule inductions. MERLIN (2005)
James Cheney, Christian Urban
alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. ICLP (2004)
Christian Urban, Andrew M. Pitts, Murdoch Gabbay
Nominal unification. Theor. Comput. Sci. 323 (1-3) (2004)
Roy Dyckhoff, Christian Urban
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. J. Log. Comput. 13 (5) (2003)
Christian Urban, Andrew M. Pitts, Murdoch Gabbay
Nominal Unificaiton. CSL (2003)
Christian Urban
Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. TLCA (2001)
Christian Urban, Gavin M. Bierman
Strong Normalisation of Cut-Elimination in Classical Logic. Fundam. Informaticae 45 (1-2) (2001)
Christian Urban, Gavin M. Bierman
Strong Normalisation of Cut-Elimination in Classical Logic. TLCA (1999)
Christian Urban
Implementation of Proof Search in the Imperative Programming Language Pizza. TABLEAUX (1998)