Once Again, The Americans Blow It...
I should have known the Eurozone would have done what I've been trying to do.
Update: I've now read the paper, and I was struck by how many things I had been failing to achieve that the authors of this paper also think are unachievable with a proof assistant. They selected a labeled transition system instead of a theory of structural congruence. At the end of section four, they explain why structural congruence is so painful (but cut and paste doesn't work, and I'm too sick with a ear/throat infection right now to transcribe all the math symbols by hand). Suffice to say, my understanding of why it doesn't work came at the expense of a lot of headache. I reproduced exactly those results with Twelf.
I also don't feel too bad about not succeeding. The problem is apparently not one for beginners. Consider the paragraph introducing section 4:
This is one of the most important sections of the present paper. In it we report a very substantial case-study of formal verification development in Coq, namely the theory of the π-calculus developed in [Milner92, section 2]. This enterprise is significant from various viewpoints. To our knowledge, it is one of the largest case-studies involving co-inductive types. But furthermore, it is perhaps the first serious attempt of using higher order syntax á la Church in metatheoretical studies outside type theory.
Okay, I don't feel too bad. I knew there were issue revolving around co-induction and higher-order syntax. I didn't know I was treading into a part of the mathematical landscape that has not been explored very deeply.
My Groups
-
Amnesty International Updated: 8 hours ago
-
Writers Hub Updated: 3 days ago
Neighborhood
Explore friends, family, friends & family, or entire neighborhood.
Comments