diff options
Diffstat (limited to 'docs/background-notes.org')
| -rw-r--r-- | docs/background-notes.org | 71 |
1 files changed, 0 insertions, 71 deletions
diff --git a/docs/background-notes.org b/docs/background-notes.org deleted file mode 100644 index 8d65233..0000000 --- a/docs/background-notes.org +++ /dev/null @@ -1,71 +0,0 @@ -* 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 |