diff options
author | Eduardo Julian | 2020-10-31 20:26:37 -0400 |
---|---|---|
committer | Eduardo Julian | 2020-10-31 20:26:37 -0400 |
commit | 69272f598d831e89da83bdc8c9290d5607dfb14d (patch) | |
tree | 4915f241708344209d4c35ccdc8b8e57bab68e4c /documentation/research/Type theory/Dependent types.md | |
parent | eea741e9b4a47ae09832311d6d61f0bd6024f673 (diff) |
Re-named the directory for my bookmarks to better reflect what they are.
Diffstat (limited to 'documentation/research/Type theory/Dependent types.md')
-rw-r--r-- | documentation/research/Type theory/Dependent types.md | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/documentation/research/Type theory/Dependent types.md b/documentation/research/Type theory/Dependent types.md deleted file mode 100644 index 84d739492..000000000 --- a/documentation/research/Type theory/Dependent types.md +++ /dev/null @@ -1,43 +0,0 @@ -# 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. [Thorsten Altenkirch - The power of Π - Lambda Days 2020](https://www.youtube.com/watch?v=3zT5eVHpQwA) -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/) -1. [The calculus of constructions](http://www.sciencedirect.com/science/article/pii/0890540188900053#) -1. https://www.idris-lang.org/ -1. https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024/ -1. http://blog.codersbase.com/posts/2013-12-03-learning-dependent-types.html -1. http://oxij.org/note/BrutalDepTypes/ -1. https://hydraz.club/posts/2017-09-08.html -1. [Hoare Type Theory, Polymorphism and Separation](http://ynot.cs.harvard.edu/papers/jfpsep07.pdf) -1. ["Dependent Types in Haskell" by Stephanie Weirich](https://www.youtube.com/watch?v=wNa3MMbhwS4) -1. [A Little Bit of Dependent Types](https://youtu.be/WI8uA4KjQJk?t=5169) -1. [Type Checking Without Types](https://matthias.benkard.de/typecore/typecore.pdf) -1. [Cubical Type Theory: a constructive interpretation of the univalence axiom](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf) -1. https://github.com/mortberg/cubicaltt -1. https://leanprover.github.io/introduction_to_lean/ -1. [Infinity](https://github.com/groupoid/infinity) -1. https://github.com/groupoid -1. http://groupoid.space/ -1. https://existentialtype.wordpress.com/2016/07/31/cubical-higher-type-theory-as-a-programming-language/ -1. https://github.com/silt-lang/silt -1. [Parametric Quantifiers for Dependent Type Theory](https://people.cs.kuleuven.be/~andreas.nuyts/ParametricQuantifiers.pdf &&& https://www.youtube.com/watch?v=lJB5MhYJ4Js) -1. [A Specification for Dependently-Typed Haskell:](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf) -1. [A Specification for Dependent Types in Haskell](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf &&& https://cs.brynmawr.edu/~rae/papers/2017/dep-haskell-spec/dep-haskell-spec.pdf &&& https://www.youtube.com/watch?v=0157rUxC4_8) -1. [Normalization by Evaluation for Sized Dependent Types](http://publications.lib.chalmers.se/records/fulltext/252072/local_252072.pdf &&& https://www.youtube.com/watch?v=uSP91COE_ZA) -1. https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html -1. [AN INTRODUCTION TO UNIVALENT FOUNDATIONS FOR MATHEMATICIANS](http://www.ams.org/journals/bull/2018-55-04/S0273-0979-2018-01616-9/S0273-0979-2018-01616-9.pdf) -1. https://medium.com/@maiavictor/about-induction-on-the-calculus-of-constructions-581fcfdb89c5 -1. [05 A Dependent Haskell Triptych](https://www.youtube.com/watch?v=soKl1IslU-I) -1. https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf -1. [Algebraic Presentations of Dependent Type Theories](https://arxiv.org/abs/1602.08504v3) - |