/resizing-reflection

Master Thesis with Nicolas Tabareau on Resizing Rules and Reflection

Primary LanguageCoq

Master Thesis with Nicolas Tabareau

Structure

  • quotient: My own implementation of quotient with resizing rules as axioms
  • rapport: Master Thesis (may be wrong)
  • reform: Formalization of the translation between MLTT + reflection and MLTT + axioms (given up)