John Harrison wrote: > [...] > any in particular. However, in the terminology of my 1995 paper, Coq's > usual "reflection" would not be called reflection, being closer to the > "workarounds in higher order logic" you mentioned. The point is that > Coq reflection relies neither on new inference rules nor on extending > the implementation with new code. Rather, the existing resources of > the logic are used to define an internal syntactic "world" and the > mappings to and from the semantic objects, and the core > transformations are executed on the internal syntax inside the logic. >
John, I deeply appreciate your response and your slide show. At first I had trouble understanding the difference between what you called "syntax-semantics" mapping with the Goedel-related consistency assertion. I think the issue is now resolved and it was a pleasure to read. Thank you so much for your explanation. Reza. ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
