EUFA

Liquid Types: Type System and Well-Formedness

Type Well-Formedness

\[\frac{0\le{n}\quad \Gamma;\nu:\langle{n}\rangle_i\vdash{a}}{\Gamma,h\vdash\{\nu:\langle{n}\rangle_i|a\}}\quad[WF-INT]\]



Abstract Block Well-Formedness


    With respect to local environment and preceding indices,

1. no two index bindings overlap, and
2. each type is well-formed

\[
   \frac{
      \begin{aligned}
      {{\Gamma,h}\vdash T}\qquad {Ind(n,T)\cap Dom(b)=\phi}  \\
      {x fresh}\qquad{\Gamma;x:T,h\vdash_Ab[x/@n]}
      \end{aligned}
   }{
      \Gamma, h\vdash_A{n:T,b}
   }
   \quad[WF-FIELD]
\]
\[
   \frac{
      \begin{aligned}
      {\Gamma,h\vdash{T}}\qquad
      {Ind(n^{+m},T)\cap Dom(b)=\phi} \qquad{\Gamma,h\vdash_A{b}}
      \end{aligned}
   }{
      \Gamma, h\vdash_A{n^{+m}:T,b}
   }
   \quad[WF-ARRAY]
\]