Skip to content

Commit b2c584b

Browse files
committed
citation for reduction semantics
1 parent a00f836 commit b2c584b

File tree

2 files changed

+15
-5
lines changed

2 files changed

+15
-5
lines changed

doc/nwpt14/NWPT14Contracts.bib

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,13 @@ @InProceedings{TFP11Hiperfit
2929
year = {2012}
3030
}
3131

32+
@Article{andersen06sttt,
33+
Title = {Compositional specification of commercial contracts},
34+
Author = {Andersen, Jesper and Elsborg, Ebbe and Henglein, Fritz and Simonsen, Jakob Grue and Stefansen, Christian},
35+
Journal = {International Journal on Software Tools for Technology Transfer},
36+
Year = {2006},
37+
Number = {6},
38+
Pages = {485--516},
39+
Volume = {8},
40+
Publisher = {Springer-Verlag}
41+
}

doc/nwpt14/NWPT14Contracts.tex

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -287,11 +287,11 @@ \subsection{Reduction Semantics}
287287

288288

289289
Apart from the denotational semantics our contract language is also
290-
equipped with a reduction semantics, which advances a contract by one
291-
time unit. We write $c \cRed \rho \tau c'$, to denote that $c$ is
292-
advanced to $c'$ in the environment $\rho$, where $\tau \in
293-
\type{Trans}$ indicates the transfers that are necessary (and
294-
sufficient) in order to advance $c$ to $c'$.
290+
equipped with a reduction semantics~\cite{andersen06sttt}, which
291+
advances a contract by one time unit. We write $c \cRed \rho \tau c'$,
292+
to denote that $c$ is advanced to $c'$ in the environment $\rho$,
293+
where $\tau \in \type{Trans}$ indicates the transfers that are
294+
necessary (and sufficient) in order to advance $c$ to $c'$.
295295

296296
The reduction semantics can be implemented as a recursive function of
297297
type

0 commit comments

Comments
 (0)