In this thesis, we develop a new library for Agda named Attic, which allows us to create and compose proof tactics that can be used to generate terms through reflection. Such tactics can be converted to Agda macros, allowing them to be used in term positions where they can generate term solutions of the expected type. Tactics can make the development of proofs faster by making proofs easier to read and write.

This project can be seen as a sister project to Ataca, which is an earlier attempt at developing tactics that operate through reflection. Attic explores new mechanisms of operation, such as non-determinism with iterators to allow for multiple solutions, and the use of deferred unification, so that the final proof term is only fully constructed at the end of tactic evaluation.

To allow for the representation of both finite and infinite sequences that can be consumed step-by-step, we have implemented the iterator data type in Agda. Although iterators existed in other systems previously, an Agda implementation had not been made. These iterators underpin the branching mechanism in tactic instructions, and support operations that can be used to generate, transform and filter values.

Finally, we have implemented a number of tactics and operations that are commonly found in other proof assistants. We also compare the resulting library to the Ataca library and examine the differences in runtime for a small test case. While Attic is not yet a complete solution, we present new ideas that may be incorporated in future tactic systems. ... Read more

For this project, JEM-id tasked us with creating a proof of concept of a new online auction in the form of a web application for Royal FloraHolland. JEM-id is a software company operating in the agricultural domain.
The pre-existing digital auction is not available as a web application and has generated technical debt over the past twenty years of it is existence.

The main challenge of the project was to make sure the application is capable of sufficiently handling the current load of the auction while maintaining similar performance. This translates to a stable connection with a ping of fewer than 30 milliseconds for clients within the Netherlands.
On top of that, the system had to be scalable to support higher numbers of buyers in the future.
We used a microservice architecture able to balance the load over several servers to resolve this.
We spread the load of communicating with clients to services separate from the main application service.
This allowed the main application service to solely and adequately keep track of the state of the clock and determine the winner of a session.

To validate that we indeed achieved the main goals of the project, we created a simulation that would simulate any number of clients connecting to the clock auction and placing bids.
In this process, we generated buyer and auctioneer behaviour by analysing transaction data. We extracted several distributions from the data and sampled from it to make it more realistic.
In the end, we ran this simulation ten times for chunks of an auction with 610 connected clients.
A few peaks showed up where pings from client to server were significantly higher than usual. However, in the long run, the system showed low standard deviations in ping, meaning the general consistency was high.
Overall, the results we gathered showed that our application was able to deal with 610 connected clients.

In the end, we consider our project to be a success.
First of all, we showed that a clock application in the browser can be implemented with seven weeks of development time.
Secondly, we showed that such an application could handle a realistic amount of traffic without much trouble, given sufficient computing resources.
These two accomplishments show that replacing the current clock application with a web-based application is feasible. ... Read more