×
Author ID: urban.christian Recent zbMATH articles by "Urban, Christian"
Published as: Urban, Christian
External Links: MGP

Publications by Year

Citations contained in zbMATH Open

32 Publications have been cited 337 times in 198 Documents Cited by Year
Nominal unification. Zbl 1078.68140
Urban, Christian; Pitts, Andrew M.; Gabbay, Murdoch J.
60
2004
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
58
2008
Nominal techniques in Isabelle/HOL. Zbl 1135.68561
Urban, Christian; Tasson, Christine
26
2005
\(\alpha\)Prolog: a logic programming language with names, binding and \(\alpha\)-equivalence. Zbl 1104.68370
Cheney, James; Urban, Christian
21
2004
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
17
2012
Barendregt’s variable convention in rule inductions. Zbl 1213.03024
Urban, Christian; Berghofer, Stefan; Norrish, Michael
16
2007
Strong normalisation of cut-elimination in classical logic. Zbl 0982.03032
Urban, C.; Bierman, G. M.
15
2001
Nominal unification. Zbl 1116.03322
Urban, Christian; Pitts, Andrew; Gabbay, Murdoch
14
2003
Mechanizing the metatheory of LF. Zbl 1351.68250
Urban, Christian; Cheney, James; Berghofer, Stefan
14
2011
A recursion combinator for nominal datatypes implemented in Isabelle/HOL. Zbl 1222.68374
Urban, Christian; Berghofer, Stefan
12
2006
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
10
2011
A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). Zbl 1342.68306
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian
10
2011
Mechanising Turing machines and computability theory in Isabelle/HOL. Zbl 1317.68237
Xu, Jian; Zhang, Xingyuan; Urban, Christian
10
2013
A head-to-head comparison of de Bruijn indices and names. Zbl 1278.03033
Berghofer, Stefan; Urban, Christian
8
2007
Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Zbl 1036.03036
Dyckhoff, Roy; Urban, Christian
6
2003
A new foundation for Nominal Isabelle. Zbl 1291.68350
Huffman, Brian; Urban, Christian
6
2010
A formalisation of the Myhill-Nerode theorem based on regular expressions. Zbl 1314.68179
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian
6
2014
Categorical proof theory of classical propositional calculus. Zbl 1121.03086
Bellin, Gianluigi; Hyland, Martin; Robinson, Edmund; Urban, Christian
5
2006
Nominal inversion principles. Zbl 1165.68448
Berghofer, Stefan; Urban, Christian
5
2008
Avoiding equivariance in Alpha-Prolog. Zbl 1114.68027
Urban, Christian; Cheney, James
5
2005
Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. Zbl 1339.03051
Urban, Christian
5
2014
Revisiting cut-elimination: One difficult proof is really a proof. Zbl 1146.68041
Urban, Christian; Zhu, Bozhi
4
2008
Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. Zbl 1278.68276
Narboux, Julien; Urban, Christian
4
2008
Strong normalisation of cut-elimination in classical logic. Zbl 0934.03074
Urban, C.; Bierman, G. M.
3
1999
Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Zbl 1173.68002
3
2009
POSIX lexing with derivatives of regular expressions (proof pearl). Zbl 1478.68118
Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian
3
2016
Strong normalisation for a Gentzen-like cut-elimination procedure. Zbl 0981.03058
Urban, Christian
2
2001
Nominal verification of algorithm \(W\). Zbl 1195.68118
Urban, Christian; Nipkow, Tobias
2
2009
Priority inheritance protocol proved correct. Zbl 1360.68772
Zhang, Xingyuan; Urban, Christian; Wu, Chunhan
2
2012
Formal SOS-proofs for the \(\lambda\)-calculus. Zbl 1310.68184
Urban, Christian; Narboux, Julien
1
2009
Mechanising a proof of Craig’s interpolation theorem for intuitionistic logic in nominal Isabelle. Zbl 1166.68340
Chapman, Peter; McKinna, James; Urban, Christian
1
2008
Mechanizing the metatheory of mini-XQuery. Zbl 1350.68054
Cheney, James; Urban, Christian
1
2011
POSIX lexing with derivatives of regular expressions (proof pearl). Zbl 1478.68118
Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian
3
2016
A formalisation of the Myhill-Nerode theorem based on regular expressions. Zbl 1314.68179
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian
6
2014
Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. Zbl 1339.03051
Urban, Christian
5
2014
Mechanising Turing machines and computability theory in Isabelle/HOL. Zbl 1317.68237
Xu, Jian; Zhang, Xingyuan; Urban, Christian
10
2013
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
17
2012
Priority inheritance protocol proved correct. Zbl 1360.68772
Zhang, Xingyuan; Urban, Christian; Wu, Chunhan
2
2012
Mechanizing the metatheory of LF. Zbl 1351.68250
Urban, Christian; Cheney, James; Berghofer, Stefan
14
2011
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
10
2011
A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). Zbl 1342.68306
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian
10
2011
Mechanizing the metatheory of mini-XQuery. Zbl 1350.68054
Cheney, James; Urban, Christian
1
2011
A new foundation for Nominal Isabelle. Zbl 1291.68350
Huffman, Brian; Urban, Christian
6
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.68118
Urban, Christian; Nipkow, Tobias
2
2009
Formal SOS-proofs for the \(\lambda\)-calculus. Zbl 1310.68184
Urban, Christian; Narboux, Julien
1
2009
Nominal techniques in Isabelle/HOL. Zbl 1140.68061
Urban, Christian
58
2008
Nominal inversion principles. Zbl 1165.68448
Berghofer, Stefan; Urban, Christian
5
2008
Revisiting cut-elimination: One difficult proof is really a proof. Zbl 1146.68041
Urban, Christian; Zhu, Bozhi
4
2008
Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. Zbl 1278.68276
Narboux, Julien; Urban, Christian
4
2008
Mechanising a proof of Craig’s interpolation theorem for intuitionistic logic in nominal Isabelle. Zbl 1166.68340
Chapman, Peter; McKinna, James; Urban, Christian
1
2008
Barendregt’s variable convention in rule inductions. Zbl 1213.03024
Urban, Christian; Berghofer, Stefan; Norrish, Michael
16
2007
A head-to-head comparison of de Bruijn indices and names. Zbl 1278.03033
Berghofer, Stefan; Urban, Christian
8
2007
A recursion combinator for nominal datatypes implemented in Isabelle/HOL. Zbl 1222.68374
Urban, Christian; Berghofer, Stefan
12
2006
Categorical proof theory of classical propositional calculus. Zbl 1121.03086
Bellin, Gianluigi; Hyland, Martin; Robinson, Edmund; Urban, Christian
5
2006
Nominal techniques in Isabelle/HOL. Zbl 1135.68561
Urban, Christian; Tasson, Christine
26
2005
Avoiding equivariance in Alpha-Prolog. Zbl 1114.68027
Urban, Christian; Cheney, James
5
2005
Nominal unification. Zbl 1078.68140
Urban, Christian; Pitts, Andrew M.; Gabbay, Murdoch J.
60
2004
\(\alpha\)Prolog: a logic programming language with names, binding and \(\alpha\)-equivalence. Zbl 1104.68370
Cheney, James; Urban, Christian
21
2004
Nominal unification. Zbl 1116.03322
Urban, Christian; Pitts, Andrew; Gabbay, Murdoch
14
2003
Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Zbl 1036.03036
Dyckhoff, Roy; Urban, Christian
6
2003
Strong normalisation of cut-elimination in classical logic. Zbl 0982.03032
Urban, C.; Bierman, G. M.
15
2001
Strong normalisation for a Gentzen-like cut-elimination procedure. Zbl 0981.03058
Urban, Christian
2
2001
Strong normalisation of cut-elimination in classical logic. Zbl 0934.03074
Urban, C.; Bierman, G. M.
3
1999
all top 5

