Zhang, Xingyuan; Urban, Christian; Wu, Chunhan Priority inheritance protocol proved correct. (English) Zbl 1468.68036 J. Autom. Reasoning 64, No. 1, 73-95 (2020). MSC: 68M20 68V15 PDFBibTeX XMLCite \textit{X. Zhang} et al., J. Autom. Reasoning 64, No. 1, 73--95 (2020; Zbl 1468.68036) Full Text: DOI
Ausaf, Fahad; Dyckhoff, Roy; Urban, Christian POSIX lexing with derivatives of regular expressions (proof pearl). (English) Zbl 1478.68118 Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 69-86 (2016). MSC: 68Q45 68Q42 68V20 68W32 PDFBibTeX XMLCite \textit{F. Ausaf} et al., Lect. Notes Comput. Sci. 9807, 69--86 (2016; Zbl 1478.68118) Full Text: DOI Link
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian A formal model and correctness proof for an access control policy framework. (English) Zbl 1426.68032 Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 292-307 (2013). MSC: 68M25 68V15 PDFBibTeX XMLCite \textit{C. Wu} et al., Lect. Notes Comput. Sci. 8307, 292--307 (2013; Zbl 1426.68032) Full Text: DOI
Xu, Jian; Zhang, Xingyuan; Urban, Christian Mechanising Turing machines and computability theory in Isabelle/HOL. (English) Zbl 1317.68237 Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 147-162 (2013). MSC: 68T15 68Q05 PDFBibTeX XMLCite \textit{J. Xu} et al., Lect. Notes Comput. Sci. 7998, 147--162 (2013; Zbl 1317.68237) Full Text: DOI
Zhang, Xingyuan; Urban, Christian; Wu, Chunhan Priority inheritance protocol proved correct. (English) Zbl 1360.68772 Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 217-232 (2012). MSC: 68T15 68M12 PDFBibTeX XMLCite \textit{X. Zhang} et al., Lect. Notes Comput. Sci. 7406, 217--232 (2012; Zbl 1360.68772) Full Text: DOI Link
Urban, Christian; Kaliszyk, Cezary General bindings and alpha-equivalence in Nominal Isabelle. (English) Zbl 1242.68283 Log. Methods Comput. Sci. 8, No. 2, Paper No. 14, 35 p. (2012). MSC: 68T15 PDFBibTeX XMLCite \textit{C. Urban} and \textit{C. Kaliszyk}, Log. Methods Comput. Sci. 8, No. 2, Paper No. 14, 35 p. (2012; Zbl 1242.68283) Full Text: DOI
Urban, Christian; Cheney, James; Berghofer, Stefan Mechanizing the metatheory of LF. (English) Zbl 1351.68250 ACM Trans. Comput. Log. 12, No. 2, Article No. 15, 42 p. (2011). MSC: 68T15 68N18 PDFBibTeX XMLCite \textit{C. Urban} et al., ACM Trans. Comput. Log. 12, No. 2, Article No. 15, 42 p. (2011; Zbl 1351.68250) Full Text: DOI arXiv
Cheney, James; Urban, Christian Mechanizing the metatheory of mini-XQuery. (English) Zbl 1350.68054 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 280-295 (2011). MSC: 68N15 68N18 68T15 PDFBibTeX XMLCite \textit{J. Cheney} and \textit{C. Urban}, Lect. Notes Comput. Sci. 7086, 280--295 (2011; Zbl 1350.68054) Full Text: DOI
Urban, Christian; Kaliszyk, Cezary General bindings and alpha-equivalence in Nominal Isabelle. (English) Zbl 1326.68265 Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 480-500 (2011). MSC: 68T15 68N15 PDFBibTeX XMLCite \textit{C. Urban} and \textit{C. Kaliszyk}, Lect. Notes Comput. Sci. 6602, 480--500 (2011; Zbl 1326.68265) Full Text: DOI arXiv
Huffman, Brian; Urban, Christian A new foundation for Nominal Isabelle. (English) Zbl 1291.68350 Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 35-50 (2010). MSC: 68T15 PDFBibTeX XMLCite \textit{B. Huffman} and \textit{C. Urban}, Lect. Notes Comput. Sci. 6172, 35--50 (2010; Zbl 1291.68350) Full Text: DOI
Urban, Christian; Narboux, Julien Formal SOS-proofs for the \(\lambda\)-calculus. (English) Zbl 1310.68184 Horizonte, Belo (ed.) et al., Proceedings of the 3rd workshop on logical and semantic frameworks, with applications (LSFA 2008), Salvador, Brazil, August 26, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 247, 139-155 (2009). MSC: 68T15 03B40 68Q55 68Q60 PDFBibTeX XMLCite \textit{C. Urban} and \textit{J. Narboux}, Electron. Notes Theor. Comput. Sci. 247, 139--155 (2009; Zbl 1310.68184) Full Text: DOI
Urban, Christian; Nipkow, Tobias Nominal verification of algorithm \(W\). (English) Zbl 1195.68118 Bertot, Yves (ed.) et al., From semantics to computer science. Essays in honour of Gilles Kahn. Cambridge: Cambridge University Press (ISBN 978-0-521-51825-3/hbk). 363-382 (2009). MSC: 68W40 68N17 68N18 68T15 68W05 PDFBibTeX XMLCite \textit{C. Urban} and \textit{T. Nipkow}, in: From semantics to computer science. Essays in honour of Gilles Kahn. Cambridge: Cambridge University Press. 363--382 (2009; Zbl 1195.68118)
Narboux, Julien; Urban, Christian Formalising in nominal Isabelle Crary’s completeness proof for equivalence checking. (English) Zbl 1278.68276 Pientka, B. (ed.) et al., Proceedings of the second international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2007), Bremen, Germany, July 15, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 196, 3-18 (2008). MSC: 68T15 03B35 03B70 PDFBibTeX XMLCite \textit{J. Narboux} and \textit{C. Urban}, Electron. Notes Theor. Comput. Sci. 196, 3--18 (2008; Zbl 1278.68276) Full Text: Link
Urban, Christian; Zhu, Bozhi Revisiting cut-elimination: One difficult proof is really a proof. (English) Zbl 1146.68041 Voronkov, Andrei (ed.), Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70588-8/pbk). Lecture Notes in Computer Science 5117, 409-424 (2008). MSC: 68Q42 03F05 03B35 68T15 PDFBibTeX XMLCite \textit{C. Urban} and \textit{B. Zhu}, Lect. Notes Comput. Sci. 5117, 409--424 (2008; Zbl 1146.68041) Full Text: DOI
Urban, Christian Nominal techniques in Isabelle/HOL. (English) Zbl 1140.68061 J. Autom. Reasoning 40, No. 4, 327-356 (2008). MSC: 68T15 03B40 PDFBibTeX XMLCite \textit{C. Urban}, J. Autom. Reasoning 40, No. 4, 327--356 (2008; Zbl 1140.68061) Full Text: DOI
Berghofer, Stefan; Urban, Christian A head-to-head comparison of de Bruijn indices and names. (English) Zbl 1278.03033 Momigliano, Alberto (ed.) et al., Proceedings of the first international workshop on logical frameworks and meta-languages: theory and practice (LFMTP 2006), Seattle, WA, USA, August 16, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 5, 53-67 (2007). MSC: 03B40 03B70 68T15 PDFBibTeX XMLCite \textit{S. Berghofer} and \textit{C. Urban}, Electron. Notes Theor. Comput. Sci. 174, No. 5, 53--67 (2007; Zbl 1278.03033) Full Text: Link
Urban, Christian; Berghofer, Stefan A recursion combinator for nominal datatypes implemented in Isabelle/HOL. (English) Zbl 1222.68374 Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 498-512 (2006). MSC: 68T15 68N18 PDFBibTeX XMLCite \textit{C. Urban} and \textit{S. Berghofer}, Lect. Notes Comput. Sci. 4130, 498--512 (2006; Zbl 1222.68374) Full Text: DOI
Urban, Christian; Tasson, Christine Nominal techniques in Isabelle/HOL. (English) Zbl 1135.68561 Nieuwenhuis, Robert (ed.), Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28005-7/pbk). Lecture Notes in Computer Science 3632. Lecture Notes in Artificial Intelligence, 38-53 (2005). MSC: 68T15 03B35 03B40 PDFBibTeX XMLCite \textit{C. Urban} and \textit{C. Tasson}, Lect. Notes Comput. Sci. 3632, 38--53 (2005; Zbl 1135.68561) Full Text: DOI