[FOM] Question about "fresh" variables/objects in logics
divip at aszt.inf.elte.hu
Tue Dec 20 10:02:47 EST 2005
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.
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.
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.
I enjoyed best the following paper:
A Formal Treatment of the Barendregt Variable Convention in Rule
More information about the FOM