Decisions, Puzzles and Cake

Potential supervisors: 
Description: 

Decisions

This project is about decision procedures: computer programs which decide how
to solve some logical puzzle. We can solve fun logical puzzles (for instance,
searching for a way to win a game of cards) and also address serious problems
(for instance, searching for inputs that would cause an error in an electrical
circuit).

In a serious setting, we often want a decision procedure to solve a difficult
problem as quickly as possible, and we also want to be confident that the
result is correct. For instance, if the program decides that there is no input
that would cause an error, we want to be sure that this is really the case.
This creates a design tension: complex algorithms and low-level performance
tweaks may be necessary for performance, but may decrease our confidence that
the program doing what it should.

CakeML

The CakeML compiler is designed to make it easier to produce efficient binary
programs with well-understood specifications. In principle, we can prove an
algorithm correct in HOL and extract a compiled binary with decent performance.

This setup should be ideal for implementing a decision procedure.

The Project

The goal of the project is to test out the CakeML approach for an interesting
logical problem.

The first goal is to pick out a logical problem or puzzle that will allow some
scope for optimisation of the decision procedure without introducing too much
complexity.

The remaining goals are:
- produce an efficient decision procedure, implemented in any given language
or framework, considering various algorithm and implementation choices.
- reimplement that decision procedure using the CakeML apparatus.
- compare the performance of the two implementations.
- (optional) investigate reasons for performance issues in CakeML.
- (optional) investigate a proof of correctness of the decision procedure.

Skills

There is scope in this project to use various skills from various domains
of computer science:
- algorithm design
- performance analysis and optimisation
- logic and verification
- analysing compiler performance, and possibly implementing compiler changes

Ideally the student or students taking on this project should have some
experience or former interest in some of the above areas.

Contact
Students interested in discussing this can feel free to contact
Thomas Sewell ( sewell@chalmers.se ).

Date range: 
January, 2019 to January, 2024