Sun Aug 30 19:13:49 CEST 2009

Dependent Types

In [1] I read: ``Dependent type theory in full generality is very
powerful: it is able to express almost any conceivable property of
programs directly in the types of the program. This generality comes
at a steep price — checking that a given program is of a given type is
undecidable. For this reason, dependent type theories in practice do
not allow quantification over arbitrary programs, but rather restrict
to programs of a given decidable index domain, for example integers,
strings, or linear programs.''

In [2] I read: ``If the user can supply a constructive proof that a
type is inhabited (i.e., that a value of that type exists) then a
compiler can then check the proof and convert it into executable
computer code that computes the value by carrying out the
construction. The proof checking feature makes dependently typed
languages closely related to proof assistants. The code-generation
aspect provides a powerful approach to formal program verification and
proof-carrying code, since the code is derived directly from a
mechanically verified mathematical proof.''

[1] http://en.wikipedia.org/wiki/Natural_deduction
[2] http://en.wikipedia.org/wiki/Dependent_types