|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 22 occurrences of 16 keywords
|
|
|
|
|
Results
Found 35 publication records. Showing 35 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Chunhan Wu, Xingyuan Zhang, Christian Urban |
The Myhill-Nerode Theorem Based on Regular Expressions.  |
Archive of Formal Proofs  |
2011 |
DBLP BibTeX RDF |
|
| 1 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the metatheory of LF. |
ACM Trans. Comput. Log. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | James Cheney, Christian Urban |
Mechanizing the Metatheory of mini-XQuery. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Christian Urban |
Quotients revisited for Isabelle/HOL. |
SAC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Chunhan Wu, Xingyuan Zhang, Christian Urban |
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Cezary Kaliszyk |
General Bindings and Alpha-Equivalence in Nominal Isabelle. |
ESOP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban |
Nominal Unification Revisited |
UNIF |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Huffman, Christian Urban |
A New Foundation for Nominal Isabelle. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel, Christian Urban |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Julien Narboux |
Formal SOS-Proofs for the Lambda-Calculus. |
Electr. Notes Theor. Comput. Sci. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (eds.) |
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Julien Narboux, Christian Urban |
Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | James Cheney, Christian Urban |
Nominal logic programming. |
ACM Trans. Program. Lang. Syst. |
2008 |
DBLP DOI BibTeX RDF |
name-binding, semantics, logic programming, Nominal logic |
| 1 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the Metatheory of LF |
CoRR |
2008 |
DBLP BibTeX RDF |
|
| 1 | Christian Urban |
Nominal Techniques in Isabelle/HOL. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
Nominal logic work, Lambda-calculus, Theorem provers |
| 1 | Christian Urban, Bozhi Zhu |
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. |
RTA |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Christian Urban |
Nominal Inversion Principles. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Chapman, James McKinna, Christian Urban |
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. |
AISC/MKM/Calculemus |
2008 |
DBLP DOI BibTeX RDF |
Nominal Isabelle, logic, automated reasoning, Formal mathematics |
| 1 | Christian Urban, James Cheney, Stefan Berghofer |
Mechanizing the Metatheory of LF. |
LICS |
2008 |
DBLP DOI BibTeX RDF |
mechanized metatheory, logical frameworks, nominal logic |
| 1 | Stefan Berghofer, Christian Urban |
A Head-to-Head Comparison of de Bruijn Indices and Names. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Stefan Berghofer, Michael Norrish |
Barendregt's Variable Convention in Rule Inductions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban |
Categorical proof theory of classical propositional calculus. |
Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | James Cheney, Christian Urban |
Nominal Logic Programming |
CoRR |
2006 |
DBLP BibTeX RDF |
|
| 1 | Christian Urban, Stefan Berghofer |
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
Lambda-calculus, proof assistants, nominal logic, primitive recursion |
| 1 | Christian Urban, James Cheney |
Avoiding Equivariance in Alpha-Prolog. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Christine Tasson |
Nominal Techniques in Isabelle/HOL. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
theorem-assistants, Lambda-calculus, nominal logic, structural induction |
| 1 | Christian Urban, Michael Norrish |
A formal treatment of the barendregt variable convention in rule inductions. |
MERLIN |
2005 |
DBLP DOI BibTeX RDF |
POPLmark challenge, ?-calculus, nominal logic |
| 1 | Christian Urban, Andrew M. Pitts, Murdoch Gabbay |
Nominal unification. |
Theor. Comput. Sci. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | James Cheney, Christian Urban |
alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. |
ICLP |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Roy Dyckhoff, Christian Urban |
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. |
J. Log. Comput. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Andrew M. Pitts, Murdoch Gabbay |
Nominal Unificaiton. |
CSL |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Gavin M. Bierman |
Strong Normalisation of Cut-Elimination in Classical Logic. |
Fundam. Inform. |
2001 |
DBLP BibTeX RDF |
|
| 1 | Christian Urban |
Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
Recursive Path Ordering, Cut-Elimination, Explicit Substitution, Classical Logic |
| 1 | Christian Urban, Gavin M. Bierman |
Strong Normalisation of Cut-Elimination in Classical Logic. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban |
Implementation of Proof Search in the Imperative Programming Language Pizza. |
TABLEAUX |
1998 |
DBLP DOI BibTeX RDF |
Success Continuations, G4ip, Pizza |
Displaying result #1 - #35 of 35 (100 per page; Change: )
|
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")