Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home FreshML Research Project
Computer Laboratory > Andrew Pitts > FreshML Research Project > Publications

FreshML project publications

Fresh Objective Caml

M.R. Shinwell and A.M. Pitts, Fresh Objective Caml User Manual. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621, February 2005.

M.R.Shinwell, The Fresh Approach: functional programming with names and binders. PhD thesis, University of Cambridge Computer Laboratory, February 2005.

M. R. Shinwell, A.M. Pitts and M.J.Gabbay, FreshML: Programmming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263-274 (ACM Press, 2003). Please note the erratum to this paper.

M. R. Shinwell, Swapping the Atom: Programming with Binders in Fresh O'Caml. In Second ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding, MERLIN'03, Uppsala, Sweden, August 2003.

A. M. Pitts and M. J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming. In R. Backhouse and J. N. Oliveira (Eds), Mathematics of Programme Construction.5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings. Lecture Notes in Computer Science, Volume 1837 (Springer-Verlag, 2000), pages 230-255.

Nominal sets and logic

A.M. Pitts, Nominal Logic, A First Order Theory of Names and Binding, Information and Computation 186(2003) 165-193. Special issue on TACS2001.

M. J. Gabbay The π-calculus in FM. In: Fairouz Kamareddine (ed.), Thirty Five Years of Automating Mathematics, Kluwer Applied Logic series. Volume 28. Pages 71-123. Kluwer Academic Publishers. November 2003. ISBN 1-4020-1656-5.

M. J. Gabbay Automating Fraenkel-Mostowski Syntax. In Track B Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), Hampton, Virginia, USA. NASA Langley Research Center Report NASA/CP-2002-211736, pages 60-70.

M. J. Gabbay FM-HOL, a Higher-Order theory of names. In F. Kamareddine (Ed.) Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot Watt, UK, April 2002.

M. J. Gabbay and A.M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing 13(2002)341-363, special issue in honour of Rod Burstall.

M. J. Gabbay, A Theory of Inductive Definitions with Alpha-Equivalence. PhD thesis, Cambridge University, 2001.

Nominal domain theory

M.R. Shinwell and A.M. Pitts, On a Monadic Semantics for Freshness, Theoretical Computer Science, 2005 (to appear). (A preliminary version appeared in Second workshop of FP5 IST thematic network IST-2001-38957 APPSEM II, Tallinn, Estonia, April 2004.)

Nominal unification

C.Urban, A.M. Pitts and M.J.Gabbay, Nominal Unification. Theoretical Computer Science 323(2004) 473-497.

J.Cheney and C.Urban, System Description: alpha-Prolog, a Fresh Approach to Logic Programming Modulo alpha-Equivalence. In J.Levy, M.Kohlhase, J.Niehren and M. Villaret (Eds), Proceedings of the 17th International Workshop on Unification, UNIF'03, Valencia, Spain, June 8-9, 2003. Technical Report DSIC-II/12/03, Departamento de Sistemas Informaticos y Computacion, Universidad Politecnica de Valencia, 2003.