sfGrammarSemantics.txt

syntax 

bnf 

\begin{matrix} \mathbf{\tau}& ::= & \lambda \mathbf{\upsilon}{\tt :}\sigma . \mathbf{\tau}\\ & | & \tau\, \tau\\ & | & \upsilon \\ & | & \Lambda \theta::\kappa.\tau\\ &|& [\sigma] &&\\&|& {\tt z} \\&|&{\tt s}\, \tau\\&&\\ \upsilon & ::= & \tt{a} | \tt{b} | \tt{c} | ... | \tt{aa} | ... \end{matrix}

\begin{matrix} \sigma & ::= & \lambda \mathbf{\theta }\tt{::}\kappa.\sigma\\&|& \sigma\,{\tt space}\,\sigma\\ &|& \theta\\ & | & \sigma \rightarrow \sigma \\ &|& Nat\\ &|& \Pi \theta::\kappa . \sigma\\ \\ \theta & ::= & \tt{A} | \tt{B} | \tt{C} | ... | \tt{AA} | ... \\ \end{matrix}

parser grammar

\begin{matrix} &&\\ \mathbf{\tau}& ::= & \lambda \mathbf{\upsilon}\tt{:}\sigma . \mathbf{\tau}\\ & | & \alpha\\ &&\\ 
\alpha & ::= & \Lambda\theta::\kappa.\tau\\ &|& \beta \\\\
\beta &::= &\mathbf{\beta\, \tt{space}\, \phi} \\ &|& \phi\\\\
\phi & ::= & \tt{(}\tau \tt{)}\\ &|& \upsilon \\ &|& {\tt z}\\ &|& {\tt s} \\ &|& [\sigma]\\
\end{matrix}

\begin{matrix} &&\\ \mathbf{\sigma}& ::= & \lambda \mathbf{\theta}\tt{::}\kappa . \mathbf{\sigma}\\ & | & \eta\\ &&\\ 
\eta & ::= &  \Pi\theta::\kappa.\eta\\
&|&\delta \\ &&\\ 
\delta & ::= & \delta \rightarrow \epsilon\\ 
&|& \epsilon\\\\ 
\epsilon & ::= & \mathbf{\epsilon\, \tt{space}\,\rho } \\
&|& \rho\\\\
\rho &::=&\tt{(}\sigma \tt{)}\\ &|& \theta \\&|& Nat\\ \end{matrix}

\upsilon & ::= & \tt{a} | \tt{b} | \tt{c} | ... | \tt{aa} | ... \\

\begin{matrix} \theta & ::= & \tt{A} | \tt{B} | \tt{C} | ... | \tt{AA} | ... \\\end{matrix}

semantics

see STLC

\frac{\Gamma \vdash A :: * \quad \Gamma, x:A\vdash M:B}{\Gamma \vdash \lambda x:A.M:B}

\frac{\Gamma\,, X\,::K \vdash t : T}{\Gamma \vdash (\Lambda X::K.t):\Pi X::K.T}

\frac{\Gamma \vdash f : \Pi X::K.T\quad\Gamma\vdash A::K}{\Gamma \vdash (f\, [A]):T[X := A]}

(\Lambda X::K.t)\,A \rightsquigarrow t[X:=A]

\frac{\Gamma\,, X\,::K \vdash T :: *}{\Gamma \vdash \Pi X::K.T::*}