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 (maybe in the spirit of the exercises of the lab sessions), carry it out, and collect the results in a report. Your report does not have to be long.
The deadline for submitting your report (via github) is Friday October 28, at midnight.
Upon request of the director of the MoL programme, this deadline is strict.
Information Feedback Games
Continue the homework of week 2 and 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.
Automated Theorem Proving. 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.
Binary Decision Diagrams (BDDs)
Donald Knuth's 17th annual 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 and not-reducing BDD package from Malvin.
Epistemic model checking. See DEMO-S5 for a simple-minded approach, and SMCDEL for a more sophisticated checker.
Compare Iris van de Pol's MOL thesis, and also the MOL thesis of Malvin Gattinger.
Your project could be to do an experiment with symbolic model checking and SAT solving, and compare with the SMCDEL method of using a BDD package.
Symbolic Model Checking for DEL
Malvin is working on this. See SMCDEL, which uses BDDs.
Your project could be to use the checker for checking example DEL formulas of interest.
Speeding up Symbolic Model Checking
This is related to the previous project. 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.
The project is to investigate whether a shift to this package would speed up symbolic epistemic model checking (the BDD packages that are in use right now are all sequential). Malvin has further details.
Voting Theory. 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.
Game theory. 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.
Selection Functions and Sequential Games
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.
Functional Programming and Constraint Programming
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 algorithms
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.
Computational Semantics with functional programming. See www.computational-semantics.eu.
Your project could be to extend one of the fragments for natural language in the book, or to develop a fragment of your own.
Generalized quantifiers for natural language semantics. See www.computational-semantics.eu. See also Jakub Szymanik's Quantifiers and Cognition book.
Your project could be to link up with the literature on the connection between generalized quantifiers and finite automata, and to implement back and forth translations between generalized quantifiers and finite automata.
Natural Logic. 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.
Finite automata. 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.
Imperative programming language semantics. See the lecture notes for week 2, 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.
Proof Theory and Functional Programming. 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) which can be found here.
Your project could be to illustrate this by means of an implementation.
Compare also the MOL thesis of Hans Bugge Grathwohl.
Certified Programming. 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.
Using a Proof Assistant
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 also document your experience in getting acquainted with Agda.
Functional programming and category theory. See Categorical Programming with Inductive and Coinductive Types and Computational Category Theory.
Your project could be to implement a fragment of computational category theory.
Categories and Monads. Start with monads made difficult by Stephen Diehl, and explore the connection between monads in Haskell and basic category theory.
Your project could be a critical comparison between various monads tutorials, with the one by Stephen Diehl at one end of the spectrum, and this one at the other end.
Generating Functions and Combinatorics. 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.
Your project could be to solve a number of problems from combinatorics and probability theory with generating functions.
Functional Programming and Graph Algorithms. See this wikibook 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).
Functional Programming and Model Checking of Cryptographic Protocols.
Talk to Malvin Gattinger, or look at his website, and follow the link to epistemic crypto logic.
The challenge here is to find compact representations for knowledge and ignorance of large keys (huge integers). In Malvin's MSc thesis there is a worked example: a check that the Diffie-Hellman key exchange protocol is correct.
Type theory. See the paper (H. P. Barendregt 1992) (link is here) and the book (H. Barendregt, Dekkers, and Statman 2011)(link is here), with this summary.
Your project could be to implement the simply typed lambda calculus, and explain the implementation.
Type Theory. See this paper.
Your project could be to implement System F with Type Equality Coercions. This is the type system behind Haskell.
Extensions of Type Theory behind Haskell. See these papers.
Your project could be to explore some state-of-the-art extensions of the type theory behind Haskell, and explain.
Genetic Programming
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.
Mutation Testing
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.
and so on ...
Barendregt, H. P. 1992. “Handbook of Logic in Computer Science (Vol. 2).” In, edited by S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, 117–309. New York, NY, USA: Oxford University Press, Inc. http://dl.acm.org/citation.cfm?id=162552.162561.
Barendregt, Henk, Wil Dekkers, and Richard Statman. 2011. Lambda Calculus with Types. Cambridge University Press.
Escardó, Martín, and Paulo Oliva. 2010. “Sequential Games and Optimal Strategies.” Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences. The Royal Society. doi:10.1098/rspa.2010.0471.
Gale, D., and L. Shapley. 1962. “College Admissions and the Stability of Marriage.” American Mathematical Monthly 69: 9–15.
Paulin-Mohring, C. 1989. “Extracting $$’s Programs from Proofs in the Calculus of Constructions.” In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 89–104. POPL ’89. New York, NY, USA: ACM. doi:10.1145/75277.75285.