TIEA1000 Topical Themes in Mathematical Information Technology (1–10 cr)

We cover
* basic functional programming, involving
* * terms and types,
* * recursion and
* * reduction,
* proof by induction, using
* * the usual induction principle on natural numbers,
* * structural induction on types, such as lists, and
* * path induction (or based path induction) on equalities,
* lists and polymorphism, featuring higher-order functions like
* * map and
* * fold (also known as reduce),
* interactive metaprogramming with tactics, focusing on
* * partial application,
* * pattern matching and
* * rewriting,
* mathematical logic, as in
* * truth and falsehood,
* * negation, conjunction and disjunction,
* * universal and existential quantification and
* * axioms, such as functional extensionality, exluded middle,
double negation elimination, choice and univalence,
* inductive propositions, via case studies in
* * computational reflection and
* * matching regular expressions, and
* propositions as types, to tie it all together.

Only basic mathematical knowledge is needed.