Edit Profile (opens in new tab) Urban, Christian Compute Distance To: Compute Author ID: urban.christian Published as: Urban, Christian External Links: MGP Documents Indexed: 33 Publications since 1999 4 Contributions as Editor Co-Authors: 23 Co-Authors with 32 Joint Publications 654 Co-Co-Authors all top 5 Co-Authors 3 single-authored 8 Zhang, Xingyuan 6 Berghofer, Stefan 5 Wu, Chunhan 4 Cheney, James 2 Bierman, Gavin M. 2 Dyckhoff, Roy 2 Gabbay, Murdoch James 2 Kaliszyk, Cezary 2 Narboux, Julien 2 Nipkow, Tobias 2 Pitts, Andrew M. 1 Abel, Andreas M. 1 Ausaf, Fahad 1 Bellin, Gianluigi 1 Chapman, Peter 1 Huffman, Brian 1 Hyland, J. Martin E. 1 McKinna, James 1 Norrish, Michael 1 Robinson, Edmund P. 1 Tasson, Christine 1 Wenzel, Makarius 1 Xu, Jian 1 Zhu, Bozhi all top 5 Serials 4 Journal of Automated Reasoning 2 Theoretical Computer Science 2 Lecture Notes in Computer Science 1 Journal of Logic and Computation 1 Fundamenta Informaticae 1 ACM Transactions on Computational Logic 1 Electronic Notes in Theoretical Computer Science 1 Logical Methods in Computer Science Fields 32 Computer science (68-XX) 16 Mathematical logic and foundations (03-XX) 4 General and overarching topics; collections (00-XX) 1 Category theory; homological algebra (18-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 31 Publications have been cited 289 times in 167 Documents Cited by ▼ Year ▼ Nominal unification. Zbl 1078.68140Urban, Christian; Pitts, Andrew M.; Gabbay, Murdoch J. 55 2004 Nominal techniques in Isabelle/HOL. Zbl 1140.68061Urban, Christian 52 2008 Nominal techniques in Isabelle/HOL. Zbl 1135.68561Urban, Christian; Tasson, Christine 20 2005 \(\alpha\)Prolog: a logic programming language with names, binding and \(\alpha\)-equivalence. Zbl 1104.68370Cheney, James; Urban, Christian 18 2004 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283Urban, Christian; Kaliszyk, Cezary 15 2012 Mechanizing the metatheory of LF. Zbl 1351.68250Urban, Christian; Cheney, James; Berghofer, Stefan 14 2011 Strong normalisation of cut-elimination in classical logic. Zbl 0982.03032Urban, C.; Bierman, G. M. 13 2001 Nominal unification. Zbl 1116.03322Urban, Christian; Pitts, Andrew; Gabbay, Murdoch 13 2003 Barendregt’s variable convention in rule inductions. Zbl 1213.03024Urban, Christian; Berghofer, Stefan; Norrish, Michael 13 2007 A recursion combinator for nominal datatypes implemented in Isabelle/HOL. Zbl 1222.68374Urban, Christian; Berghofer, Stefan 11 2006 A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). Zbl 1342.68306Wu, Chunhan; Zhang, Xingyuan; Urban, Christian 8 2011 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265Urban, Christian; Kaliszyk, Cezary 7 2011 A formalisation of the Myhill-Nerode theorem based on regular expressions. Zbl 1314.68179Wu, Chunhan; Zhang, Xingyuan; Urban, Christian 6 2014 A head-to-head comparison of de Bruijn indices and names. Zbl 1278.03033Berghofer, Stefan; Urban, Christian 6 2007 Mechanising Turing machines and computability theory in Isabelle/HOL. Zbl 1317.68237Xu, Jian; Zhang, Xingyuan; Urban, Christian 5 2013 A new foundation for Nominal Isabelle. Zbl 1291.68350Huffman, Brian; Urban, Christian 5 2010 Nominal inversion principles. Zbl 1165.68448Berghofer, Stefan; Urban, Christian 5 2008 Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Zbl 1036.03036Dyckhoff, Roy; Urban, Christian 5 2003 Avoiding equivariance in Alpha-Prolog. Zbl 1114.68027Urban, Christian; Cheney, James 4 2005 Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. Zbl 1339.03051Urban, Christian 4 2014 Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. Zbl 1278.68276Narboux, Julien; Urban, Christian 4 2008 Categorical proof theory of classical propositional calculus. Zbl 1121.03086Bellin, Gianluigi; Hyland, Martin; Robinson, Edmund; Urban, Christian 4 2006 Revisiting cut-elimination: One difficult proof is really a proof. Zbl 1146.68041Urban, Christian; Zhu, Bozhi 4 2008 Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002 3 2009 Strong normalisation of cut-elimination in classical logic. Zbl 0934.03074Urban, C.; Bierman, G. M. 2 1999 Nominal verification of algorithm \(W\). Zbl 1195.68118Urban, Christian; Nipkow, Tobias 2 2009 Strong normalisation for a Gentzen-like cut-elimination procedure. Zbl 0981.03058Urban, Christian 2 2001 Mechanizing the metatheory of mini-XQuery. Zbl 1350.68054Cheney, James; Urban, Christian 1 2011 POSIX lexing with derivatives of regular expressions (proof pearl). Zbl 1478.68118Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian 1 2016 Formal SOS-proofs for the \(\lambda\)-calculus. Zbl 1310.68184Urban, Christian; Narboux, Julien 1 2009 Priority inheritance protocol proved correct. Zbl 1360.68772Zhang, Xingyuan; Urban, Christian; Wu, Chunhan 1 2012 POSIX lexing with derivatives of regular expressions (proof pearl). Zbl 1478.68118Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian 1 2016 A formalisation of the Myhill-Nerode theorem based on regular expressions. Zbl 1314.68179Wu, Chunhan; Zhang, Xingyuan; Urban, Christian 6 2014 Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. Zbl 1339.03051Urban, Christian 4 2014 Mechanising Turing machines and computability theory in Isabelle/HOL. Zbl 1317.68237Xu, Jian; Zhang, Xingyuan; Urban, Christian 5 2013 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283Urban, Christian; Kaliszyk, Cezary 15 2012 Priority inheritance protocol proved correct. Zbl 1360.68772Zhang, Xingyuan; Urban, Christian; Wu, Chunhan 1 2012 Mechanizing the metatheory of LF. Zbl 1351.68250Urban, Christian; Cheney, James; Berghofer, Stefan 14 2011 A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). Zbl 1342.68306Wu, Chunhan; Zhang, Xingyuan; Urban, Christian 8 2011 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265Urban, Christian; Kaliszyk, Cezary 7 2011 Mechanizing the metatheory of mini-XQuery. Zbl 1350.68054Cheney, James; Urban, Christian 1 2011 A new foundation for Nominal Isabelle. Zbl 1291.68350Huffman, Brian; Urban, Christian 5 2010 Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002 3 2009 Nominal verification of algorithm \(W\). Zbl 1195.68118Urban, Christian; Nipkow, Tobias 2 2009 Formal SOS-proofs for the \(\lambda\)-calculus. Zbl 1310.68184Urban, Christian; Narboux, Julien 1 2009 Nominal techniques in Isabelle/HOL. Zbl 1140.68061Urban, Christian 52 2008 Nominal inversion principles. Zbl 1165.68448Berghofer, Stefan; Urban, Christian 5 2008 Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. Zbl 1278.68276Narboux, Julien; Urban, Christian 4 2008 Revisiting cut-elimination: One difficult proof is really a proof. Zbl 1146.68041Urban, Christian; Zhu, Bozhi 4 2008 Barendregt’s variable convention in rule inductions. Zbl 1213.03024Urban, Christian; Berghofer, Stefan; Norrish, Michael 13 2007 A head-to-head comparison of de Bruijn indices and names. Zbl 1278.03033Berghofer, Stefan; Urban, Christian 6 2007 A recursion combinator for nominal datatypes implemented in Isabelle/HOL. Zbl 1222.68374Urban, Christian; Berghofer, Stefan 11 2006 Categorical proof theory of classical propositional calculus. Zbl 1121.03086Bellin, Gianluigi; Hyland, Martin; Robinson, Edmund; Urban, Christian 4 2006 Nominal techniques in Isabelle/HOL. Zbl 1135.68561Urban, Christian; Tasson, Christine 20 2005 Avoiding equivariance in Alpha-Prolog. Zbl 1114.68027Urban, Christian; Cheney, James 4 2005 Nominal unification. Zbl 1078.68140Urban, Christian; Pitts, Andrew M.; Gabbay, Murdoch J. 55 2004 \(\alpha\)Prolog: a logic programming language with names, binding and \(\alpha\)-equivalence. Zbl 1104.68370Cheney, James; Urban, Christian 18 2004 Nominal unification. Zbl 1116.03322Urban, Christian; Pitts, Andrew; Gabbay, Murdoch 13 2003 Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Zbl 1036.03036Dyckhoff, Roy; Urban, Christian 5 2003 Strong normalisation of cut-elimination in classical logic. Zbl 0982.03032Urban, C.; Bierman, G. M. 13 2001 Strong normalisation for a Gentzen-like cut-elimination procedure. Zbl 0981.03058Urban, Christian 2 2001 Strong normalisation of cut-elimination in classical logic. Zbl 0934.03074Urban, C.; Bierman, G. M. 2 1999 all cited Publications top 5 cited Publications all top 5 Cited by 213 Authors 19 Gabbay, Murdoch James 18 Fernández, Maribel 11 Ayala-Rincón, Mauricio 9 Urban, Christian 7 Pitts, Andrew M. 7 Sobrinho, Daniele Nantes 6 Cheney, James 5 Kaliszyk, Cezary 5 Nipkow, Tobias 5 Norrish, Michael 5 Parrow, Joachim 5 Szasz, Nora 5 Tasistro, Alvaro 4 Calvès, Christophe 4 Copello, Ernesto 4 de Carvalho-Segundo, Washington 4 Kutz, Yunus D. K. 4 Miller, Dale Allen 4 Rocha-Oliveira, Ana Cristina 4 Schmidt-Schauß, Manfred 4 Traytel, Dmitry 3 Aceto, Luca 3 Åman Pohjola, Johannes 3 Borgström, Johannes 3 Fábregas, Ignacio 3 Gacek, Andrew 3 García-Pérez, Álvaro 3 Ingólfsdóttir, Anna 3 Kikuchi, Kentaro 3 Momigliano, Alberto 3 Nadathur, Gopalan 3 Paulson, Lawrence Charles 3 Pollack, Randy 3 Popescu, Andrei 3 Sato, Masahiko 3 Smolka, Gert 2 Abdulaziz, Mohammad 2 Aoto, Takahito 2 Bengtson, Jesper 2 Berghofer, Stefan 2 Chaudhuri, Kaustuv 2 Clouston, Ranald A. 2 Dawson, Jeremy E. 2 Doczkal, Christian 2 Dyckhoff, Roy 2 Forster, Yannick 2 Gretton, Charles 2 Keshvardoost, Khadijeh 2 Kesner, Delia 2 Lakin, Matthew R. 2 Lipton, James B. 2 Lochbihler, Andreas 2 Mahmoudi, Mojgan 2 Ortega-Mallén, Yolanda 2 Pientka, Brigitte 2 Raabjerg, Palle 2 Reis, Giselle 2 Ricciotti, Wilmer 2 Silva, Gabriel Ferreira 2 Struth, Georg 2 Tiu, Alwen Fernanto 2 Urban, Josef 2 Vale, Deivid 2 Lima Ventura, Daniel 2 Weber, Tjark 2 Wu, Chunhan 2 Zhang, Xingyuan 1 Abel, Andreas M. 1 Aehlig, Klaus 1 Ahn, Ki Yung 1 Allais, Guillaume 1 Amato, Gianluca 1 Ambal, Guillaume 1 Armstrong, Alasdair 1 Asperti, Andrea 1 Ausaf, Fahad 1 Ayhan, Sara 1 Azevedo de Amorim, Arthur 1 Barendregt, Hendrik Pieter 1 Bayer, Jonas 1 Berger, Martin J. 1 Bickford, Mark 1 Blanchette, Jasmin Christian 1 Bloo, Roel 1 Borisavljević, Mirjana 1 Bove, Ana 1 Brauner, Paul 1 Breitner, Joachim 1 Brown, Chad Edward 1 Brun, Matthias 1 Byrd, William E. 1 Calude, Cristian S. 1 Carneiro, Mario M. 1 Cave, Andrew 1 Cerrito, Serenella 1 Charguéraud, Arthur 1 Cimini, Matteo 1 Coecke, Bob 1 Coquand, Thierry 1 Crole, Roy L. ...and 113 more Authors all top 5 Cited in 25 Serials 28 Journal of Automated Reasoning 15 Theoretical Computer Science 11 MSCS. Mathematical Structures in Computer Science 10 Journal of Functional Programming 5 Information and Computation 5 Logical Methods in Computer Science 3 Annals of Pure and Applied Logic 2 Journal of Computer and System Sciences 2 Journal of Symbolic Computation 2 Formal Aspects of Computing 2 Higher-Order and Symbolic Computation 2 Journal of Logical and Algebraic Methods in Programming 1 Journal of Philosophical Logic 1 The Journal of Symbolic Logic 1 Indagationes Mathematicae. New Series 1 Journal of Applied Non-Classical Logics 1 The Bulletin of Symbolic Logic 1 Annals of Mathematics and Artificial Intelligence 1 Soft Computing 1 Fundamenta Informaticae 1 Theory and Practice of Logic Programming 1 Journal of Applied Logic 1 Logica Universalis 1 Journal of Formalized Reasoning 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 10 Fields 149 Computer science (68-XX) 86 Mathematical logic and foundations (03-XX) 5 Category theory; homological algebra (18-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 2 Information and communication theory, circuits (94-XX) 1 History and biography (01-XX) 1 General algebraic systems (08-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Mathematics education (97-XX) Citations by Year