For each topic we only give a title, some literature, and a few hints. It is up to you to formulate a short research agenda, carry it out, and collect the results in a report of at most 15 pages!
You can search on hackage.org for existing packages.
Please use the report-example template. Again, the strict length limit is 15 pages.
The deadline is Friday 4 February, at 23:59. You should submit your code and your report via email or git. If you use a private git repository on GitLab or GitHub, please share it with “m4lvin”.
Grading/Passing criteria can be found in the slides of Lecture 4.
Your project could be to implement classical ciphers and attacks on them: Caesar cipher, Vigenère cipher, multi-time pad, etc. It would especially be nice to automate attacks, i.e. build a tool that takes many forms of gibberish and tries different methods to find and break the cipher that was used.
You might also try to use Haskell to solve the challenges from cryptography courses by Christian Schaffner: 2016, 2014, 2012 or 2011.
Dynamic Gossip generalizes the classic telephone problem with partial knowledge and exchange of phone numbers. For an introduction, see for example Chapter 6 of Malvin’s PhD thesis.
For existing tools, see GoMoChe and elm-gossip.
Your project could be to start from scratch and implement a variant of the gossip problem not yet covered by those tools, or to improve them with new features or extensions.
This will be the main topic of Lecture 5 and especially if you followed the DEL course with Alexandru Baltag, this might be for you.
See DEMO-S5 for a simple explicit approach, and SMCDEL for the more sophisticated symbolic model checker for DEL.
Your project can start from scratch and implement model checking for variants of DEL that are not covered by DEMO or SMCDEL so far: neighbourhood models, infinite models, weight models, probabilistic models, etc.
Alternatively, there are many problems with SMCDEL you could tackle, see https://github.com/jrclogic/SMCDEL or talk to Malvin. Examples:
Explore if a SAT solver could be used instead of BDDs. This is also known as bounded model checking (BMC).
Use the parallel BDD library Sylvan Sylvan via Haskell bindings.
Your project would be to investigate whether a shift to this package would speed up symbolic epistemic model checking, because the BDD packages that SMCDEL uses currently (CacBDD and CUDD) are both sequential.
See, e.g., hylotab, and this list of theorem provers. Interesting FOL provers are paradox and equinox. Paradox reads specifications in first order logic and tries to find finite domain models. Equinox implements theorem proving for first order logic with equality. These provers can be used to check the consistency of software specifications on small domains.
Your project could be to carry out a specific task with a prover of your choice, to compare the results of using different provers, or to write a small prover of your own for your choice fragment of modal logic. Also interesting would be to compare the use of a special purpose prover (say, for modal logic) with translating to FOL and using FOL theorem proving.
Another idea for a theorem prover for Modal Logic would be to implement a finitary canonical model construction, see the BRV book.
See basic voting theory with software, and the papers of Don Saari to get an idea of how much the voting rules influence the outcome of the vote.
Your project could be to compare the outcomes of various voting rules for given voter profiles.
See this domain-specific language for experimental game theory, with software here.
Your project could be to use the software for a game theoretic experiment in evolutionary game theory.
Compare also Babette Paping's MoL thesis
Functional programming can be used to compute optimal strategies in sequential games, as explained in Escardó and Oliva 2010. Use these ideas to define and implement some interesting sequential games, and demonstrate how optimal strategies for these can be computed.
Sudoku solving is a particular kind of a constraint satisfaction problem. A constraint satisfaction problem or CSP can be viewed as a directed graph where the nodes are the variables of the problem, and and edge from x to y indicates that the values of x are constrained by the values of y. Inspecting an edge or arc results in removing the values of x that are inconsistent with values of y. A well-known algorithm for this is AC-3.
Implement this in Haskell, and next show how it can be applied to Sudoku solving and some other problems of your choice.
Matching theory starts with the definition of stable matchings, and with the Gale-Shapley algorithm (Gale and Shapley 1962) for finding them. See Stable Marriage Problem for more information. See also Wouter Kroese's MoL thesis.
An important application is school allocation. Your project could be to carry on with the analysis of what went wrong in the Amsterdam school allocation method in Spring 2015, and to design and implement an alternative.
This challenge was taken up in the MoL thesis of Philip Michgelsen.
See also: Ronald de Haan: Why a Dutch court stopped high school students from swapping schools.
See natural logic for natural language or a brief history.
Compare also Fangzhou Zhai's MoL thesis.
Your project could be to implement a fragment of natural logic, starting from scratch or an implementation started by Larry Moss that your can get from Malvin.
There is a connection with graph theory. The Floyd-Warshall algorithm can be viewed as an implementation of Kleene's construction of a regular expression from a nondeterministic finite automaton. See regular language.
Your project could be to implement finite automata in Haskell, and implement translations between finite automata and regular expressions.
A first step here would be to implement the Powerset construction
Compare also the MoL thesis of Sarah McWhirter.
See these lecture notes.
Your project could be to extend the imperative programming language of the lecture notes with procedures (see procedural programming), and to develop read and show functions for imperative programs, thus developing a language for imperative programming as a DSL within Haskell.
Programming can be related to proof theory by taking proofs in a suitable logical system (such as the Calculus of Constructions) and extract programs from these. See Paulin-Mohring 1989.
Your project could be to illustrate this by means of an implementation.
Compare also the MoL thesis of Hans Bugge Grathwohl.
In a type theory with dependent types it is possible to formalize proofs of programs, which enables the development of programs that carry their own correctness proofs with them, so called certified programs. A suitable language for this is Idris.
Your project could be to investigate the use of Idris for writing model checkers as we discussed in the course, as a certified program, and document your process. See also Adam Chlipala's Book Certified Programming With Dependent Types for inspiration.
Read up on generating functions, and use these to explore combinatorial problems with Haskell and report on your findings. See Chapter 10 of The Haskell Road book.
Your project could be to solve a number of problems from combinatorics and probability theory with generating functions.
See Wikipedia book on graph algorithms.
Your project could be to give Haskell implementations of a number of graph algorithms for finding connected components or for computing shortest paths, and compare these for a number of possible graph representations (adjacency matrix, adjacency lists, lists of edge pairs).
See Lambda calculi with types by H. P. Barendregt (1992) and the book by H. Barendregt, Dekkers, and Statman (2011), with this summary.
Your project could be to implement the simply typed lambda calculus, and then to test and explain your implementation. Additional inspiration for this can be found in many blog posts, ranging from this simple version by Jim Fisher to this elaborate version by Tobin Yehle.
See this paper.
Your project could be to implement System F with Type Equality Coercions. This is the type system behind Haskell.
Genetic programming or evolutionary computation is a paradigm for programming by evolutionary refinement that is inspired by biological evolution. Good places to start are this list of FAQs and this textbook by David Goldberg. What makes the topic fascinating are the connection with evolutionary game theory and the fact that the approach often offers useful answers to difficult scheduling problems with relatively litte programming effort.
Your project could be to tackle a difficult scheduling problem with this genetic programming library, and report on the results.
You can also talk to Jana about this, she did a project on Genetic Algorithms.
See also the MoL thesis of Philip Michgelsen.
Mutation testing is a method to evaluate the quality of existing specification-based software tests. The method: create a number of mutants of a program under test by modifying the program in small ways, and check which proportion of the mutants is killed off by the specification.
Mutation testing is a bit hard to apply to strongly typed programs, as most of the mutants would be killed off immediately by the type checker.
Your project could be to study the prototype mutation testing tool for Haskell MuCheck, and investigate how well it does on a number of Haskell functions for which you have given QuickCheck specifications. Next, discuss if it is possible to extend MuCheck with new methods for mutant generation?
See also Joel Bartholomew's Master of Software Engineering Thesis.
See Wikipedia on Argumentation framework and the paper An abstract, argumentation-theoretic approach to default reasoning by Bondarenkoa, Dung, Kowalskic and Tonic https://doi.org/10.1016/S0004-3702(97)00015-5.
You project could be to implement argumentation graphs and algorithms that compute stable or defendable sets of arguments according to the definition from the literature.
For more inspiration, see also the PhD thesis Reason to Believe by Chenwei Shi.
Binary Decision Diagrams are an interesting and powerful data structure to represent boolean functions. Donald Knuth’s 17th Christmas Tree Lecture is probably the best introduction, next to the chapter in his The Art of Computer Programming: Combinatorial Algorithms, Part 1, vol. 4A. (2011), pp. 202–280.
NooBDD is a totally naive, inefficient and not-reducing BDD package by Malvin. A better package is obdd. More efficient BDD packages are written in C or C++, but can still be used from Haskell via bindings. See for example HasCacBDD and sylvan-haskell.
Your project goal could be to make a review study of existing Haskell libraries, with benchmarks etc. or even to write your own BDD library.
See https://staff.fnwi.uva.nl/d.j.n.vaneijck2/courses/16/fsa/lab/FSAlab2.html.
Do a detailed comparison of mastermind strategies. Another possibility is to investigate which of the mastermind strategies translate to strategies for balance and coin problems.
See https://staff.fnwi.uva.nl/d.j.n.vaneijck2/courses/16/fsa/lab/FSAlab5.html.
See https://staff.fnwi.uva.nl/d.j.n.vaneijck2/courses/16/fsa/lab/FSAlab3.html.
The language elm is a Haskell-like language for the web that compiles to JavaScript and runs in a browser. See http://elm-lang.org/ and read https://guide.elm-lang.org/architecture/.
One approach here would be to reimplement a program you saw in the course in Elm instead of Haskell. Another way would be to do any of the other topics mentioned here but then do it in Elm instead of Haskell.
… and so on, feel free to suggest your own topic!