next up previous contents index
Next: From informal proofs to Up: Theorem-proving in Agda Previous: Theorem-proving in Agda   Contents   Index

Introduction to dependent type theory

The is an implementation of dependent type theory due to Per Martin-Löf. Type theory is used as a logical framework: Different theories can be represented in type theory. In this section, we represent several logical systems via interpretation due to Heyting. This is called a shallow embedding. We shall formalize proofs in dependent type theory, and then express them in .

Subsections

Agda distribution team