blob: 133b638c1ee138cf30a6c353fbf4427f19b60572 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
