Note that 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. Your report does not have to be long.
You can use this report-example as a template.
The deadline for submitting your report (via email or GitHub) is Friday June 29, at 17:17. This deadline is strict.
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.
For an implementation, see NooBDD, a totally naive, inefficient and not-reducing BDD package from Malvin.
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.
Your project could be to implement classical ciphers and attacks on them: Caesar cipher, Vigenère cipher, multi-time pad, etc. Especially somewhat automated attacks would be interesting.
You might also try to use Haskell to solve the challenges from cryptography courses by Christian Schaffner: 2016, 2014, 2012 or 2011.
See https://homepages.cwi.nl/~jve/courses/16/fsa/lab/FSAlab5.html.
See https://homepages.cwi.nl/~jve/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 idea would be to visualize the dynamic gossip problem, building a better tool than webgossip.
Another project would be to combine this with the topic of Mastermind.
This will be the main lecture topic on Thursday and Friday. Especially if you have taken the course about DEL with Alexandru Baltag, this might be for you.
See DEMO-S5 for a simple explicit approach, and SMCDEL for a more sophisticated symbolic model checker for DEL.
Your project might start from scratch to implement model checking for other variants of (D)EL: neighbourhood models, infinite models, weight models, etc.
Alternatively, there are some concrete problems with SMCDEL you could tackle:
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, see https://github.com/jrclogic/SMCDEL/issues/5.
Sylvan is a new BDD software library that implements parallelized (multi-core) operations on BDDs, and that is being developed at the University of Twente.
There are Haskell bindings for this library and Malvin has an example how to use them at https://github.com/m4lvin/sylvan-haskell-example.
Your project is to investigate whether a shift to this package would speed up symbolic epistemic model checking, because the BDD packages that SMCDEL use currently (CacBDD and CUDD) are both sequential.
Update the CUDD library, see https://github.com/jrclogic/SMCDEL/issues/7.
For other aspects of model checking DEL, see also:
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.
Your project could be to write your own implementation of Dynamic Gossip or to improve upon https://github.com/m4lvin/gossip.
Jana and Malvin have ongoing work on reducing Dynamic Gossip to NetKAT, a network programming language.
If you have experience with OCaml, your project could be to get a new NetKAT decision method running and benchmark it on NetKAT formulas encoding the Dynamic Gossip problem. Start by talking to Malvin and Jana, then explore GossipKATS and frenetic.
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 https://homepages.cwi.nl/~jve/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 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 is 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.
Compare also the MoL thesis of Sarah McWhirter.
See these lecture notes, plus Computational Semantics.
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; see also Idris on Wikipedia.
Your project could be to investigate the use of Idris for writing a sample of certified programs, and document the process. See Adam Chlipala's Book Certified Programming With Dependent Types for inspiration.
Use the proof assistant Agda, programmed in Haskell, for writing and checking a number of proofs. Agda is also a functional programming language in its own right, with dependent typing.
Your report could document your experience in getting acquainted with Agda and try to prove some small results about arithmetic or logic.
Read up on generating functions, and use these to explore combinatorial problems with Haskell and report on your findings. Compare 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 category 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 to explain your implementation.
See this paper
Your project could be to implement System F with Type Equality Coercions. This is the type system behind Haskell.
Use the new GHC extensions for dependent types for a nicer implementation of the geometric solution to the Russian Cards problem. You might start by watching “Dependent Types in Haskell” by Stephanie Weirich here https://youtu.be/wNa3MMbhwS4. Then meet Esteban Landerreche.
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?
This challenge was taken up in 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.
… and so on, feel free to suggest your own topic(s)!