Cited by 235 Authors

19 Fernández, Maribel
19 Gabbay, Murdoch James
12 Urban, Christian
11 Ayala-Rincón, Mauricio
7 Nipkow, Tobias
7 Pitts, Andrew M.
7 Sobrinho, Daniele Nantes
6 Cheney, James
5 Calvès, Christophe
5 Kaliszyk, Cezary
5 Kikuchi, Kentaro
5 Norrish, Michael
5 Parrow, Joachim
5 Szasz, Nora
5 Tasistro, Alvaro
5 Traytel, Dmitry
4 Copello, Ernesto
4 de Carvalho-Segundo, Washington
4 Gacek, Andrew
4 Kutz, Yunus D. K.
4 Miller, Dale Allen
4 Popescu, Andrei
4 Rocha-Oliveira, Ana Cristina
4 Schmidt-Schauß, Manfred
4 Smolka, Gert
3 Aceto, Luca
3 Åman Pohjola, Johannes
3 Borgström, Johannes
3 Fábregas, Ignacio
3 Forster, Yannick
3 García-Pérez, Álvaro
3 Ingólfsdóttir, Anna
3 Lipton, James B.
3 Nadathur, Gopalan
3 Ortega-Mallén, Yolanda
3 Paulson, Lawrence Charles
3 Pollack, Randy
3 Sato, Masahiko
3 Wu, Chunhan
3 Zhang, Xingyuan
2 Abdulaziz, Mohammad
2 Aoto, Takahito
2 Asperti, Andrea
2 Bengtson, Jesper
2 Berghofer, Stefan
2 Blanchette, Jasmin Christian
2 Borisavljević, Mirjana
2 Chaudhuri, Kaustuv
2 Clouston, Ranald A.
2 Dawson, Jeremy E.
2 Doczkal, Christian
2 Dyckhoff, Roy
2 Foster, Simon
2 Gallego Arias, Emilio Jesús
2 Gheri, Lorenzo
2 Gretton, Charles
2 Keshvardoost, Khadijeh
2 Kesner, Delia
2 Kunčar, Ondřej
2 Kutsia, Temur
2 Lakin, Matthew R.
2 Larchey-Wendling, Dominique
2 Lengrand, Stéphane Jean Eric
2 Levy, Jordi
2 Lochbihler, Andreas
2 Mahmoudi, Mojgan
2 Mariño, Julio
2 Momigliano, Alberto
2 Pientka, Brigitte
2 Raabjerg, Palle
2 Reis, Giselle
2 Ricciotti, Wilmer
2 Roßkopf, Simon
2 Schmitt, Alan
2 Silva, Gabriel Ferreira
2 Sternagel, Christian
2 Struth, Georg
2 Thompson, Declan
2 Tiu, Alwen Fernanto
2 Urban, Josef
2 Vale, Deivid
2 Lima Ventura, Daniel
2 Villaret, Mateu
2 Weber, Tjark
1 Abel, Andreas M.
1 Aehlig, Klaus
1 Ahn, Ki Yung
1 Allais, Guillaume
1 Amato, Gianluca
1 Ambal, Guillaume
1 Armstrong, Alasdair
1 Ausaf, Fahad
1 Ayhan, Sara
1 Azevedo de Amorim, Arthur
1 Barendregt, Hendrik Pieter
1 Bayer, Jonas
1 Bellin, Gianluigi
1 Berger, Martin J.
1 Bickford, Mark
1 Bloo, Roel
...and 135 more Authors

Citations by Year