1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3b1.md b/content/zettel/3b1.md
new file mode 100644
index 0000000..133b638
--- /dev/null
+++ b/content/zettel/3b1.md
@@ -0,0 +1,25 @@
++++
+title = "Dependent Types"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b"]
+forwardlinks = ["3b2"]
+zettelid = "3b1"
++++
+
+A language with *dependent types* may include programs inside of the
+types. For arrays, this could, for example, be an array which has a
+program expression in the type which specifies the size of the array.
+
+The kernel proof language is what underlies the theorem proving. The "de
+Bruijn criterion" is satisfied by a theorem prover if the kernel
+language in which the proof is expressed in is expressed in a small
+kernel language. This is satisfied by most theorem provers including
+Coq. Only this small kernel language has to be trusted, as any searches
+for proofs will result in this kernel language and then be checked
+independently. That is why the search itself does not actually need to
+be trusted. Coq and Isabelle/HOL allow the programmer to define proof
+manipulations that cannot end up in the acceptance of invalid proofs.
+This can either be done in OCaml for Coq, but also in Ltac, which is a
+language in Coq designed for that purpose.