×
Compute Distance To:
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

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

Citations by Year