Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Computer Laboratory::Timothy Griffin
Part II Projects

  • Part II Project Suggestions (2017/2018)
  • If interested, please contact Tim Griffin,

  • 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.