diff --git a/docs/logic.tex b/docs/logic.tex index 2283fc838793d6425847411b6ea3c72cb75a7356..6f9293703dd1d6efb754f4ebb565fa8bff5519ab 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -1,18 +1,3 @@ -% CONVENTION: -% Use \Ra/Lra for the logic and \implies/\iff for the metalogic. - -% This short (for now) note lays out a \emph{generic} separation logic which -% manages sharing through invariants and ownership through (partial commutative) -% monoids. The logic is generic in that the actual language it applies to is -% taken as a parameter, giving in particular the atomic (per-thread) reduction -% relation. Over this, we layer concurrency (by giving a semantics to \kw{fork} -% and lifting to thread pools). The generic logic provides numerous logical -% connectives and the semantics of Hoare triples and view shifts, together with a -% large portion of the proof theory---including, in particular, the structural -% rules for Hoare logic. Ultimately, these are proved sound relative to some -% simple assumptions about the language. It should be possible, moreover, to give -% a generic adequacy proof for Hoare triples as applied to the lifted thread-pool -% semantics. \section{Parameters to the logic} diff --git a/docs/setup.tex b/docs/setup.tex index 5ba0f0f2009666a8079fc745dde7f71f51c5715b..22e824e6b8ba340f3d675a026a19f6136df86f37 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -277,7 +277,7 @@ %% LOGIC SYMBOLS & NOTATION & IDENTIFIERS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\Sig}{\Sigma} +\newcommand{\Sig}{\mathcal{S}} \newcommand{\SigType}{\mathcal{T}} \newcommand{\SigFn}{\mathcal{F}} \newcommand{\sigfn}{F} @@ -292,7 +292,7 @@ \newcommand{\termB}{u} \newcommand{\termVal}{V} -\newcommand{\sort}{\sigma} +\newcommand{\sort}{\Sigma} \newcommand{\vctx}{\Gamma} \newcommand{\pfctx}{\Theta} @@ -463,3 +463,8 @@ \newcommand{\AuthInv}{\textsf{AuthInv}} \newcommand{\Auth}{\textsf{Auth}} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "iris" +%%% End: