notes

diff --git a/docs/background-notes.org b/docs/background-notes.org
new file mode 100644 (file)
index 0000000..8d65233
--- /dev/null
+++ b/docs/background-notes.org
@@ -0,0 +1,71 @@
+* TODO [15/24] Papers
+  - [X] “Observational Equality, Now!” OTT2.pdf
+  - [X] “The Gentle Art of Levitation” conor-levitation.pdf
+    Offers a nice metalanguage
+  - [ ] “Dependently Typed Functional Programs and their Proofs” conor-thesis.pdf
+    His PhD thesis, probably relevant
+  - [ ] “Elaborating Inductive Definition” elaborating-inductive.pdf
+    Don’t really knof what it’s about yet, probably interesting
+  - [X] “Giving Haskell a Promotion” haskell-promotion.pdf
+    Could cite it as related developement in the mainstream.
+  - [X] “Implementing General Purpose Dependently Typed Programming Languages” idris-implementation.pdf
+  - [ ] “Indexed Containers” indexed-containers.pdf
+    Don’t really know what this is about yet, but is probably relevant
+  - [X] “Local Type Inference” local-type-inference.pdf
+    Will cite when talking about bidirectional type checking
+  - [ ] “Unification Under a Mixed Prefix” miller-unification.pdf
+    I think it’s needed to write Epigram/Agda style dep. pattern matching
+  - [X] “OutsideIn(X)” outsidein.pdf
+    Cite this as an example of how damn hard inference is...
+  - [ ] “A tutorial implementation of dynamic pattern unification” pattern-unification.pdf
+  - [X] “ΠΣ: Dependent Types without the Sugar” PiSigma.pdf
+  - [X] “The Power of Pi” powerofpi.pdf
+  - [ ] “Simply Easy!” simply-easy.pdf
+  - [ ] “Dependently Typed Programming with Singletons” singleton-types.pdf
+    As haskell-promotion.pdf, could cite it as related developement in the
+    mainstream.
+  - [X] “System F with Type Equality Coercions” systemf-coercions.pdf
+    Same as haskell-promotion.pdf, but even better
+  - [X] “Towards a practical programming language based on dependent type theory” ulf-thesis.pdf
+    Agda
+  - [X] “The View from the Left” view-from-the-left.ps.gz
+  - [X] “Introduction to Generalised Type Systems” lambda-cube.pdf
+  - [ ] “Computation and Reasoning: A Type Theory for Computer Science”
+    I can’t find this one.
+  - [X] “Intuitionistic Type Theory” martin-lof-tt.pdf
+  - [ ] “Implicit Syntax” implicit-syntax.pdf
+  - [X] “The Calculus of Constructions” coc.pdf
+  - [X] “An Extended Calculus of Constructions” luo-thesis.ps
+
+* Outline
+** Simple and not-so-simple types
+*** The untyped lambda-calculus
+*** The STLC
+*** The Curry-Howard isomorphism
+** Intuitionistic Type Theory
+*** A Core Type Theory
+*** More than one equality
+*** Data
+    A core type theory with 0, 1, 2, W
+*** Inductive families
+**** Dependent pattern matching
+*** Corecursion
+*** Quotient types
+** Observational Type Theory
+*** Extensionality is hard to get
+    The “naive” extensionality and the problems with it
+*** A solution
+*** The problems with W
+    See blog post
+** Things to do
+*** Usable, Observational TT implementation
+    In the style of ΠΣ, Mini-TT
+    Possible features:
+    - Corecursion
+    - Quotient types
+    - Total or non-total?
+*** Inference for coercions
+    Specifically, what to do when we express inductive families indices as
+    equalities
+*** Eliminators based calculus
+    In the style of ETT