Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
b6e2991e
Commit
b6e2991e
authored
Jan 31, 2016
by
Ralf Jung
Browse files
change some metachars araound a little
parent
764f5144
Changes
2
Hide whitespace changes
Inline
Side-by-side
docs/logic.tex
View file @
b6e2991e
% 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
}
...
...
docs/setup.tex
View file @
b6e2991e
...
...
@@ -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
}{
\
s
igma
}
\newcommand
{
\sort
}{
\
S
igma
}
\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:
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment