Simple types, propositional proofs, and dynamics

The core STLC types and terms are $$A,B::=P\mid \mathbf{2}\mid A\to B,e::=x\mid \lambda x:A.e\mid ee\mid \mathsf{tt}\mid \mathsf{ff}\mid \mathsf{if}(e;e;e).$$ Type and context formation are generated by

$P\mathsf{type}$

$\mathbf{2}\mathsf{type}$

$A\mathsf{type}$$B\mathsf{type}$

$A\to B\mathsf{type}$

$\cdot \mathsf{ctx}$

$\mathrm{\Gamma }\mathsf{ctx}$$A\mathsf{type}$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma },x:A\mathsf{ctx}$

Rule instances below range over well-formed contexts and types; in Lam, the context-formation convention supplies $x\notin \mathrm{dom}(\mathrm{\Gamma })$.

$(x:A)\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:A$

$\mathrm{\Gamma }⊢\mathsf{tt}:\mathbf{2}$

$\mathrm{\Gamma }⊢\mathsf{ff}:\mathbf{2}$

$\mathrm{\Gamma }⊢e:\mathbf{2}$$\mathrm{\Gamma }⊢e_1:C$$\mathrm{\Gamma }⊢e_2:C$

$\mathrm{\Gamma }⊢\mathsf{if}(e;e_1;e_2):C$

$\mathrm{\Gamma },x:A⊢e:B$

$\mathrm{\Gamma }⊢\lambda x:A.e:A\to B$

$\mathrm{\Gamma }⊢e_1:A\to B$$\mathrm{\Gamma }⊢e_2:A$

$\mathrm{\Gamma }⊢e_1{e}_2:B$

Core values are $v::=\mathsf{tt}\mid \mathsf{ff}\mid \lambda x:A.e$. The core call-by-value dynamics are

$e_1⟼e_1^{\prime }$

$e_1{e}_2⟼e_1^{\prime }{e}_2$

$v_1\mathsf{value}$$e_2⟼e_2^{\prime }$

$v_1{e}_2⟼v_1{e}_2^{\prime }$

$v\mathsf{value}$

$(\lambda x:A.b)v⟼b[v/x]$

$e⟼e^{\prime }$

$\mathsf{if}(e;e_1;e_2)⟼\mathsf{if}(e^{\prime };e_1;e_2)$

$\mathsf{if}(\mathsf{tt};e_1;e_2)⟼e_1$

$\mathsf{if}(\mathsf{ff};e_1;e_2)⟼e_2$

The propositional extension adds Its formation and typing rules are

$A\mathsf{type}$$B\mathsf{type}$

$A\times B\mathsf{type}$

$A\mathsf{type}$$B\mathsf{type}$

$A+B\mathsf{type}$

$\mathbf{1}\mathsf{type}$

$\mathbf{0}\mathsf{type}$

$\mathrm{\Gamma }⊢e_1:A$$\mathrm{\Gamma }⊢e_2:B$

$\mathrm{\Gamma }⊢(e_1,e_2):A\times B$

$\mathrm{\Gamma }⊢e:A\times B$

$\mathrm{\Gamma }⊢\mathsf{fst}(e):A$

$\mathrm{\Gamma }⊢e:A\times B$

$\mathrm{\Gamma }⊢\mathsf{snd}(e):B$

$\mathrm{\Gamma }⊢\star :\mathbf{1}$

$\mathrm{\Gamma }⊢e:A$$B\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{inl}(e):A+B$

$A\mathsf{type}$$\mathrm{\Gamma }⊢e:B$

$\mathrm{\Gamma }⊢\mathsf{inr}(e):A+B$

$\mathrm{\Gamma }⊢e:A+B$$\mathrm{\Gamma },x:A⊢e_1:C$$\mathrm{\Gamma },y:B⊢e_2:C$

$\mathrm{\Gamma }⊢\mathsf{case}(e;x.e_1;y.e_2):C$

$\mathrm{\Gamma }⊢e:\mathbf{0}$$C\mathsf{type}$

$\mathrm{\Gamma }⊢{\mathsf{abort}}_C(e):C$

Extended values add $\star ,(v_1,v_2),\mathsf{inl}(v),\mathsf{inr}(v)$. Their call-by-value rules are

$e_1⟼e_1^{\prime }$

$(e_1,e_2)⟼(e_1^{\prime },e_2)$

$v_1\mathsf{value}$$e_2⟼e_2^{\prime }$

$(v_1,e_2)⟼(v_1,e_2^{\prime })$

$e⟼e^{\prime }$

$\mathsf{fst}(e)⟼\mathsf{fst}(e^{\prime })$

$v_1\mathsf{value}$$v_2\mathsf{value}$

$\mathsf{fst}((v_1,v_2))⟼v_1$

$e⟼e^{\prime }$

$\mathsf{snd}(e)⟼\mathsf{snd}(e^{\prime })$

$v_1\mathsf{value}$$v_2\mathsf{value}$

$\mathsf{snd}((v_1,v_2))⟼v_2$

$e⟼e^{\prime }$

$\mathsf{inl}(e)⟼\mathsf{inl}(e^{\prime })$

$e⟼e^{\prime }$

$\mathsf{inr}(e)⟼\mathsf{inr}(e^{\prime })$

$e⟼e^{\prime }$

$\mathsf{case}(e;x.e_1;y.e_2)⟼\mathsf{case}(e^{\prime };x.e_1;y.e_2)$

$v\mathsf{value}$

$\mathsf{case}(\mathsf{inl}(v);x.e_1;y.e_2)⟼e_1[v/x]$

$v\mathsf{value}$

$\mathsf{case}(\mathsf{inr}(v);x.e_1;y.e_2)⟼e_2[v/y]$

$e⟼e^{\prime }$

${\mathsf{abort}}_A(e)⟼{\mathsf{abort}}_A(e^{\prime })$

There is no root contraction for abort. Call-by-name on the untyped core uses $$F::=[-]\mid Fe\mid \mathsf{if}(F;e_1;e_2)$$ and the roots $$(\lambda x.b)a{⟼}_{\mathrm{n}}b[a/x],\mathsf{if}(\mathsf{tt};e_1;e_2){⟼}_{\mathrm{n}}{e}_1,\mathsf{if}(\mathsf{ff};e_1;e_2){⟼}_{\mathrm{n}}{e}_2.$$

The propositional natural-deduction rules are

$(h:A)\in \mathrm{\Delta }$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}\mathrm{\top }$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}\mathrm{\perp }$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}C$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A$$\mathrm{\Delta }{⊢}_{\mathsf{N}}B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\wedge B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\wedge B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\wedge B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}B$

$\mathrm{\Delta },h:A{⊢}_{\mathsf{N}}B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\Rightarrow B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\Rightarrow B$$\mathrm{\Delta }{⊢}_{\mathsf{N}}A$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\vee B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\vee B$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}A\vee B$$\mathrm{\Delta },h:A{⊢}_{\mathsf{N}}C$$\mathrm{\Delta },k:B{⊢}_{\mathsf{N}}C$

$\mathrm{\Delta }{⊢}_{\mathsf{N}}C$

Finally, the proof root relation is Its compatible closure is generated by The closure rule is $$\frac{r{⇝}_{\mathsf{p}}q}{K[r]{⟶}_{\mathsf{p}}K[q]}\mathrm{P}-\mathrm{Ctx}.$$