Christian Urban

52 papers A* 1A 5B 12Misc 1Journal 19Unranked 12

Year	Rank	Type	Title / Venue / Authors
2023	B	`conf`	POSIX Lexing with Bitcoded Derivatives. ITP Chengsong Tan, Christian Urban
2023	J	`jnl`	POSIX Lexing with Derivatives of Regular Expressions. J. Autom. Reason. Christian Urban
2020	J	`jnl`	Priority Inheritance Protocol Proved Correct. J. Autom. Reason. Xingyuan Zhang, Christian Urban, Chunhan Wu
2019	J	`jnl`	Selected Extended Papers of ITP 2015: Preface. J. Autom. Reason. Xingyuan Zhang, Christian Urban
2019	J	`jnl`	Universal Turing Machine. Arch. Formal Proofs Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten
2017	A	`conf`	Modelling Homogeneous Generative Meta-Programming. ECOOP Martin Berger, Laurence Tratt, Christian Urban
2016	J	`jnl`	Modelling homogeneous generative meta-programming. CoRR Martin Berger, Laurence Tratt, Christian Urban
2016	B	`conf`	POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). ITP Fahad Ausaf, Roy Dyckhoff, Christian Urban
2016	J	`jnl`	POSIX Lexing with Derivatives of Regular Expressions. Arch. Formal Proofs Fahad Ausaf, Roy Dyckhoff, Christian Urban
2015	B	`ed.`	Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings ITP Christian Urban, Xingyuan Zhang
2014	J	`jnl`	A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. J. Autom. Reason. Chunhan Wu, Xingyuan Zhang, Christian Urban
2013	B	`conf`	A Formal Model and Correctness Proof for an Access Control Policy Framework. CPP Chunhan Wu, Xingyuan Zhang, Christian Urban
2013	B	`conf`	Mechanising Turing Machines and Computability Theory in Isabelle/HOL. ITP Jian Xu, Xingyuan Zhang, Christian Urban
2012	J	`jnl`	General Bindings and Alpha-Equivalence in Nominal Isabelle Log. Methods Comput. Sci. Christian Urban, Cezary Kaliszyk
2012	J	`jnl`	Preface: Theory and Applications of Abstraction, Substitution and Naming. J. Autom. Reason. Maribel Fernández, Christian Urban
2012	B	`conf`	Priority Inheritance Protocol Proved Correct. ITP Xingyuan Zhang, Christian Urban, Chunhan Wu
2011	B	`conf`	A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). ITP Chunhan Wu, Xingyuan Zhang, Christian Urban
2011	A	`conf`	General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP Christian Urban, Cezary Kaliszyk
2011	B	`conf`	Mechanizing the Metatheory of mini-XQuery. CPP James Cheney, Christian Urban
2011	J	`jnl`	Mechanizing the metatheory of LF. ACM Trans. Comput. Log. Christian Urban, James Cheney, Stefan Berghofer
2011	Misc	`conf`	Quotients revisited for Isabelle/HOL. SAC Cezary Kaliszyk, Christian Urban
2011	J	`jnl`	The Myhill-Nerode Theorem Based on Regular Expressions. Arch. Formal Proofs Chunhan Wu, Xingyuan Zhang, Christian Urban
2010	B	`conf`	A New Foundation for Nominal Isabelle. ITP Brian Huffman, Christian Urban
2010	—	`conf`	Nominal Unification Revisited UNIF Christian Urban
2009	—	`ed.`	Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008 LFMTP@LICS Andreas Abel, Christian Urban
2009	—	`ed.`	Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings TPHOLs Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel
2008	—	`conf`	Formal SOS-Proofs for the Lambda-Calculus. LSFA Christian Urban, Julien Narboux
2008	—	`conf`	Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. AISC/MKM/Calculemus Peter Chapman, James McKinna, Christian Urban
2008	J	`jnl`	Mechanizing the Metatheory of LF CoRR Christian Urban, James Cheney, Stefan Berghofer
2008	A*	`conf`	Mechanizing the Metatheory of LF. LICS Christian Urban, James Cheney, Stefan Berghofer
2008	—	`conf`	Nominal Inversion Principles. TPHOLs Stefan Berghofer, Christian Urban
2008	J	`jnl`	Nominal Techniques in Isabelle/HOL. J. Autom. Reason. Christian Urban
2008	J	`jnl`	Nominal logic programming. ACM Trans. Program. Lang. Syst. James Cheney, Christian Urban
2008	—	`conf`	Preface. LFMTP@LICS Andreas Abel, Christian Urban
2008	—	`conf`	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. RTA Christian Urban, Bozhi Zhu
2007	A	`conf`	Barendregt's Variable Convention in Rule Inductions. CADE Christian Urban, Stefan Berghofer, Michael Norrish
2007	—	`conf`	Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. LFMTP@CADE Julien Narboux, Christian Urban
2006	—	`conf`	A Head-to-Head Comparison of de Bruijn Indices and Names. LFMTP@FLoC Stefan Berghofer, Christian Urban
2006	A	`conf`	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR Christian Urban, Stefan Berghofer
2006	J	`jnl`	Categorical proof theory of classical propositional calculus. Theor. Comput. Sci. Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban
2006	J	`jnl`	Nominal Logic Programming CoRR James Cheney, Christian Urban
2005	—	`conf`	A formal treatment of the barendregt variable convention in rule inductions. MERLIN Christian Urban, Michael Norrish
2005	—	`conf`	Avoiding Equivariance in Alpha-Prolog. TLCA Christian Urban, James Cheney
2005	A	`conf`	Nominal Techniques in Isabelle/HOL. CADE Christian Urban, Christine Tasson
2004	J	`jnl`	Nominal unification. Theor. Comput. Sci. Christian Urban, Andrew M. Pitts, Murdoch Gabbay
2004	B	`conf`	alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. ICLP James Cheney, Christian Urban
2003	B	`conf`	Nominal Unificaiton. CSL Christian Urban, Andrew M. Pitts, Murdoch Gabbay
2003	J	`jnl`	Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. J. Log. Comput. Roy Dyckhoff, Christian Urban
2001	—	`conf`	Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. TLCA Christian Urban
2001	J	`jnl`	Strong Normalisation of Cut-Elimination in Classical Logic. Fundam. Informaticae Christian Urban, Gavin M. Bierman
1999	—	`conf`	Strong Normalisation of Cut-Elimination in Classical Logic. TLCA Christian Urban, Gavin M. Bierman
1998	B	`conf`	Implementation of Proof Search in the Imperative Programming Language Pizza. TABLEAUX Christian Urban