If interested, please contact Tim Griffin, tgg22@cam.ac.uk.
Formalising fixed points of asynchronous computations in Agda
With the increasing prevalence of multi-core computers, asynchronous
computation offers one of our best hopes for significant performance gains.
Unfortunately the behaviour of asynchronous algorithms are much harder than
that of their synchronous counterparts for humans to reason about.
However several theorems exist allow proofs of properties of asynchronous
computations to be derived from proofs of the corresponding synchronous behaviour.
The project is to verify a proof published by Üresin & Dubois on the fixed point
of iterative asynchronous algorithms in Agda,
a dependently typed theorem prover slash programming language (see Part II Types course).
The proofs in question in the paper cited below.
A suitable candidate would be interested in mathematical reasoning,
functional programming and machine verification.
No previous knowledge of Agda will be assumed.
Üresin, Aydin, and Michel Dubois. "Parallel asynchronous algorithms for discrete data."
Journal of the ACM (JACM) 37.3 (1990): 588-606.