blob: 8d65233a796e146d94195da34f70510019a9adaf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
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
|
