# Exemplar

0. []()
0. [Mononym: Type-Level Named Values in Rust - Part 1: Demo and Implementation](https://maybevoid.com/blog/mononym-part-1/)
0. [POMPOM LANGUAGE](https://github.com/caotic123/PomPom-Language)
0. [A simple type-theoretic language:  Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf)
0. https://cedille.github.io/

# Reference

0. []()
0. [Checking Dependent Types with Normalization by Evaluation: A Tutorial](https://davidchristiansen.dk/tutorials/nbe/)
0. [A Language Agnostic Introduction to Dependent Types](https://www.shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html)
0. [The Gentle Art of Levitation](http://lambda-the-ultimate.org/node/5526)
0. [Programming up to Congruence](http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf)
0. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman (Part 1)](https://vimeo.com/134561872)
0. [From Scheme to Dependent Types in 100 Lines by Gershom Bazerman (Part 2)](https://vimeo.com/135746080)
0. [Program = Proof](http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf)
0. [Multimodal Dependent Type Theory](https://arxiv.org/abs/2011.15021)
0. [Thorsten Altenkirch - The power of Π - Lambda Days 2020](https://www.youtube.com/watch?v=3zT5eVHpQwA)
0. [A Path To DOT: Formalizing Fully Path-Dependent Types](https://arxiv.org/abs/1904.07298)
0. [Ghosts of Departed Proofs (Functional Pearl)](https://www.youtube.com/watch?v=2cAxOJEiL00)
0. [Ghosts of Departed Proofs (Functional Pearl)](https://kataskeue.com/gdp.pdf)
0. [F# Linear algebra with type-level dimensions and static checks](https://notebooks.azure.com/allisterb/projects/sylvester/html/Sylvester.Tensors.ipynb)
0. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman](https://vimeo.com/134561872 &&& https://vimeo.com/135746080)
0. [A Tutorial Implementation of a Dependently Typed Lambda Calculus](https://www.andres-loeh.de/LambdaPi/)
0. [The calculus of constructions](http://www.sciencedirect.com/science/article/pii/0890540188900053#)
0. https://www.idris-lang.org/
0. https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024/
0. http://blog.codersbase.com/posts/2013-12-03-learning-dependent-types.html
0. http://oxij.org/note/BrutalDepTypes/
0. https://hydraz.club/posts/2017-09-08.html
0. [Hoare Type Theory, Polymorphism and Separation](http://ynot.cs.harvard.edu/papers/jfpsep07.pdf)
0. ["Dependent Types in Haskell" by Stephanie Weirich](https://www.youtube.com/watch?v=wNa3MMbhwS4)
0. [A Little Bit of Dependent Types](https://youtu.be/WI8uA4KjQJk?t=5169)
0. [Type Checking Without Types](https://matthias.benkard.de/typecore/typecore.pdf)
0. [Cubical Type Theory: a constructive interpretation of the univalence axiom](http://www.cse.chalmers.se/~coquand/cubicaltt.pdf)
0. https://github.com/mortberg/cubicaltt
0. https://leanprover.github.io/introduction_to_lean/
0. [Infinity](https://github.com/groupoid/infinity)
0. https://github.com/groupoid
0. http://groupoid.space/
0. https://existentialtype.wordpress.com/2016/07/31/cubical-higher-type-theory-as-a-programming-language/
0. https://github.com/silt-lang/silt
0. [Parametric Quantifiers for Dependent Type Theory](https://people.cs.kuleuven.be/~andreas.nuyts/ParametricQuantifiers.pdf &&& https://www.youtube.com/watch?v=lJB5MhYJ4Js)
0. [A Specification for Dependently-Typed Haskell:](http://www.seas.upenn.edu/~sweirich/papers/systemd-submission.pdf)
0. [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)
0. [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)
0. https://bluishcoder.co.nz/2018/01/03/writing-basic-proofs-in-ats.html
0. [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)
0. https://medium.com/@maiavictor/about-induction-on-the-calculus-of-constructions-581fcfdb89c5
0. [05 A Dependent Haskell Triptych](https://www.youtube.com/watch?v=soKl1IslU-I)
0. https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf
0. [Algebraic Presentations of Dependent Type Theories](https://arxiv.org/abs/1602.08504v3)

# Math | Proofs

0. []()
0. http://logipedia.inria.fr/about/about.php