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
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
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
41 ** Simple and not-so-simple types
42 *** The untyped lambda-calculus
44 *** The Curry-Howard isomorphism
45 ** Intuitionistic Type Theory
46 *** A Core Type Theory
47 *** More than one equality
49 A core type theory with 0, 1, 2, W
50 *** Inductive families
51 **** Dependent pattern matching
54 ** Observational Type Theory
55 *** Extensionality is hard to get
56 The “naive” extensionality and the problems with it
58 *** The problems with W
61 *** Usable, Observational TT implementation
62 In the style of ΠΣ, Mini-TT
67 *** Inference for coercions
68 Specifically, what to do when we express inductive families indices as
70 *** Eliminators based calculus