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

[Divianszky Peter]

Thanks to all who helped me about fresh variables.

> You might be interested in the work of Christian Urban. He is developing
> a system to reason about proofs in higher-order logic  that takes
> special  care of the treatment of fresh variables. This is  work  along
> the lines of the  "nominal  approach"  introduced by Andrew Pitts.
>
> See http://www.mathematik.uni-muenchen.de/~urban/publications.html, for
> example "Nominal Reasoning Techniques in Isabelle/HOL".
>
> Steven Obua

That was a great help.

> There's much active work in this direction. Check the Merlin workshop's, for
> instance. There are implementions and libraries for both Haskell and OCaml.
>
> Bas

That is the same concept I think.

> It is indeed Pitts and Gabbay. They have a series of workshops on this
> stuff, one of which is coming up soon.

Indeed.
A. M. Pitts. Nominal Logic: A first order theory of names and binding.

Lately I am not sure that this is the concept which I need.
Thanks, anyway.

I enjoyed best the following paper:
  A Formal Treatment of the Barendregt Variable Convention in Rule
  Inductions
from
  http://www.mathematik.uni-muenchen.de/~urban/publications.html

Peter Divianszky