label-free -> labeled typing

Ayertienna / IS5

Intuitionistic S5 logic formalization

4 stars 0 forks source link

Closed Ayertienna closed 11 years ago

Ayertienna commented 12 years ago

If G |= w, Gamma |- M ::: A, then the result of translation satisfies types_L ....

Ayertienna commented 12 years ago

This depends on #30 - rewrite of the labeled language

Ayertienna commented 11 years ago

done