\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

The Module System

The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as a means of massive abstraction.

Modules and module types

Access path. An access path is denoted by \(p\) and can be either a module variable \(X\) or, if \(p′\) is an access path and \(id\) an identifier, then \(p′.id\) is an access path.

Structure element. A structure element is denoted by \(e\) and is either a definition of a constant, an assumption, a definition of an inductive, a definition of a module, an alias of a module or a module type abbreviation.

Structure expression. A structure expression is denoted by \(S\) and can be:

  • an access path \(p\)
  • a plain structure \(\Struct~e ; … ; e~\End\)
  • a functor \(\Functor(X:S)~S′\), where \(X\) is a module variable, \(S\) and \(S′\) are structure expressions
  • an application \(S~p\), where \(S\) is a structure expression and \(p\) an access path
  • a refined structure \(S~\with~p := p\)′ or \(S~\with~p := t:T\) where \(S\) is a structure expression, \(p\) and \(p′\) are access paths, \(t\) is a term and \(T\) is the type of \(t\).

Module definition. A module definition is written \(\Mod{X}{S}{S'}\) and consists of a module variable \(X\), a module type \(S\) which can be any structure expression and optionally a module implementation \(S′\) which can be any structure expression except a refined structure.

Module alias. A module alias is written \(\ModA{X}{p}\) and consists of a module variable \(X\) and a module path \(p\).

Module type abbreviation. A module type abbreviation is written \(\ModType{Y}{S}\), where \(Y\) is an identifier and \(S\) is any structure expression .

Typing Modules

In order to introduce the typing system we first slightly extend the syntactic class of terms and environments given in section The terms. The environments, apart from definitions of constants and inductive types now also hold any other structure elements. Terms, apart from variables, constants and complex terms, include also access paths.

We also need additional typing judgments:

  • \(\WFT{E}{S}\), denoting that a structure \(S\) is well-formed,
  • \(\WTM{E}{p}{S}\), denoting that the module pointed by \(p\) has type \(S\) in environment \(E\).
  • \(\WEV{E}{S}{\ovl{S}}\), denoting that a structure \(S\) is evaluated to a structure \(S\) in weak head normal form.
  • \(\WS{E}{S_1}{S_2}\) , denoting that a structure \(S_1\) is a subtype of a structure \(S_2\).
  • \(\WS{E}{e_1}{e_2}\) , denoting that a structure element e_1 is more precise than a structure element e_2.

The rules for forming structures are the following:

WF-STR
\[\frac{% \WF{E;E′}{}% }{% \WFT{E}{ \Struct~E′ ~\End}% }\]
WF-FUN
\[\frac{% \WFT{E; \ModS{X}{S}}{ \ovl{S′} }% }{% \WFT{E}{ \Functor(X:S)~S′}% }\]

Evaluation of structures to weak head normal form:

WEVAL-APP
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\% \hspace{3em}% \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}}% \hspace{3em}% \end{array}% }{% \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}}% }\end{split}\]

In the last rule, \(\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}\) is the resulting substitution from the inlining mechanism. We substitute in \(S\) the inlined fields \(p_i .c_i\) from \(\ModS{X}{S_1 }\) by the corresponding delta- reduced term \(t_i\) in \(p\).

WEVAL-WITH-MOD
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~% \hspace{3em}% E[] ⊢ p : S_2 \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~x := p}{}\\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End% \hspace{3em}% \end{array}% }\end{split}\]
WEVAL-WITH-MOD-REC
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := p_1}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};e_{i+2} \{p_1 /X_1.p\} ;…;e_n \{p_1 /X_1.p\} ~\End% \hspace{3em}% \end{array}% }\end{split}\]
WEVAL-WITH-DEF
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~c := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]
WEVAL-WITH-DEF-REC
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]
WEVAL-PATH-MOD1
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% E[] ⊢ p.X \lra \ovl{S}% }\end{split}\]
WEVAL-PATH-MOD2
\[\frac{% \WF{E}{}% \hspace{3em}% \Mod{X}{S}{S_1}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]
WEVAL-PATH-ALIAS1
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.X}{\ovl{S}}% }\end{split}\]
WEVAL-PATH-ALIAS2
\[\frac{% \WF{E}{}% \hspace{3em}% \ModA{X}{p_1 }∈ E% \hspace{3em}% \WEV{E}{p_1}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]
WEVAL-PATH-TYPE1
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.Y}{\ovl{S}}% }\end{split}\]
WEVAL-PATH-TYPE2
\[\frac{% \WF{E}{}% \hspace{3em}% \ModType{Y}{S}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{Y}{\ovl{S}}% }\]

Rules for typing module:

MT-EVAL
\[\frac{% \WEV{E}{p}{\ovl{S}}% }{% E[] ⊢ p : \ovl{S}% }\]
MT-STR
\[\frac{% E[] ⊢ p : S% }{% E[] ⊢ p : S/p% }\]

