Publications

C. Calves, M. Fernandez. Matching and Alpha-Equivalence Check for Nominal Terms. Journal of Computer and System Sciences, 2009. Special issue: Selected papers from WOLLIC 2008. Elsevier.
[DOI: http://dx.doi.org/10.1016/j.jcss.2009.10.003]

M. R. Lakin and A. M. Pitts, Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. In 18th European Symposium on Programming (ESOP 2009), York, UK, Lecture Notes in Computer Science, Volume 5502, pages 47-61 (Springer-Verlag, 2009).
[DOI: http://dx.doi.org/10.1007/978-3-642-00590-9_4]

A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names, Logical Methods in Computer Science, Vol. 4 (1:4) 2008, pp. 1-33.
[DOI: http://dx.doi.org/10.2168/LMCS-4(1:4)2008]

C. Calves, M. Fernandez. A polynomial nominal unification algorithm. Theoretical Computer Science, Elsevier, 2008.
[DOI: http://dx.doi.org/10.1016/j.tcs.2008.05.012]

C. Calves, M. Fernandez. Matching and Alpha-Equivalence Check for Nominal Terms with Variables and Permutations. Proceedings WOLLIC 2008, LNAI, Springer. pdf © 2008 Springer

M. R. Lakin and A. M. Pitts, A Metalanguage for Structural Operational Semantics. In M. T. Morazan (ed.), Trends in Functional Programming Volume 8, selected papers from the Eighth Symposium on Trends in Functional Programming (TFP 2007), New York, USA, April 2007, pages 19-35 (Intellect, 2008).

M. Fernandez, M.J. Gabbay. Nominal Rewriting. Information and Computation 205:917-965, 2007.

M. Fernandez and M.J. Gabbay. Curry style types for nominal terms. Proceedings of TYPES 2006, Lecture Notes in Computer Science, 2007. pdf © 2007 Springer

C. Calves, M. Fernandez. Implementing Nominal Unification. 3rd Int. Workshop on Term Graph Rewriting (TERMGRAPH'06), Vienna, 2006. Electronic Notes in Theoretical Computer Science. pdf © 2007 Elsevier, software (tar file).

R. A. Clouston and A. M. Pitts, Nominal Equational Logic. In L. Cardelli, M. Fiore and G. Winskel (eds) Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science, Volume 1496 (Elsevier, 2007). pdf © 2007 Elsevier B.V.

A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names. In 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, pages 85-95 (ACM Press, 2007). pdf © ACM 2007

A. M. Pitts, Alpha-Structural Recursion and Induction, Journal of the ACM 53(2006)459-506. pdf © ACM 2006