diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/background-notes.org | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/docs/background-notes.org b/docs/background-notes.org new file mode 100644 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 |