[FOM] Question about "fresh" variables/objects in logics

Andrej Bauer Andrej.Bauer at andrej.com
Sun Nov 27 05:18:51 EST 2005

Divianszky Peter wrote:
> Does anybody know of a formal description of the concept of "fresh"
> variable/object in logic?

You'd be better off asking computer scientists about this :-)

I believe you are looking for "nu calculus", which was (correct me if I
am wrong) proposed by A. Pitts and J. Gabbay. The paper I am aware of is

  A New Approach to Abstract Syntax Involving Binders (1999)
  Murdoch Gabbay, Andrew Pitts (LICS'99)

but there is probably an earlier one (it would be best to hear from
horse's mouth). They use permutation models of set theory to establish
their results. You may also look at the related work

  Marcelo Fiore, Gordon Plotkin and Daniele Turi
  Abstract Syntax and Variable Binding

For games semantics of nu calculus, search for "nominal games" by
S. Abramsky, D. Ghica, A. Murawski, L. Ong and I. Stark.

Depending on what you want to do, Aleksandar Nanevski's Ph.D. thesis
"Functional Programming with Names and Necessity" may also be of
interest, see http://www.eecs.harvard.edu/~aleks/thesis/thesis.ps
(references [PG00] and [Pit01] therein refer to Pitt's and Gabbay's
other relevant work).

Andrej Bauer

More information about the FOM mailing list