docs/background-notes.org

   1 * TODO [15/24] Papers
   2   - [X] “Observational Equality, Now!” OTT2.pdf
   3   - [X] “The Gentle Art of Levitation” conor-levitation.pdf
   4     Offers a nice metalanguage
   5   - [ ] “Dependently Typed Functional Programs and their Proofs” conor-thesis.pdf
   6     His PhD thesis, probably relevant
   7   - [ ] “Elaborating Inductive Definition” elaborating-inductive.pdf
   8     Don’t really knof what it’s about yet, probably interesting
   9   - [X] “Giving Haskell a Promotion” haskell-promotion.pdf
  10     Could cite it as related developement in the mainstream.
  11   - [X] “Implementing General Purpose Dependently Typed Programming Languages” idris-implementation.pdf
  12   - [ ] “Indexed Containers” indexed-containers.pdf
  13     Don’t really know what this is about yet, but is probably relevant
  14   - [X] “Local Type Inference” local-type-inference.pdf
  15     Will cite when talking about bidirectional type checking
  16   - [ ] “Unification Under a Mixed Prefix” miller-unification.pdf
  17     I think it’s needed to write Epigram/Agda style dep. pattern matching
  18   - [X] “OutsideIn(X)” outsidein.pdf
  19     Cite this as an example of how damn hard inference is...
  20   - [ ] “A tutorial implementation of dynamic pattern unification” pattern-unification.pdf
  21   - [X] “ΠΣ: Dependent Types without the Sugar” PiSigma.pdf
  22   - [X] “The Power of Pi” powerofpi.pdf
  23   - [ ] “Simply Easy!” simply-easy.pdf
  24   - [ ] “Dependently Typed Programming with Singletons” singleton-types.pdf
  25     As haskell-promotion.pdf, could cite it as related developement in the
  26     mainstream.
  27   - [X] “System F with Type Equality Coercions” systemf-coercions.pdf
  28     Same as haskell-promotion.pdf, but even better
  29   - [X] “Towards a practical programming language based on dependent type theory” ulf-thesis.pdf
  30     Agda
  31   - [X] “The View from the Left” view-from-the-left.ps.gz
  32   - [X] “Introduction to Generalised Type Systems” lambda-cube.pdf
  33   - [ ] “Computation and Reasoning: A Type Theory for Computer Science”
  34     I can’t find this one.
  35   - [X] “Intuitionistic Type Theory” martin-lof-tt.pdf
  36   - [ ] “Implicit Syntax” implicit-syntax.pdf
  37   - [X] “The Calculus of Constructions” coc.pdf
  38   - [X] “An Extended Calculus of Constructions” luo-thesis.ps
  39
  40 * Outline
  41 ** Simple and not-so-simple types
  42 *** The untyped lambda-calculus
  43 *** The STLC
  44 *** The Curry-Howard isomorphism
  45 ** Intuitionistic Type Theory
  46 *** A Core Type Theory
  47 *** More than one equality
  48 *** Data
  49     A core type theory with 0, 1, 2, W
  50 *** Inductive families
  51 **** Dependent pattern matching
  52 *** Corecursion
  53 *** Quotient types
  54 ** Observational Type Theory
  55 *** Extensionality is hard to get
  56     The “naive” extensionality and the problems with it
  57 *** A solution
  58 *** The problems with W
  59     See blog post
  60 ** Things to do
  61 *** Usable, Observational TT implementation
  62     In the style of ΠΣ, Mini-TT
  63     Possible features:
  64     - Corecursion
  65     - Quotient types
  66     - Total or non-total?
  67 *** Inference for coercions
  68     Specifically, what to do when we express inductive families indices as
  69     equalities
  70 *** Eliminators based calculus
  71     In the style of ETT