search

rogerburtonpatel / vml

Code and proofs for Verse-ML, an equation-style sub-ml language. Part of an undergraduate senior thesis with Norman Ramsey, Milod Kazerounian, and Roger Burtonpatel.
5 stars 0 forks source link

Review core equation rules in V- #16

Closed rogerburtonpatel closed 7 months ago

rogerburtonpatel commented 7 months ago

Looking for thoughts on:

  1. Coverage: Do these rules cover what you consider to be important per what we've discussed in the language?
  2. Formatting: Is the first rule, Ge-Ctx-Stuck, sound with regards to premises being adjacent vs. above each other?
  3. Productive next steps: Would it be helpful to add rules for things like literals and value constructors, or focus my efforts on a more significant task like our termination, soundness, and completeness proofs?

https://github.com/rogerburtonpatel/vml/blob/main/tex/syntax-and-judgement/syntax-judgement-V-.pdf

Thanks!

nrnrnr commented 7 months ago
  1. The current representation of "temporarily stuck" definitely will not do. Otherwise I got bogged down with some questionable notation choices.
    1. The rule looks wrong (a \rho where it needs a \rhohat), but the rule looks well formed.
    2. Yes, I think you want a rule for value constructors. Value constructors can subsume literals, so no, no literals. Before adding more rules or attempting a proof, fix what you have.