Let me know if you would want to hear more about sth in particular or if I should add sth to the lists below:
-
induction: best known is induction on natural numbers. We have also seen induction on terms. What is the general principle? Can we explain induction in a way that it can account for all the different examples (and more):
- numbers
- terms
- is our definition of the transitive closure of a relation a definition by induction?
- ...
-
pattern matching: our basic mechanism of computation is the following: given a term and a set of rules, choose a rule, apply the rule to the term, get a new term, keep on going (until no rule can be applied, in which case the term you got is the result). But applying the rule requires some kind of pattern matching. So what kind of pattern matching is allowed here? Can we increase computational power by making pattern matching more powerful?
-
computation is proof and proof is computation
-
equivalence relation: many important structures can be defined as sets of equivalence classes:
- in economics: price
- in maths: angles, sets, numbers (integer, rational, real), vectors, ...
- ...
And some of these can actually only be defined as equivalence classes (afaik)
-
...
- lambda calculus
- types and a little type theory
- what are dependent types?
- polymorphism
- just enough category theory to elucidate some of the concepts we learned
- some theorem proving in proof assistants such as Isabelle and Idris
- logic programming and Prolog
- concurrency, transition systems, bisimulation
- Kripke structures, modal logic, model checking, SPIN and Promela
- extending the believes, desires, intentions paradigm in multi-agent systems
- ...
The list is long and growing. I can easily add and remove things if you have particular interests ... let me know ...