Type Preservation for Mini-ML with References

This example specifies
  • the language of Mini-ML with references
  • the language of continuations
  • the typing rules
  • the evaluation rules
  • the implementation of type preservation
    • [ language | continuations | typing | evaluation | type preservation || MLref || LLF ]

    Frank Pfenning