aboutsummaryrefslogtreecommitdiff
path: root/documentation/bookmark/Type theory/Dependent types.md
diff options
context:
space:
mode:
authorEduardo Julian2020-12-02 04:42:03 -0400
committerEduardo Julian2020-12-02 04:42:03 -0400
commit982a19e0c5d57b53f9726b780fec4c18f0787b4f (patch)
tree50bf995dd5f1361c4a6651e2865819693ea25ca5 /documentation/bookmark/Type theory/Dependent types.md
parentcfa0a075b89a0df4618e7009f05c157393cbba72 (diff)
Test for Aedifex's "auto" command.
Diffstat (limited to '')
-rw-r--r--documentation/bookmark/Type theory/Dependent types.md1
1 files changed, 1 insertions, 0 deletions
diff --git a/documentation/bookmark/Type theory/Dependent types.md b/documentation/bookmark/Type theory/Dependent types.md
index 84d739492..8269310db 100644
--- a/documentation/bookmark/Type theory/Dependent types.md
+++ b/documentation/bookmark/Type theory/Dependent types.md
@@ -5,6 +5,7 @@
# Reference
+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)