diff options
author | Francesco Mazzoli <f@mazzo.li> | 2013-01-16 17:26:42 +0000 |
---|---|---|
committer | Francesco Mazzoli <f@mazzo.li> | 2013-01-16 17:26:42 +0000 |
commit | 8aee0ff8e7a2e5d27c5b48b54e27979a5d1651b0 (patch) | |
tree | 18a0985ec67d21738ab283a97dc1cc792e84e9aa /docs/background-notes.org | |
parent | e432bd5f35a1ac262f0f2734802aa2d4ecb853f6 (diff) |
renaming, more stuff
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 |