Skip to content

Commit 2eab983

Browse files
jihgfeejihgfee
committed
Initial commit
0 parents  commit 2eab983

36 files changed

+12672
-0
lines changed

Diff for: ‎.gitignore

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
## LaTeX
2+
*.aux
3+
*.bbl
4+
*.blg
5+
*.brf
6+
*.fdb_latexmk
7+
*.fls
8+
*.log
9+
*.out
10+
*.pdf
11+
*.toc
12+
13+
## Emacs
14+
*~

Diff for: ‎CONTRIBUTING.md

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
Contributing to the Iris Lecture Notes is done via pull requests.
2+
To create a pull request, we advice creating a local fork of the repository,
3+
in which branches can be made with the suggested changes.
4+
We advice creating small branches, that isolate individual changes
5+
(e.g. typos of a single section)
6+
Pull requests can then be made through the github user interface, after which
7+
point the changeset will be reviewed by the Iris Lecture Notes team.

Diff for: ‎LICENSE

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Everything in this repository is licensed under the terms of the CC-BY 4.0 license.

Diff for: ‎Makefile

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
2+
all:
3+
latexmk -pdf main
4+
5+
clean:
6+
rm *~ *.aux *.bbl *.blg *.log *.out *.brf *.fls *.toc

Diff for: ‎README.md

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
# Iris Lecture Notes
2+
3+
This is the official source code for the Iris Lecture Notes (ILN), that has been
4+
used for multiple iterations of the Program Logics course at
5+
Aarhus University, Denmark.
6+
7+
The ILN are under continuous development, for which we welcome suggested
8+
changes (for more on how to contribute see [CONTRIBUTING.md](CONTRIBUTING.md)).
9+
10+
The ILN can be compiled using `make`.

Diff for: ‎heaplang.sty

+89
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
2+
\ProvidesPackage{heaplang}
3+
4+
\RequirePackage{amssymb}
5+
6+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7+
% CONCRETE LANGUAGE SYNTAX AND SEMANTICS
8+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9+
\newcommand{\textlang}[1]{\textsf{#1}}
10+
\newcommand{\langkw}[1]{\textlang{\color{blue} #1}}
11+
\newcommand{\lvar}[1]{\textit{#1}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions.
12+
\newcommand{\lvarA}{\lvar{\var}}
13+
\newcommand{\lvarB}{\lvar{\varB}}
14+
\newcommand{\lvarC}{\lvar{\varC}}
15+
16+
\newcommand{\loc}{\ell}
17+
18+
\newcommand{\mdef}{\eqdef}
19+
\newcommand{\ldef}{:=}
20+
21+
\def\LetNoIn#1=#2{\langkw{let} \spac #1 \mathrel{\ldef} #2 \spac}
22+
\def\In{\langkw{in}\spac}
23+
\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{\ldef} #2 \spac \langkw{in} \spac}
24+
\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
25+
\def\Else{\spac\langkw{else} \spac}
26+
\def\Ref(#1){\langkw{ref}\spac (#1)}
27+
\def\Rec#1 #2={\langkw{rec}\spac #1\ {#2} \mathrel{\ldef}}
28+
\def\Skip{\langkw{skip}}
29+
\def\SkipN{\langkw{skipN}}
30+
\def\Assert{\langkw{assert}}
31+
\newcommand\Inj[1]{\langkw{inj}_{#1}\spac}
32+
\def\Inl{\langkw{inl}}
33+
\def\Inr{\langkw{inr}}
34+
\def\Fst{\langkw{fst}}
35+
\def\Snd{\langkw{snd}}
36+
\newcommand\Proj[1]{\pi_{#1}\spac}
37+
\def\True{\langkw{true}}
38+
\def\False{\langkw{false}}
39+
\def\Match#1with#2=>#3|#4=>#5end{\langkw{match} \spac #1 \spac \langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
40+
\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
41+
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
42+
&#2&\Ra#3\\|&#4&\Ra#5\\%
43+
\multicolumn{3}{l}{\langkw{end}#6}%
44+
\end{array}}}
45+
\def\MatchMLT#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}{rll}%
46+
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
47+
&#2&\Ra#3\\|&#4&\Ra#5\\%
48+
\multicolumn{3}{l}{\langkw{end}#6}%
49+
\end{array}}}
50+
\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
51+
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
52+
&#2&\Ra#3\\|&#4&\Ra#5\\|&#6&\Ra#7\\%
53+
\multicolumn{3}{l}{\langkw{end}#8}%
54+
\end{array}}}
55+
\def\MatchS#1with#2=>#3end{
56+
\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
57+
\newcommand\CAS{\langkw{CAS}}
58+
\newcommand\CmpX{\langkw{CmpX}}
59+
\newcommand*\Fork[1]{\langkw{fork}\spac\set{#1}}
60+
\newcommand\deref{\mathop{!}}
61+
\let\gets\leftarrow
62+
63+
\newcommand{\fold}{\langkw{fold}\spac}
64+
\newcommand{\unfold}{\langkw{unfold}\spac}
65+
66+
\newcommand{\Op}[1]{\mathrel{#1}}
67+
68+
\newcommand{\binop}{\circledcirc}
69+
\newcommand{\Plus}{\Op{+}}
70+
\newcommand{\Minus}{\Op{-}}
71+
\newcommand{\Mult}{\Op{*}}
72+
\newcommand{\Eq}{\Op{=}}
73+
\newcommand{\Lt}{\Op{<}}
74+
75+
\newcommand{\TT}{()}
76+
\newcommand{\FAA}{\langkw{FAA}\spac}
77+
\newcommand{\free}{\langkw{free}\spac}
78+
79+
\newcommand{\heaplang}{HeapLang\xspace}
80+
\newcommand{\assert}[1]{\langkw{assert}\ #1}
81+
82+
\newcommand{\tryacquire}{\mathsf{try\_acquire}}
83+
84+
\newcommand{\go}{\mathit{go}}
85+
86+
\newcommand{\none}{\Inj 1 {\TT}}
87+
\newcommand{\some}[1]{\Inj 2 {#1}}
88+
89+
\newcommand{\parop}{\vert\vert}

0 commit comments

Comments
 (0)