The last rule, called strengthening is used to make all module fields manifestly equal to themselves. The notation \(S/p\) has the following meaning:

  • if \(S\lra~\Struct~e_1 ;…;e_n ~\End\) then \(S/p=~\Struct~e_1 /p;…;e_n /p ~\End\) where \(e/p\) is defined as follows (note that opaque definitions are processed as assumptions):

    • \(\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}\)
    • \(\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}\)
    • \(\ModS{X}{S}/p = \ModA{X}{p.X}\)
    • \(\ModA{X}{p′}/p = \ModA{X}{p′}\)
    • \(\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}\)
    • \(\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}\)

  • if \(S \lra \Functor(X:S′)~S″\) then \(S/p=S\)

The notation \(\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}\) denotes an inductive definition that is definitionally equal to the inductive definition in the module denoted by the path \(p\). All rules which have \(\Ind{}{Γ_P}{Γ_C}{Γ_I}\) as premises are also valid for \(\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}\). We give the formation rule for \(\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}\) below as well as the equality rules on inductive types and constructors.

The module subtyping rules:

MSUB-STR
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\% \hspace{3em}% σ : \{1… m\} → \{1… n\} ~\injective% \hspace{3em}% \end{array}% }{% \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End}% }\end{split}\]
MSUB-FUN
\[\frac{% \WS{E}{\ovl{S_1'}}{\ovl{S_1}}% \hspace{3em}% \WS{E; \ModS{X}{S_1'}}{\ovl{S_2}}{\ovl{S_2'}}% }{% E[] ⊢ \Functor(X:S_1 ) S_2 <: \Functor(X:S_1') S_2'% }\]

Structure element subtyping rules:

ASSUM-ASSUM
\[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }}% }\]
DEF-ASSUM
\[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }}% }\]
ASSUM-DEF
\[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ c =_{βδιζη} t_2% }{% \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }}% }\]
DEF-DEF
\[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ t_1 =_{βδιζη} t_2% }{% \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }}% }\]
IND-IND
\[\frac{% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C'% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% }{% \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}}% }\]
INDP-IND
\[\frac{% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C'% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% }{% \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}}% }\]
INDP-INDP
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% \hspace{3em}% E[] ⊢ p =_{βδιζη} p'% \hspace{3em}% \end{array}% }{% \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}}% }\end{split}\]
MOD-MOD
\[\frac{% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }}% }\]
ALIAS-MOD
\[\frac{% E[] ⊢ p : S_1% \hspace{3em}% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }}% }\]
MOD-ALIAS
\[\frac{% E[] ⊢ p : S_2% \hspace{3em}% \WS{E}{S_1}{S_2}% \hspace{3em}% E[] ⊢ X =_{βδιζη} p% }{% \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}}% }\]
ALIAS-ALIAS
\[\frac{% E[] ⊢ p_1 =_{βδιζη} p_2% }{% \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }}% }\]
MODTYPE-MODTYPE
\[\frac{% \WS{E}{S_1}{S_2}% \hspace{3em}% \WS{E}{S_2}{S_1}% }{% \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }}% }\]

New environment formation rules

WF-MOD1
\[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% WF(E; \ModS{X}{S})[]% }\]
WF-MOD2
\[\frac{% \WS{E}{S_2}{S_1}% \hspace{3em}% \WF{E}{}% \hspace{3em}% \WFT{E}{S_1}% \hspace{3em}% \WFT{E}{S_2}% }{% \WF{E; \Mod{X}{S_1}{S_2}}{}% }\]
WF-ALIAS
\[\frac{% \WF{E}{}% \hspace{3em}% E[] ⊢ p : S% }{% \WF{E, \ModA{X}{p}}{}% }\]
WF-MODTYPE
\[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% \WF{E, \ModType{Y}{S}}{}% }\]
WF-IND
\[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\% \hspace{3em}% E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\% \hspace{3em}% E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I}% \hspace{3em}% \end{array}% }{% \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{}% }\end{split}\]

Component access rules

ACC-TYPE1
\[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End% }{% E[Γ] ⊢ p.c : T% }\]
ACC-TYPE2
\[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{T};… ~\End% }{% E[Γ] ⊢ p.c : T% }\]

Notice that the following rule extends the delta rule defined in section Conversion rules

ACC-DELTA
\[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{U};… ~\End% }{% E[Γ] ⊢ p.c \triangleright_δ t% }\]

In the rules below we assume \(Γ_P\) is \([p_1 :P_1 ;…;p_r :P_r ]\), \(Γ_I\) is \([I_1 :A_1 ;…;I_k :A_k ]\), and \(Γ_C\) is \([c_1 :C_1 ;…;c_n :C_n ]\).

ACC-IND1
\[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End% }{% E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j% }\]
ACC-IND2
\[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End% }{% E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k}% }\]
ACC-INDP1
\[\frac{% E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End% }{% E[] ⊢ p.I_i \triangleright_δ p'.I_i% }\]
ACC-INDP2
\[\frac{% E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End% }{% E[] ⊢ p.c_i \triangleright_δ p'.c_i% }\]