stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Work on Soundness

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-30 12:03:37 +02:00
parent c75f0c1ace
commit 550bc384e5
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
soundness.tex
View File

@ -86,7 +86,12 @@ We have to show T-Let and T-Call which leaves us with:
\begin{itemize} \begin{itemize}
\item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
\item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash $ \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied
\begin{itemize}
\item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
\item $\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot \ol{N}$ and lemma \ref{lemma:unifySoundness}
TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
\end{itemize}
\end{itemize} \end{itemize}
\item[$\texttt{v}.\texttt{m}(\ol{v})$] \item[$\texttt{v}.\texttt{m}(\ol{v})$]
Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise. Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.