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

SameW rule soundness

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-04-03 00:45:51 +02:00
parent 87f413241a
commit a151415950
2 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
soundness.tex
View File

@ -388,6 +388,8 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$
\item[Settle] Assumption, S-Trans \item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans \item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$ \item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Same] by S-Exists
\item[SameW] %TODO
\item[Adapt] Assumption, S-Extends, S-Trans \item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset C'$ \item[Adopt] Assumption, because $C \subset C'$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases: %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:

2
tRules.tex
View File

@ -132,7 +132,7 @@ $
% \caption{Input Syntax}\label{fig:syntax} % \caption{Input Syntax}\label{fig:syntax}
% \end{figure} % \end{figure}
\subsection{ANF transformation} \subsection{ANF transformation}\ref{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)} \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
%https://en.wikipedia.org/wiki/A-normal_form) %https://en.wikipedia.org/wiki/A-normal_form)
Featherweight Java's syntax involves no \texttt{let} statement Featherweight Java's syntax involves no \texttt{let} statement