Towards homotopy Good blog http://siddhartha-gadgil.github.io/LogicTypesSpaces/blog/2015/01/22/dependent-function-types/ DTT - Martin Loef "Constructive Mathematics and Computer Programing" https://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf http://macqueenfest.cs.uchicago.edu/ Proof directed debugging https://www.cs.cmu.edu/~rwh/papers/regexp/jfp.pdf Minimal TT impl https://github.com/Andromedans/andromeda DTT Impl - Andrej Bauer http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ Lambda Pi tutorial https://www.andres-loeh.de/LambdaPi/ Cartesian Cubical https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf STLC http://flint.cs.yale.edu/cs430/lectureNotes/terse/Stlc.html Type systems / write you a haskell http://dev.stephendiehl.com/fun/004_type_systems.html Computation as Deduction (Pfenning) https://www.cs.cmu.edu/~fp/courses/comp-ded History of "type" in PL http://arcanesentiment.blogspot.com/2015/01/a-brief-history-of-type.html?m=1 Type system (due to Allen 87 "non-type-theoretic semantics for type-theoretic language." phd) # Type theory and its meaning explanations https://www.youtube.com/watch?v=xMAqniX2Paw # Cornell - Advanced Programing Languages CS6110 spring 2013 http://www.cs.cornell.edu/courses/cs6110/2013sp/ 8 - Evaluation contexts http://www.cs.cornell.edu/courses/cs6110/2013sp/lectures/lec08-sp13.pdf STLC http://www.cs.cornell.edu/courses/cs6110/2013sp/lectures/lec25-sp13.pdf # Program synthesis Relational program synthesis https://arxiv.org/abs/1809.02283 # Proof Refinement https://iohk.io/blog/proof-refinement-basics/ https://iohk.io/blog/bidirectional-proof-refinement/ https://iohk.io/blog/telescopic-proof-refinement/