74 citations · 88 across the 3 of their papers we have counts for
5 papers
Modelling homogeneous generative meta-programming
Martin Berger, Laurence Tratt, Christian Urban
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present the first foundational calculus which can model p…
General Bindings and Alpha-Equivalence in Nominal Isabelle
Christian Urban, Cezary Kaliszyk
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving nam…
Nominal Unification Revisited
Christian Urban
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's hi…
Mechanizing the Metatheory of LF
Christian Urban, James Cheney, Stefan Berghofer
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as pr…
Nominal Logic Programming
James Cheney, Christian Urban
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names…