Dear Rasmus, Well, it wasn't all that serious a suggestion - there isn't actually a publically available theorem prover in reflect at the moment, although Intel have one. But it is interesting to know of your research as a potential user of this kind of idea.
Tom -----Original Message----- From: Rasmus Lerchedahl Petersen [mailto:[email protected]] Sent: 01 October 2010 00:42 To: Thomas Melham Cc: Tjark Weber; [email protected] Subject: Re: [Hol-info] Substitutions in formulae Dear Tom, > Or you could use a logic based on a lambda-calculus with reflection: > > http://www.comlab.ox.ac.uk/tom.melham/pub/Grundy-2006-RFL.pdf thank you for this interesting article. I may not be able to switch platform for my current project, but it is certainly nice to know about this for future reference :-) best Rasmus ------------------------------------------------------------------------------ Start uncovering the many advantages of virtual appliances and start using them to simplify application deployment and accelerate your shift to cloud computing. http://p.sf.net/sfu/novell-sfdev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
