Talk

Type-Driven Development of Communicating Systems using Idris

Speaker: Jan de Muijnck-Hughes

Abstract

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.

 

 

 

Event details

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

Talk: Using cost models of algorithmic skeletons

Abstract:

 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.

Event details

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

Multi-modal Indoor Positioning: Trends and Challenges by Prof. Niki Trigoni, Oxford University

Abstract:

GPS has enabled a number of location based services outdoors, but the problem of localisation remains open in GPS-denied environments, such as indoors and underground. In this talk, I will discuss the key challenges to accurate and robust position estimation, and will describe a variety of sensor modalities and algorithms developed at Oxford to address this problem.

The talk will cover inertial, radio-based and vision-based localisation approaches and their advantages and disadvantages in different settings.

 

Short Bio:

Niki Trigoni is a Professor at the Oxford University Department of Computer Science and a fellow of Kellogg College. She obtained her PhD at the University of Cambridge (2001), became a postdoctoral researcher at Cornell University (2002-2004), and a Lecturer at Birkbeck College (2004-2007). Since she moved to Oxford in 2007, she established the Sensor Networks Group, and has conducted research in communication, localization and in-network processing algorithms for sensor networks. Her recent and ongoing projects span a wide variety of sensor networks applications, including indoor/underground localization, wildlife sensing, road traffic monitoring, autonomous (aerial and ground) vehicles, and sensor networks for industrial processes.

Event details

  • When: 8th November 2016 14:00 - 15:00
  • Where: Cole 1.33
  • Series: School Seminar Series
  • Format: Seminar, Talk

Quicker Sort by Dietmar Kühl, Bloomberg L.P.

 

Abstract:

Quicksort is a well-known sorting algorithm used to implement sort functionality in many libraries. The presentation isn’t really about the algorithm itself but rather about how to actually create an efficient implementation of the algorithm: a text-book implementation of the algorithm actually is not that quick (even if the pivot is chosen cleverly). It takes paying some attention to detail to improve the implementation significantly. This presentation starts with a simple implementation and makes incremental improvements to eventually yield a proper generic and fast sorting function. All code will be in C++ but it should be possible to follow the majority of the reasoning with knowledge of another programming language.

 

Short Bio:

Dietmar Kühl is a senior software developer at Bloomberg L.P. working on the data distribution environment used both internally and by enterprise installations at clients. Before joining Bloomberg he has done mainly consulting for software projects in the finance area. He is a regular attendee of the ANSI/ISO C++ standards committee, presents at conferences, and he used to be a moderator of the newsgroup comp.lang.c++.moderated. He frequently answers questions on Stackoverflow.

Event details

  • When: 25th October 2016 14:30 - 15:30
  • Where: Cole 1.33
  • Series: School Seminar Series
  • Format: Seminar, Talk

School Seminar ‘Closure Experiences in Digital Product Design’ by Joe Macleod

“Closure Experiences in Digital Product Design. The loss of the resolution in the shop of abundance”

F8_2bLVV

Abstract
Most experiences in life are punctuated by a closure experience. In the past these were profound; however, over generations we have distanced ourselves from meaningful closure experiences thanks to our lifestyles increasing in comfort, the church weakening and medicine advancing. This has seemingly freed us from the shackles of the ultimate closure experience – death – and sanctioning our personal pursuit of heaven on earth in the form of consumption. We are now encouraged to drunkenly stumble from purchase to purchase, with any sense of longevity and responsibility removed. Long term side effects of this are exampled in the Product, Service and Digital landscapes that we frequent. The consequences of our behaviour results in a changing climate, industries fined billions for mis-selling and individuals casually eroding their personal online reputations. Many of us are active in the creation of services, products or digital products; making them attractive, engaging and usable for consumers, but we often overlook concluding these experiences for the user in a responsible way. Closure Experiences offers a model to frame this change.

Bio
Joe Macleod has been working in the mobile design space since 1998 and has been involved in a pretty diverse range of projects. At Nokia he helped develop some of the most streamlined packaging in the world, he created a hack team to disrupt the corporate drone of powerpoint, produced mobile services for pregnant women in Africa and pioneered lighting behavior for millions of phones. For the last four years he has been key to establishing ustwo as the UKs best digital product studio, with 180 people globally in London, New York, Sydney and Sweden, while also successfully building education initiatives, curriculums and courses on the back of the IncludeDesign campaign which launched in 2013. He now works independently on projects and has recently established established Closure Experiences, a new business looking at issues around consumption, consumerism and designing the end of things.

Event details

  • When: 29th March 2016 14:00 - 15:00
  • Where: Cole 1.33
  • Series: School Seminar Series
  • Format: Seminar, Talk

School Seminar ‘Paraphrase Generation from Latent-Variable PCFGs for Semantic Parsing’ by Shashi Narayan

Abstract:

