Skip to content

Fix typo in textbook #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
pitmonticone wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix typo in textbook #61

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion frap_book.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4769,7 +4769,7 @@ \subsection{Soundness Proof}

Actually, we need to modify our translation judgment so that it also applies to ``silly'' intermediate states of execution in the target language.
For instance, we wind up with $\skipe$s that are quickly stepped away, yet those configurations must be related to source configurations by $\sim$.
Here is one example of the extra rules that we need to add to make our induction hypothsis strong enough.
Here is one example of the extra rules that we need to add to make our induction hypothesis strong enough.
$$\infer{\dscomp{v}{x \leftarrow \mt{Return} \; n; c(x)}{\mt{skip}; s}}{
v(y) = n
& \dscomp{v}{c(n)}{s}
Expand Down