Christian Urban
Titel
Geciteerd door
Geciteerd door
Jaar
Nominal unification
C Urban, AM Pitts, MJ Gabbay
Theoretical Computer Science 323 (1-3), 473-497, 2004
2322004
Nominal techniques in Isabelle/HOL
C Urban
Journal of Automated Reasoning 40 (4), 327-356, 2008
1982008
Nominal techniques in Isabelle/HOL
C Urban, C Tasson
International Conference on Automated Deduction, 38-53, 2005
1382005
Classical logic and computation
C Urban
University of Cambridge, 2000
1322000
αProlog: A Logic Programming Language with Names, Binding and α-Equivalence
J Cheney, C Urban
International Conference on Logic Programming, 269-283, 2004
992004
Ancient Egyptian mummy genomes suggest an increase of Sub-Saharan African ancestry in post-Roman periods
VJ Schuenemann, A Peltzer, B Welte, WP Van Pelt, M Molak, CC Wang, ...
Nature communications 8 (1), 1-11, 2017
842017
Nominal logic programming
J Cheney, C Urban
ACM Transactions on Programming Languages and Systems (TOPLAS) 30 (5), 1-47, 2008
812008
Strong normalisation of cut-elimination in classical logic
C Urban, GM Bierman
Fundamenta Informaticae 45 (1-2), 123-155, 2001
802001
Barendregt’s variable convention in rule inductions
C Urban, S Berghofer, M Norrish
International Conference on Automated Deduction, 35-50, 2007
782007
General bindings and alpha-equivalence in Nominal Isabelle
C Urban, C Kaliszyk
European Symposium on Programming, 480-500, 2011
702011
Nominal unification
C Urban, A Pitts, M Gabbay
International Workshop on Computer Science Logic, 513-527, 2003
612003
A recursion combinator for nominal datatypes implemented in Isabelle/HOL
C Urban, S Berghofer
International Joint Conference on Automated Reasoning, 498-512, 2006
482006
Mechanizing the metatheory of LF
C Urban, J Cheney, S Berghofer
ACM Transactions on Computational Logic (TOCL) 12 (2), 1-42, 2011
412011
Measuring the equation of state of a hard-disc fluid
M Brunner, C Bechinger, U Herz, HH von Grünberg
EPL (Europhysics Letters) 63 (6), 791, 2003
38*2003
Quotients revisited for Isabelle/HOL
C Kaliszyk, C Urban
Proceedings of the 2011 ACM Symposium on Applied Computing, 1639-1644, 2011
362011
Mechanising turing machines and computability theory in Isabelle/HOL
J Xu, X Zhang, C Urban
International Conference on Interactive Theorem Proving, 147-162, 2013
342013
A head-to-head comparison of de Bruijn indices and names
S Berghofer, C Urban
Electronic Notes in Theoretical Computer Science 174 (5), 53-67, 2007
342007
A formalisation of the Myhill-Nerode theorem based on regular expressions
C Wu, X Zhang, C Urban
Journal of automated reasoning 52 (4), 451-480, 2014
33*2014
A new foundation for Nominal Isabelle
B Huffman, C Urban
International Conference on Interactive Theorem Proving, 35-50, 2010
332010
Ancient genomes reveal a high diversity of Mycobacterium leprae in medieval Europe
VJ Schuenemann, C Avanzi, B Krause-Kyora, A Seitz, A Herbig, S Inskip, ...
PLoS pathogens 14 (5), e1006997, 2018
322018
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20