The next qualitative hurdle appears to be handling the mutual recursion that arises when we extend the language in other ways. To add case expressions, I need to represent case alternatives. Case alternatives contain expressions, and expressions contain (lists of) alternatives.

Unfortunately, with mutually recursive definitions, it appears that Coq can't automatically generate all the induction schemes I need. I could be wrong on this though, as I'm still a Coq newbie. I've figured out that the Coq command "Combined Schemes", will make

*some*of the schemes I might want, but it doesn't cover all of the use-cases. The problem (I think) is that although expressions are defined in terms of lists of alternatives, the lists themselves are polymorphic and aren't directly defined in terms of alternatives. For this reason, I can't convince "Combined Scheme" to make me a strong enough induction scheme, so I must write down and prove this myself.

At least, that's what I'm inferring from reading the proof of soundness for the STG machine described in a paper by Maciej Pirog and Dariusz Biernacki. I'm still working through it.

Hard Rock Casino Philadelphia - MapyRO

ReplyDeleteHard Rock Casino Philadelphia is 대구광역 출장안마 your 안성 출장마사지 North 상주 출장마사지 Philadelphia casino destination located in Chester, PA. Plan 김해 출장안마 your visit now to discover what it all boils down 세종특별자치 출장샵 to.