Sciweavers

JAR
2010
95views more  JAR 2010»
13 years 5 months ago
Equivariant Unification
Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves ...
James Cheney
CORR
2010
Springer
105views Education» more  CORR 2010»
13 years 11 months ago
Nominal Unification from a Higher-Order Perspective
Abstract. Nominal Logic is an extension of first-order logic with equality, name-binding, name-swapping, and freshness of names. Contrarily to higher-order logic, bound variables a...
Jordi Levy, Mateu Villaret
TLCA
2005
Springer
14 years 4 months ago
Avoiding Equivariance in Alpha-Prolog
αProlog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed λ-calculi and many other languages involving...
Christian Urban, James Cheney
FOSSACS
2005
Springer
14 years 4 months ago
A Simpler Proof Theory for Nominal Logic
Abstract. Nominal logic is a variant of first-order logic equipped with a “freshname quantifier” N and other features useful for reasoning about languages with bound names. I...
James Cheney
PPDP
2007
Springer
14 years 5 months ago
Mechanized metatheory model-checking
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has r...
James Cheney, Alberto Momigliano