diff options
| author | Eduardo Julian | 2019-09-07 01:50:37 -0400 |
|---|---|---|
| committer | Eduardo Julian | 2019-09-07 01:50:37 -0400 |
| commit | b63ac226cc2ea843f08f7c72b18d22602462c624 (patch) | |
| tree | 7fb72562c39549108b7a48c1a6819c9bd3a64dab /documentation/research/Type theory/Dependent types.md | |
| parent | 181f93f3e963c9738ed60f6f5e2d2a37253a0b1b (diff) | |
Modified compiler's machinery to use the new abstractions for descriptors and signatures.
Diffstat (limited to '')
| -rw-r--r-- | documentation/research/Type theory/Dependent types.md | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/documentation/research/Type theory/Dependent types.md b/documentation/research/Type theory/Dependent types.md index f8849fcd1..8ea68473b 100644 --- a/documentation/research/Type theory/Dependent types.md +++ b/documentation/research/Type theory/Dependent types.md @@ -1,9 +1,13 @@ # Exemplar +1. [A simple type-theoretic language: Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf) 1. https://cedille.github.io/ # Reference +1. [A Path To DOT: Formalizing Fully Path-Dependent Types](https://arxiv.org/abs/1904.07298) +1. [Ghosts of Departed Proofs (Functional Pearl)](https://www.youtube.com/watch?v=2cAxOJEiL00) +1. [Ghosts of Departed Proofs (Functional Pearl)](https://kataskeue.com/gdp.pdf) 1. [F# Linear algebra with type-level dimensions and static checks](https://notebooks.azure.com/allisterb/projects/sylvester/html/Sylvester.Tensors.ipynb) 1. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman](https://vimeo.com/134561872 &&& https://vimeo.com/135746080) 1. [A Tutorial Implementation of a Dependently Typed Lambda Calculus](https://www.andres-loeh.de/LambdaPi/) |