Christian Urban

Available identifiers

zbMath Open urban.christianMaRDI QIDQ860832

List of research outcomes

Publication	Date of Publication	Type
POSIX lexing with bitcoded derivatives	2024-11-26	Paper
POSIX lexing with derivatives of regular expressions	2023-08-04	Paper
Priority inheritance protocol proved correct	2020-03-03	Paper
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)	2016-10-27	Paper
Mechanizing the metatheory of LF	2015-09-17	Paper
A formalisation of the Myhill-Nerode theorem based on regular expressions	2015-06-23	Paper
Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation	2015-05-22	Paper
Formal SOS-Proofs for the Lambda-Calculus	2015-03-18	Paper
A Formal Model and Correctness Proof for an Access Control Policy Framework	2015-01-13	Paper
A head-to-head comparison of de Bruijn indices and names	2014-01-10	Paper
Formalising in nominal Isabelle Crary's completeness proof for equivalence checking	2014-01-10	Paper
Mechanising Turing Machines and Computability Theory in Isabelle/HOL	2013-08-07	Paper
Priority Inheritance Protocol Proved Correct	2012-09-20	Paper
General bindings and alpha-equivalence in Nominal Isabelle	2012-07-03	Paper
Mechanizing the Metatheory of mini-XQuery	2011-11-22	Paper
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)	2011-08-17	Paper
General Bindings and Alpha-Equivalence in Nominal Isabelle	2011-05-19	Paper
A New Foundation for Nominal Isabelle	2010-09-14	Paper
https://portal.mardi4nfdi.de/entity/Q3400637	2010-02-05	Paper
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL	2009-03-12	Paper
Barendregt’s Variable Convention in Rule Inductions	2009-03-06	Paper
Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle	2009-01-27	Paper
Nominal Inversion Principles	2008-12-04	Paper
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof	2008-08-28	Paper
Nominal techniques in Isabelle/HOL	2008-06-11	Paper
Computer Science Logic	2007-06-21	Paper
Categorical proof theory of classical propositional calculus	2007-01-09	Paper
Automated Deduction – CADE-20	2006-11-01	Paper
Typed Lambda Calculi and Applications	2005-11-11	Paper
Logic Programming	2005-08-26	Paper
Nominal unification	2004-10-01	Paper
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation	2004-01-28	Paper
https://portal.mardi4nfdi.de/entity/Q2778837	2002-03-21	Paper

Research outcomes over time

This page was built for person: Christian Urban