From 3ebd38caad922a64f0b362729e7fab4c92f13e75 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 3 Jun 2024 15:00:06 -0400
Subject: [PATCH] init

---
 .gitignore         |   2 +
 ahmed/notes.typ    | 165 +++++++++++++++++++++++++++++++++++++++++++++
 common.typ         |   3 +
 pfenning/notes.typ | 135 +++++++++++++++++++++++++++++++++++++
 pfenning/test.adj0 |   7 ++
 5 files changed, 312 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 ahmed/notes.typ
 create mode 100644 common.typ
 create mode 100644 pfenning/notes.typ
 create mode 100644 pfenning/test.adj0

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..d142e25
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.pdf
+.DS_Store
\ No newline at end of file
diff --git a/ahmed/notes.typ b/ahmed/notes.typ
new file mode 100644
index 0000000..3ddb34f
--- /dev/null
+++ b/ahmed/notes.typ
@@ -0,0 +1,165 @@
+#import "@preview/prooftrees:0.1.0": *
+#set page(width: 5in, height: 8in, margin: 0.4in)
+
+#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
+#let subst(x, v, e) = $#e [#v\/#x]$
+#let isValue(x) = $#x "value"$
+#let mapstostar = $op(arrow.r.long.bar)^*$
+#let safe = $"safe"$
+#let db(x) = $bracket.l.double #x bracket.r.double$
+
+= Mon. Jun 3 \@ 14:00
+
+== Logical relations
+
+Logical relations are used to prove things about programs
+
+- Unary equivalence
+  - Example: Prove termination of the STLC
+  - Example: Prove type soundness / safety (these lectures)
+
+- Binary equivalence
+  - Example: are two programs going to behave the same when you put them in some different context? (*contextual equivalence*)
+
+-
+  Representation independence
+
+  - Example: suppose u implement a stack and have 2 different implementations. Prove that it doesn't matter which implementation you use.
+  - Parametricity for existential types "there exists a stack such that these properties are true"
+
+- Parametricity
+- Security levels of data in a security programming language
+  - Establish that high-security data never flows to low-security observers (*non-interference*)
+
+You can also relate source terms to target terms in different languages.
+This can be used to prove compiler correctness.
+
+== Type safety / soundness
+
+Unary realizability relations for FFI. "all well-behaved terms from language A can be used in language B without causing problems with either language"
+
+== STLC
+
+Statics
+
+- $tau ::= "bool" | tau_1 arrow.r tau_2$
+- $e ::= x | "true" | "false" | ifthenelse(e, e_1, e_2) | lambda (x : tau) . e | e_1 " " e_2$
+- $v ::= "true" | "false" | lambda (x:tau) . e$
+- $E ::= [dot] | "if" E "then" e_1 "else" e_2 | E " " e_2 | v " " E$
+
+Operational semantics
+
+#let mapsto = $arrow.r.long.bar$
+
+#rect[$e mapsto e'$]
+
+#tree(
+  axi[],
+  uni[$ifthenelse("true", e_1, e_2) mapsto e_1$]
+)
+
+#tree(
+  axi[],
+  uni[$ifthenelse("false", e_1, e_2) mapsto e_2$]
+)
+
+#tree(
+  axi[],
+  uni[$(lambda (x:tau) e) v mapsto subst(x, v, e)$]
+)
+
+#tree(
+  axi[$e mapsto e'$],
+  uni[$E[e] mapsto E[e']$]
+)
+
+Contexts:
+
+$Gamma ::= dot | Gamma , x : A$
+
+#rect[$Gamma tack.r e : tau$]
+
+#tree(
+  axi[],
+  uni[$Gamma tack.r "true" : "bool"$]
+)
+
+#tree(
+  axi[],
+  uni[$Gamma tack.r "false" : "bool"$]
+)
+
+#tree(
+  axi[$Gamma tack.r e : "bool"$],
+  axi[$Gamma tack.r e_1 : tau$],
+  axi[$Gamma tack.r e_2 : tau$],
+  tri[$Gamma tack.r ifthenelse(e, e_1, e_2) : tau$]
+)
+
+#tree(
+  axi[$Gamma(x) = tau$],
+  uni[$Gamma tack.r x : tau$]
+)
+
+#tree(
+  axi[$Gamma , x : tau tack.r e : tau_2$],
+  uni[$Gamma tack.r lambda (x : tau_1) . e : tau_1 arrow.r tau_2  $]
+)
+
+#tree(
+  axi[$Gamma tack.r e_1 : tau_2 arrow.r tau$],
+  axi[$Gamma tack.r e_2 : tau_2$],
+  bin[$Gamma tack.r e_1 e_2 : tau$],
+)
+
+#quote(block: true, attribution: [Milner])[
+  Well-typed programs do not go wrong
+]
+
+What does "going wrong" mean? It means getting stuck. You can't take another step and it's not a value.
+
+*Definition (Type Soundness).* If $dot tack.r e : tau$, then
+$forall(e' . e mapstostar e')$ either $isValue(e')$ or $exists e'' . e' mapsto e''$
+
+*Definition (Progress).* If $dot tack.r e : tau$ then either $isValue(e)$ or $exists e' . (e mapsto e')$.
+
+*Definition (Preservation).* If $dot tack.r e : tau$ and $e mapsto e'$ then $dot tack.r e' : tau$.
+
+Progress and preservation are a _technique_ for proving type soundness, by just using the two functions over and over.
+
+== Logical relations
+
+$ P_tau(e) $
+
+A unary relation on any expression $e$ and its corresponding type $tau$.
+(There are also binary relations $R_tau (e_1, e_2)$)
+
+The property we're interested in is: $safe(e)$
+
+- If $dot tack.r e:tau$ then $safe(e)$
+
+*Definition (safe).* $safe(e) :equiv forall e' . (e mapstostar e') arrow.r.double isValue(e') or exists e'' . (e' mapsto e'')$
+
+Common technique:
+
+- Focus on the values, when do values belong to the relation, when are they safe? 
+- Then check expressions. When do expressions belong to the relation, and when are they safe?
+
+$ V db(tau_1) = { v | ... } \
+V db("bool") = { "true" , "false" } \
+V db(tau_1 arrow.r tau_2) = { lambda (x : tau_1) . e | ...  }
+$ 
+
+Can't have just arbitrary $lambda (x : tau_1) . e$ under $V db(tau_1 arrow.r tau_2)$.
+The body also needs to be well-typed.
+
+$
+V db(tau_1 arrow.r tau_2) = { lambda (x : tau_1) . e | forall v in V db(tau_1) . subst(x, v, e) in Epsilon db(tau_2) } \
+Epsilon db(tau) = { e | forall e' . e mapstostar e' and "irreducible"(e') arrow.r.double e' in V db(tau)}
+$
+
+#rect[
+*Example of code from Rust.*
+Unsafe code blocks are an example of a something that may not be _syntactically well-formed_, but are still represented by logical relations because they behave the same at the boundary.
+]
+
diff --git a/common.typ b/common.typ
new file mode 100644
index 0000000..22d1139
--- /dev/null
+++ b/common.typ
@@ -0,0 +1,3 @@
+#import "@preview/prooftrees:0.1.0": *
+
+#set page(width: 5in, height: 8in, margin: 0.4in)
diff --git a/pfenning/notes.typ b/pfenning/notes.typ
new file mode 100644
index 0000000..eda39c4
--- /dev/null
+++ b/pfenning/notes.typ
@@ -0,0 +1,135 @@
+#import "../common.typ": *
+
+= Adjoint Functional Programming
+
+== Lecture 1. Linear functional programming
+
+- Origins of linearity is from linear logic
+- from 1987 or before
+
+#let isValue(x) = $#x "value"$
+
+Language to be studied is called "snax"
+	- Features
+		- Substructural programming
+		- Inference
+			- Overloading? writing the same function that works both linearly and non-linearly
+		- "Proof-theoretic compiler"
+			- Everything up til the target C is either natural deduction, sequent calculus, etc.
+	- Types
+		- "if there's something you don't need in the language, don't put it in the language"
+		- no empty type
+		- unit type
+			- 1
+				- #tree(axi[], uni[$() : 1$])
+				- #tree(axi[], uni[$isValue(())$])
+			- +
+				- ${e : A}{"inl" e : A + B}$
+				- ${e : B}{"inr" e : A + B}$
+				- #tree(axi[$isValue("v")$], uni[$isValue("inl" v)$])
+				- #tree(axi[$isValue("v")$], uni[$isValue("inr" v)$])
+			- $A + B :equiv +\{"inl":A, "inr": B\}$
+			- label set $L eq.not emptyset$ , finite
+				- finiteness is important
+			- nat = $+\{ "zero" : 1 , "succ" : "nat" \}$
+				- recursion is required to define an infinite amount of things
+					- "equirecursive" types
+						- nat is "equal" to the recursive definition in some sense
+			- k
+				- $\{(k \in l) e : A_e}{k(e) : +\{l : A_l\}_{l : L}}$
+			- $ceil(0) = "zero" ()$
+
+  - Computational rules
+
+    Define negation of booleans
+
+    $"not" (x : "bool") : "bool" \
+    "not" x = "match" x "with" \
+    | "true" u arrow.r "false" u\
+    | "false" u arrow.r "true" u \
+    $
+
+    Function definitiosn like these operate at the meta level.
+    Avoid introducing function types today.
+
+    Linear functional programming means *every variable must be used exactly once.*
+
+    *NOTE:* Above cannot be defined $"true" u arrow.r "false" ()$, since $u$ is not used.
+
+    DOn't need a garbage collector for linear functional programming language
+
+    #tree(
+      axi[$e : +{l : A_l}_(l in L)$],
+      axi[$x : A_l$],
+      axi[$tack.r e_l : C(l in L)$],
+      nary(3)[$"match" e "with" (l(x) arrow.r.double e_l)_(l in L) : C$],
+    )
+
+    Cannot write a function $"duplicate"(x) = (x , x)$ because of linear programming
+
+    #tree(
+      axi[$Delta tack.r e_1: A$],
+      axi[$Gamma tack.r e_2 : B$],
+      bin[$Delta,Gamma tack.r (e_1, e_2) : A times B$],
+    )
+
+    so introducing contexts
+
+    $Gamma :equiv (dot) | Gamma , x : A$
+
+    where the variable $x$ must be unique.
+
+    #tree(axi[], uni[$x : A tack.r x : A$])
+
+    *NOTE:* Left side is $x : A$, not $Gamma , x : A$ because those others would be unused, violating the single use rule.
+
+    #tree(
+      axi[$Delta , e : A times B$],
+      axi[$Gamma , x : A, y : B tack.r e' : C$],
+      nary(2)[$Delta , Gamma tack.r "match" e "with" (x , y) => e' : C$],
+    )
+
+    Have to split your variables to check $e$ and $e'$. This is not the way to implement it.
+
+    To implement it, check $"FV"(e)$ and $"FV"(e')$. These correspond to $Delta$ and $Gamma$ respectively. This is expensive.
+
+    - An easier way is to have each judgement give back another context containing the variables not use. Called a "subtractive" approach.
+
+    - Additive approach returns the variables used, and then check to make sure variables don't exist on the output.
+
+    GOing backk
+
+    #tree(
+      axi[],
+      uni[$dot tack.r () : 1$],
+    )
+
+    // #tree(
+    //   axi[$Delta tack.r e : +{l : A_l}_(l in L)$],
+    //   axi[$Gamma $]
+    // )
+
+  Defining plus:
+
+  - 
+    $"plus" (x : "nat") (y : "nat") : "nat" \
+    "plus" x " " y = "match" x "with" \
+    | "zero" () arrow.r.double #text(fill: red)[$"zero" ()$] \
+    | "succ" x' arrow.r.double "succ" ("plus" x' y)
+    $
+
+    This is problematic because it doesn't use up $y$ in the first branch.
+
+  - 
+    $"plus" (x : "nat") (y : "nat") : "nat" \
+    "plus" x " " y = "match" x "with" \
+    | "zero" () arrow.r.double y \
+    | "succ" x' arrow.r.double "succ" ("plus" x' y)
+    $
+
+    This uses up all inputs exactly.
+
+  #tree(
+    axi[$Gamma tack.r e : A_k (k in L)$],
+    uni[$Gamma tack.r k(e) : +{l : A_l}_(l in L)$],
+  )
diff --git a/pfenning/test.adj0 b/pfenning/test.adj0
new file mode 100644
index 0000000..83c2600
--- /dev/null
+++ b/pfenning/test.adj0
@@ -0,0 +1,7 @@
+type bool = +{'true : 1, 'false : 1}
+
+decl not (x : bool) : bool
+defn not x = match x with
+  | 'true () => 'false ()
+  | 'false () => 'true ()
+