Seminar: The technology driving the evolution of internet advertising, targeted advertising or intrusive surveillance?

Event details

  • When: 27th February 2017 14:00 - 15:00
  • Where: Cole 1.33a
  • Series: CS Colloquia Series
  • Format: Seminar

“The technology driving the evolution of internet advertising, targeted advertising or intrusive surveillance?”

 Tim Palmer, Senior Partner, Digiterre (


Type-Driven Development of Communicating Systems using Idris

Event details

  • When: 23rd February 2017 13:00 - 15:00
  • Where: Cole 1.33b
  • Format: Colloquium, Seminar, Talk

Speaker: Jan de Muijnck-Hughes


Communicating protocols are a cornerstone of modern system design.
However, there is a disconnect between the different tooling used to design, implement and reason about these protocols and their implementations.
Session Types are a typing discipline that help resolve this difference by allowing protocol specifications to be used during type-checking to ensure that implementations adhere to a given specification.

Idris is a general purpose programming language that supports full-dependent types, providing programmers with the ability to reason more precisely about programs.
This talk introduces =Sessions=, our implementation of Session Types in Idris, and demonstrates =Sessions= ability to design and realise several common protocols.

=Sessions= improves upon existing Session Type implementations by introducing value dependencies between messages and fine-grained channel management during protocol design and implementation.
We also use Idris’ support for EDSL construction to allow for protocols to be designed and reasoned about in the same language as their implementation.
Thereby allowing for an intrinsic bond to be introduced between a protocol’s implementation and specification, and also with its verification.

Using =Sessions=, we can reduce the existing disconnect between the tooling used for protocol design, implementation, and verification.




Talk: Using cost models of algorithmic skeletons

Event details

  • When: 13th December 2016 16:00 - 17:00
  • Where: Honey 103 - GFB
  • Format: Talk


 The increasing importance of parallelism has motivated the creation of better abstractions for writing parallel software, including structured parallelism using nested algorithmic skeletons. Such approaches provide high-level abstractions that avoid common problems, such as race conditions, and often allow strong cost models to be defined. However, choosing a combination of algorithmic skeletons that yields good parallel speedups for a program on some specific parallel architecture remains a difficult task. In order to achieve this, it is necessary to simultaneously reason both about the costs of different parallel structures and about the semantic equivalences between them. This paper presents a new type-based mechanism that enables strong static reasoning about these properties. We exploit well-known properties of a very general recursion pattern, hylomorphisms, and give a denotational semantics for structured parallel processes in terms of these hylomorphisms. Using our approach, it is possible to determine formally whether it is possible to introduce a desired parallel structure into a program without altering its functional behaviour, and also to choose a version of that parallel structure that minimises some given cost model.