default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDChristian Urban
Person information
- affiliation: Technical University Munich, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
[j16]Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions. J. Autom. Reason. 67(3): 24 (2023)- [c30]Chengsong Tan, Christian Urban:
POSIX Lexing with Bitcoded Derivatives. ITP 2023: 27:1-27:18 - 2020
- [j15]Xingyuan Zhang, Christian Urban
, Chunhan Wu:
Priority Inheritance Protocol Proved Correct. J. Autom. Reason. 64(1): 73-95 (2020)
2010 – 2019
- 2019
- [j14]Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten:
Universal Turing Machine. Arch. Formal Proofs 2019 (2019) - [j13]Xingyuan Zhang, Christian Urban:
Selected Extended Papers of ITP 2015: Preface. J. Autom. Reason. 62(4): 431-432 (2019) - 2017
- [c29]Martin Berger, Laurence Tratt, Christian Urban:
Modelling Homogeneous Generative Meta-Programming. ECOOP 2017: 5:1-5:23 - 2016
- [j12]Fahad Ausaf, Roy Dyckhoff, Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions. Arch. Formal Proofs 2016 (2016) - [c28]Fahad Ausaf, Roy Dyckhoff, Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). ITP 2016: 69-86 - [i3]Martin Berger, Laurence Tratt, Christian Urban:
Modelling homogeneous generative meta-programming. CoRR abs/1602.06568 (2016) - 2015
- [e3]Christian Urban, Xingyuan Zhang:
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. Lecture Notes in Computer Science 9236, Springer 2015, ISBN 978-3-319-22101-4 [contents] - 2014
- [j11]Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. J. Autom. Reason. 52(4): 451-480 (2014) - 2013
- [c27]Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formal Model and Correctness Proof for an Access Control Policy Framework. CPP 2013: 292-307 - [c26]Jian Xu, Xingyuan Zhang, Christian Urban:
Mechanising Turing Machines and Computability Theory in Isabelle/HOL. ITP 2013: 147-162 - 2012
- [j10]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. Log. Methods Comput. Sci. 8(2) (2012) - [j9]Maribel Fernández, Christian Urban:
Preface: Theory and Applications of Abstraction, Substitution and Naming. J. Autom. Reason. 49(2): 111-114 (2012) - [c25]Xingyuan Zhang, Christian Urban, Chunhan Wu:
Priority Inheritance Protocol Proved Correct. ITP 2012: 217-232 - 2011
- [j8]Chunhan Wu, Xingyuan Zhang, Christian Urban:
The Myhill-Nerode Theorem Based on Regular Expressions. Arch. Formal Proofs 2011 (2011) - [j7]Christian Urban, James Cheney, Stefan Berghofer:
Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2): 15:1-15:42 (2011) - [c24]James Cheney, Christian Urban:
Mechanizing the Metatheory of mini-XQuery. CPP 2011: 280-295 - [c23]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP 2011: 480-500 - [c22]Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). ITP 2011: 341-356 - [c21]Cezary Kaliszyk, Christian Urban:
Quotients revisited for Isabelle/HOL. SAC 2011: 1639-1644 - 2010
- [c20]Brian Huffman, Christian Urban:
A New Foundation for Nominal Isabelle. ITP 2010: 35-50 - [c19]Christian Urban:
Nominal Unification Revisited. UNIF 2010: 1-11
2000 – 2009
- 2009
- [e2]Andreas Abel, Christian Urban:
Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008. Electronic Notes in Theoretical Computer Science 228, Elsevier 2009 [contents] - [e1]Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel:
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, ISBN 978-3-642-03358-2 [contents] - 2008
- [j6]Christian Urban:
Nominal Techniques in Isabelle/HOL. J. Autom. Reason. 40(4): 327-356 (2008) - [j5]James Cheney, Christian Urban:
Nominal logic programming. ACM Trans. Program. Lang. Syst. 30(5): 26:1-26:47 (2008) - [c18]Peter Chapman, James McKinna, Christian Urban:
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus 2008: 38-52 - [c17]Christian Urban, James Cheney, Stefan Berghofer:
Mechanizing the Metatheory of LF. LICS 2008: 45-56 - [c16]Christian Urban, Bozhi Zhu:
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. RTA 2008: 409-424 - [c15]Stefan Berghofer, Christian Urban:
Nominal Inversion Principles. TPHOLs 2008: 71-85 - [c14]Andreas Abel, Christian Urban:
Preface. LFMTP@LICS 2008: 1 - [c13]Christian Urban, Julien Narboux:
Formal SOS-Proofs for the Lambda-Calculus. LSFA 2008: 139-155 - [i2]Christian Urban, James Cheney, Stefan Berghofer:
Mechanizing the Metatheory of LF. CoRR abs/0804.1667 (2008) - 2007
- [c12]Christian Urban, Stefan Berghofer, Michael Norrish:
Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50 - [c11]Julien Narboux, Christian Urban:
Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. LFMTP@CADE 2007: 3-18 - 2006
- [j4]Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban:
Categorical proof theory of classical propositional calculus. Theor. Comput. Sci. 364(2): 146-165 (2006) - [c10]Christian Urban, Stefan Berghofer:
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR 2006: 498-512 - [c9]Stefan Berghofer, Christian Urban:
A Head-to-Head Comparison of de Bruijn Indices and Names. LFMTP@FLoC 2006: 53-67 - [i1]James Cheney, Christian Urban:
Nominal Logic Programming. CoRR abs/cs/0609062 (2006) - 2005
- [c8]Christian Urban, Christine Tasson:
Nominal Techniques in Isabelle/HOL. CADE 2005: 38-53 - [c7]Christian Urban, Michael Norrish:
A formal treatment of the barendregt variable convention in rule inductions. MERLIN 2005: 25-32 - [c6]Christian Urban, James Cheney:
Avoiding Equivariance in Alpha-Prolog. TLCA 2005: 401-416 - 2004
- [j3]Christian Urban, Andrew M. Pitts, Murdoch Gabbay:
Nominal unification. Theor. Comput. Sci. 323(1-3): 473-497 (2004) - [c5]James Cheney, Christian Urban:
alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. ICLP 2004: 269-283 - 2003
- [j2]Roy Dyckhoff, Christian Urban:
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. J. Log. Comput. 13(5): 689-706 (2003) - [c4]Christian Urban, Andrew M. Pitts, Murdoch Gabbay:
Nominal Unificaiton. CSL 2003: 513-527 - 2001
- [j1]Christian Urban, Gavin M. Bierman:
Strong Normalisation of Cut-Elimination in Classical Logic. Fundam. Informaticae 45(1-2): 123-155 (2001) - [c3]Christian Urban:
Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. TLCA 2001: 415-430
1990 – 1999
- 1999
- [c2]Christian Urban, Gavin M. Bierman:
Strong Normalisation of Cut-Elimination in Classical Logic. TLCA 1999: 365-380 - 1998
- [c1]Christian Urban:
Implementation of Proof Search in the Imperative Programming Language Pizza. TABLEAUX 1998: 313-319
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 21:12 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