One of the limitations of semantic parsing approaches to open-domain question answering is the lexicosyntactic gap between natural language questions and knowledge base entries — there are many ways to ask a question, all with the same answer. In this paper we propose to bridge this gap by generating paraphrases to the input question with the goal that at least one of them will be correctly mapped to a correct knowledge-base query. We introduce a novel grammar model for paraphrase generation that does not require any sentence-aligned paraphrase corpus. Our key idea is to leverage the flexibility and scalability of latent-variable probabilistic context-free grammars to sample paraphrases. We do an extrinsic evaluation of our paraphrases by plugging them into a semantic parser for Freebase. Our evaluation experiments on WebQuestions benchmark dataset show that the performance of the semantic parser significantly improves over strong
baselines.

Bio:

Shashi Narayan is a research associate at School of Informatics at the University of Edinburgh. He is currently working with Shay Cohen onthe problems of spectral methods for parsing and generation. Before,he earned his doctoral degree in 2014 from Université de Lorraine,under the supervision of Claire Gardent. He received Erasmus MundusMasters scholarship (2009-2011) in Language and CommunicationTechnology (EM-LCT). He did his major in Computer Science and Engineeringfrom Indian Institute of Technology (IIT), Kharagpur India. He is interested in the application of syntax and semantics to solvevarious NLP problems, in particular, natural language generation,parsing, sentence simplification, paraphrase generation and questionanswering.

Event details

  • When: 26th January 2016 14:00 - 15:00
  • Where: Cole 1.33
  • Series: School Seminar Series
  • Format: Seminar, Talk

Seminar: “Data Exploration on Smart watches” by Dr Rachel Menzies

rachel menzies

Abstract:

For many of us, interacting with data on mobile devices such as phones and tablets is commonplace in our lives, e.g. phone call data, TV guide, maps, fitness and wearable data. With the introduction of smart watches, the screen size of mobile devices has dramatically decreased. This reduction in screen real estate provides challenges for the design of interfaces, including the presentation and exploration of data visualisations. Using bar charts as an example, this presentation will explore the shortcomings of current zooming techniques on very small screens and consider proposed guidelines for the development of simple data exploration applications. Key design features such as the need for overview and context will be considered in respect to a simple and effective data exploration task.

 

Biography:

Rachel Menzies is a lecturer and Head of Undergraduate Studies (Computing) at the School of Science and Engineering at the University of Dundee. Her research interests include user centred design with marginalised user groups, such as users with disabilities, as well as exploring novel interfaces, data visualisation and CS education. Rachel is an Accessibility and Usability Consultant with the Human Centred Computing Consultancy, run by the University of Dundee, and has worked for many large international clients as well as providing bespoke training sessions to small companies.

Event details

  • When: 23rd February 2016 14:00 - 15:00
  • Where: Cole 1.33
  • Series: School Seminar Series
  • Format: Seminar, Talk

The scientific life of Ada Lovelace

Prof. Ursula Martin will be talking about the letters of Lady Ada Lovelace at 5.30pm on Thursday 17th December in Abertay University (Kydd Building, Bell St, Dundee, behind Dundee High School).

This is a BCS sponsored event and all are welcome. Teas/Coffees from 4.30pm. PhD research posters will also be on display.

Event details

  • When: 17th December 2015 16:30 - 18:30
  • Format: Talk

Seminar: “Interaction, Embodiment and Technologies in Early Learning” by Dr Andrew Manches

as

Abstract: 

 

Most of us might agree that ‘hands-on learning’ is good for children in the early years. But why? Is it simply more fun and sociable, or are there any more direct cognitive benefits? And what determines definitions of ‘hands-on’? Can we include iPads? This talk will draw upon an ESRC-funded project to examine the educational implications of recent theoretical arguments about the embodied nature of cognition. Video data from the project will be used to illustrate the methodological significance of the way children gesture when describing mathematical concepts and evaluate a hypothesis that numerical development is grounded upon two particular embodied metaphors. If correct, this presents a serious challenge to traditional approaches to the types of learning materials we offer children. The talk then demonstrates two embodied technologies to consider the potential of new forms of digital interaction to further our understanding of embodied cognition as well as support early learning.

 

 Bio:  

 

Dr Andrew Manches is a Chancellor’s Fellow in the School of Education and leads the Children and Technology group at the University of Edinburgh.  He has 20 years experience working with children, first as a teacher, then as an academic. His recent research, funded by an ESRC Future Research Leader grant, focuses on the role of interaction in thinking, and the implications this has for early learning and new forms of technology.  When not being an academic, Andrew is a parent of two young children and directs an early learning technology start-up that was awarded a SMART grant this year to build an early years maths tangible technology.

Event details

  • When: 24th November 2015 14:00 - 15:00
  • Where: Cole 1.33a
  • Series: School Seminar Series
  • Format: Seminar, Talk