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

P+ → V-, V- → D, V- → V #29

Closed rogerburtonpatel closed 2 months ago

rogerburtonpatel commented 6 months ago

The three translations; two non-trivial. To do this:

  1. Formalize P+ and V- (with new judgement form, #21 and #24 )
  2. Translate P+ to V- in theory and code (#22 )
  3. Formalize Verse (implementation not yet needed, may collect from Verse people) (#18)
  4. Translate V- to Verse formally
  5. Finalize formalization of D
  6. Translate V- to D in theory and code (#18)

One wonder: Where does #19 fit into this story?

nrnrnr commented 6 months ago

19 is a prototype for item 6 on your list (translate V- to D)

rogerburtonpatel commented 4 months ago

P+ -> V- done, needs theory. V- -> V in the works, so is V- -> D.

rogerburtonpatel commented 2 months ago

Closing as too broad.