diff options
Diffstat (limited to 'documentation')
| -rw-r--r-- | documentation/bookmark/compilation/target/c++.md | 1 | ||||
| -rw-r--r-- | documentation/bookmark/incremental_computing.md | 9 | ||||
| -rw-r--r-- | documentation/bookmark/type_theory/dependent.md | 98 |
3 files changed, 59 insertions, 49 deletions
diff --git a/documentation/bookmark/compilation/target/c++.md b/documentation/bookmark/compilation/target/c++.md index 40625b60e..2e1c893ef 100644 --- a/documentation/bookmark/compilation/target/c++.md +++ b/documentation/bookmark/compilation/target/c++.md @@ -23,6 +23,7 @@ # Reference 0. []() +0. [Conan, the C/C++ Package Manager](https://conan.io/) 0. [C++ keywords: noexcept (since C++11)](https://en.cppreference.com/w/cpp/keyword/noexcept) 0. [alignas specifier (since C++11)](https://en.cppreference.com/w/cpp/language/alignas) 0. [Perfect Forwarding](https://www.modernescpp.com/index.php/perfect-forwarding) diff --git a/documentation/bookmark/incremental_computing.md b/documentation/bookmark/incremental_computing.md index 9daa63439..30bf02a79 100644 --- a/documentation/bookmark/incremental_computing.md +++ b/documentation/bookmark/incremental_computing.md @@ -1,5 +1,10 @@ # Reference -1. [Incremental computing](https://en.wikipedia.org/wiki/Incremental_computing) -1. [A theory of changes for higher-order languages](https://www.researchgate.net/publication/269126515_A_theory_of_changes_for_higher-order_languages) +0. []() +0. [Incremental](https://github.com/janestreet/incremental) +0. [Adapton](https://github.com/Adapton/adapton.rust) +0. [Anchors](https://github.com/lord/anchors) +0. [A Library for Incremental Computing](https://timilearning.com/posts/incremental-computing/) +0. [Incremental computing](https://en.wikipedia.org/wiki/Incremental_computing) +0. [A theory of changes for higher-order languages](https://www.researchgate.net/publication/269126515_A_theory_of_changes_for_higher-order_languages) diff --git a/documentation/bookmark/type_theory/dependent.md b/documentation/bookmark/type_theory/dependent.md index f731e988a..03a5606ec 100644 --- a/documentation/bookmark/type_theory/dependent.md +++ b/documentation/bookmark/type_theory/dependent.md @@ -1,56 +1,60 @@ # Exemplar -1. [Mononym: Type-Level Named Values in Rust - Part 1: Demo and Implementation](https://maybevoid.com/blog/mononym-part-1/) -1. [POMPOM LANGUAGE](https://github.com/caotic123/PomPom-Language) -1. [A simple type-theoretic language: Mini-TT](http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf) -1. https://cedille.github.io/ +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 -1. [A Language Agnostic Introduction to Dependent Types](https://www.shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html) -1. [The Gentle Art of Levitation](http://lambda-the-ultimate.org/node/5526) -1. [Programming up to Congruence](http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf) -1. [From Scheme to Dependent Types in 100 lines by Gershom Bazerman (Part 1)](https://vimeo.com/134561872) -1. [From Scheme to Dependent Types in 100 Lines by Gershom Bazerman (Part 2)](https://vimeo.com/135746080) -1. [Program = Proof](http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf) -1. [Multimodal Dependent Type Theory](https://arxiv.org/abs/2011.15021) -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) +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 -1. http://logipedia.inria.fr/about/about.php +0. []() +0. http://logipedia.inria.fr/about/about.php |