Christian Urban

Available identifiers

zbMath Open urban.christianMaRDI QIDQ860832

List of research outcomes

Publication	Date of Publication	Type
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
https://portal.mardi4nfdi.de/entity/Q2871859	2014-01-10	Paper
https://portal.mardi4nfdi.de/entity/Q2871867	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Christian Urban