Congratulations to To Masih Hajiarabderkani, who has successfully defended his PhD thesis. Pictured celebrating with supervisor Dr Graham Kirby and Internal examiner Dr John Thomson.
PhD Viva Success
Congratulations to Ruth Hoffmann and Jonathan Ward who passed their PhD vivas earlier this week. Ruth is pictured with Dr Tom Kelsey (internal examiner) and Jonathan (top left) with his PhD supervisor Dr Adam Barker. We look forward to celebrating their achievements at June Graduation.
Type-driven Verification of Communicating Systems in Idris
Speaker: Edwin Brady
Abstract: Idris (http://idris-lang.org/) is a general-purpose programming language with an expressive type system which allows a programmer to state properties of a program precisely in its type. Type checking is equivalent to formally and mechanically checking a program’s correctness. Introductory examples of programs verified in this way typically involve length preserving operations on lists, or ordering invariants on sorting.
Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will give an introduction to programming in Idris, with demonstrations, and show how its advanced type systems allows us to express such interactions precisely. I will show how it supports verification of stateful and communicating systems, in particular giving an example showing how to verify properties of concurrent communicating systems.
Bio: Edwin Brady is a Lecturer in Computer Science at the University of St Andrews. His research interests include programming language design, in particular type systems and domain specific languages. He leads the design and implementation of the Idris programming language, a general purpose functional programming language with dependent types, which he uses to implement verified domain specific languages. When he’s not doing that, he’s likely to be playing a game of Go, wrestling with the crossword, or stuck on a train somewhere.
Event details
- When: 7th April 2015 14:00 - 15:00
- Where: Cole 1.33a
- Series: School Seminar Series
- Format: Seminar
April 13th, seminar by Nicolai Marquardt: Towards Ad-hoc Collaboration Spaces with Cross-Device Interaction Techniques
Speaker: Nicolai Marquardt, University College London
Date/Time: 1-2pm April 13, 2015
Location: CS1.33a, University of St Andrews
Abstract:
Despite the ongoing proliferation of devices and form-factors such as tablets and electronic whiteboards, technology often hinders (rather than helps) informal small-group interactions. Whereas natural human conversation is fluid and dynamic, discussions that rely on digital content—slides, documents, clippings—often remain hindered due to the awkwardness of manipulating, sharing, and displaying information on and across multiple devices. Addressing these shortcomings, in this talk I present our research towards fluid, ad-hoc, minimally disruptive techniques for co-located collaboration by leveraging the proxemics of people as well as the proxemics of devices. In particular, I will demonstrate a number of cross-device interaction techniques—situated within the research theme of proxemic interactions—that support nuanced gradations of sharing. I will also introduce different novel hybrid sensing approaches enabling these interaction techniques and discuss future research directions.
Bio:
Nicolai Marquardt is Lecturer in Physical Computing at University College London. At the UCL Interaction Centre he is working in the research areas of ubiquitous computing, physical user interfaces, proxemic interactions, and interactive surfaces. He is co-author of the books Proxemic Interactions: From Theory to Practice (Morgan & Claypool 2015) and Sketching User Experiences: The Workbook (Elsevier, Morgan Kaufmann 2012).
This seminar is part of our ongoing series from researchers in HCI. See here for our current schedule.
Following on from Nicolai Marquardt’s successful talk his slides can now be viewed here: St Andrews guest lecture Nicolai Marquardt – Slide Presentation
Event details
- When: 13th April 2015 13:00 - 14:00
- Where: Cole 1.33a
- Format: Seminar
New EPSRC project C3: Scalable & Verified Shared Memory
C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence
Dr Susmit Sarkar
Susmit Sarkar with colleagues in the University of Edinburgh and Intel as project partners, have been successful in their application to the EPSRC for their project C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence. This 3 year project starts in July 2015 and aims to realise scalable and verified shared memory.
Shared-memory multi-core processors are ubiquitous, but programming them remains challenging. The programming model exposed by such multi-core processors depends crucially on a “memory consistency model” (MCM), a contract between the hardware and the programmer, which essentially specifies what value a read can return. On the hardware side, one key mechanism to implement the memory consistency model is the “cache-coherence protocol” (CCP), which essentially communicates memory operations between processors. However, the connection between the CCP and the MCM remains unclear. This is especially true for modern CCPs and MCMs, in which CCP design has been divorced from the requirements of the MCM. Susmit and his colleagues argue that this has negatively impacted the scalability and the verifiability of CCPs.
On the scalability front, there are serious question marks about sustaining cache coherence as the number of cores continue to scale. On the verification front, the application of existing verification techniques, which do not verify the CCP against the MCM, are arguably broken.
The C3 proposal, proposes a family of CCPs that are “aware” of, and verified against the MCM. Their approach is motivated by the fact that both hardware and programming languages are converging to various relaxed MCMs for performance oriented reasons. The team use such relaxed MCMs as inspiration to research CCPs that can take advantage of them.
Specifically, they will research “lazy” CCPs where memory operations are batched, and the cost of communicating a memory operation can be amortised. They will also, for the first time, formally verify the relationship between the hardware CCPs and the programmer-oriented MCM they provide. They will investigate rigorously the gains to be had from such lazy CCPs. The team will do this by creating a multi-core silicon prototype of our proposed CCP, leveraging our experience in the design of industrial-strength micro-architectures and their implementations.
Mario Kart Around the World
The School recently hosted “Mario Kart Around the World” for students from Newport Primary.
All versions of Mario Kart with the exception of arcade versions were available for the youngsters to play. Our visitors had access to a range of consoles and games ranging from Vectrex to Leap Motion and a great opportunity to see modern equipment and how it looked in the “olden days“.
Staff were pictured testing out the equipment ( by way of playing Mario Kart) post event. Peter Nightingale (top left) is pictured playing the Vectrex Home Arcade System. Jon Lewis (bottom left) was seen tackling Elite on the Sinclair Spectrum.
The successful event was organised by Ruth Letham with help from Ian Gent, Jon Lewis, Peter Nightingale, Chris Jefferson, Ian Miguel, Gonzalo Mendez and Shyam Reyal.
Images Courtesy of Ian Miguel and Ian Gent.
Torchlit Procession
The Torchlit Procession and Rectorial Drag are historic university traditions, in February the soon-to-be-installed Rector Catherine Stihler addressed all students in St Mary’s Quad. The Torchlit Procession later in the evening left from Sallies Lawn where students collected and lit their torches. The walk continued down to the pier offering some fabulous photographic opportunities.
Stunning images from the procession were captured by MSc students Xu Zhu and Fearn Bishop.
School Hosts StacsHack 2015
The School hosted a hugely successful StacsHack last month. We congratulate Stacs St Andrews Computing Society for organising and running a fantastic event. Hackathons allow students with a range of talents and aptitudes to form groups and create innovative projects in 24hrs. It’s clear from the many photos that great fun was had by all. View some of the winning projects at the challenge post submission gallery.
Thanks to Gala Malbasic, Nick Tikhonov, Ieva Vasiļjeva and Vika Anisimova for representing the School of Computer Science in such a positive way and for all their hard work and enthusiasm.
Sponsors: Palantir, J.P. Morgan, Braintree_Dev, Bloomberg and Thalmiclabs.
MLH Hardware Lab partners: Oculus VR, Pebble, Thalmic Labs, Sparkfun, Estimote, Leap Motion and Spark.
Images courtesy of Gala Malbasic and Major League Hacking.
March 10th, seminar by Nick Taylor: Sustaining Civic Engagement in Communities
Speaker: Nick Taylor, University of Dundee
Date/Time: 2-3pm March 10, 2015
Location: CS1.33a, University of St Andrews
Abstract:
Engagement with local issues is typically very low, despite digital technologies opening up more channels for citizens to access information and get involved than ever before. This talk will present research around the use of simple physical interfaces in public spaces to lower barriers to participation and engage a wider audience in local issues. It will also explore the potential for moving beyond top-down interventions to support sustainable grassroots innovation, in which citizens can develop their own solutions to local issues.
Bio:
Nick Taylor is a Lecturer and Dundee Fellow in the Duncan of Jordanstone College of Art and Design at the University of Dundee. His research interests involve the use of novel technologies in social contexts, particularly in communities and public spaces. This has involved the exploration of technologies to support civic engagement in local democracy, public displays supporting community awareness and heritage, as well as methods of engaging communities in design.
This seminar is part of our ongoing series from researchers in HCI. See here for our current schedule.
Event details
- When: 10th March 2015 14:00 - 15:00
- Where: Cole 1.33a
- Format: Seminar
CNC Router Test PCB Made
The first real test of the CNC Router milling a printed circuit board took place this week and the results so far are very encouraging.
The PCB design is part of a suite of hardware required for a research project. This involves the development of a Science grade Arduino we have called Scienceduino , it will be used to log analogue data with a high degree of accuracy and traceability , in terms of readings and time logging. The picture of the complete PCB shows the complexity and general layout of the components , these will be mostly surface mount. Surface mount technology is being used to help reduce the overall size of the system and to allow automated manufacture.
The microscope webcam picture shows a circular pad which is 1.0mm in diameter , track width of 0.35mm and track spacing of 0.35mm. The copper flakes in the gaps on the PCB will be cleaned away with water and detergent. So all in all this is good news for the School’s ability to manufacture PCB’s for various research projects.