| Dependent Types at Work Lecture Notes for the LerNet Summer School (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-Löf type theory and Martin-Löf’s logical framework. We begin by showing how to do simply typed functional programming, and discuss the differences between Agda’s type system and the Hindley-Milner type system, which underlies mainstream typed functional programming languages like Haskell and ML. We then show how to employ dependent types for programming with functional data structures such as vectors and binary search trees. We go on to explain the Curry-Howard identification of propositions and types, and how it makes Agda not only a programming language but also a programming logic. According to Curry-Howard, we also identify programs and proofs, something which is possible only by requiring that all program terminate. However, we show in the final section a method for encoding general and possibly partial recursive functions as total | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||