Date/Time
Date(s) - 15/10/2014
All Day
Location
Heriot-Watt University
SICSA is pleased to once again sponsor the Scottish Programming Languages Seminar, to be held on 15th October 2014 at Heriot-Watt University.
Please complete the doodle poll if you would like to attend.
The programme is as follows:
Keynote Title TBC. Paul Kelly, Imperial College London.
Intrinsic Security of Functional Languages: Outcome of the LaFoSec Study. Manuel Maarek, Heriot-Watt University.
The LaFoSec study aimed at investigating the impact of using functional languages for the development of secure applications. The investigation focused on three languages (OCaml, F# and Scala) and their distributions. While key features such as strong typing, encapsulation, pattern matching provide security on the cheap, some implementation details should be taken care of. The study was funded and initiated by the French Network and Information Security Agency (ANSSI) and conducted by a consortium lead by SafeRiver. We present the results of the security oriented analysis of the OCaml language, compiler and tools, and the impact the study had.
An expressive semantics of mocking. Josef Svenningsson, Chalmers University of Technology.
We present a semantics of mocking, based on a process calculus-like formalism, and an associated mocking framwork. We can build expressive mocking specifications from small, orthogonal set of operators. Our framework detects and rejects ambiguous specifications as a validation measure. We report our experience testing software components for the car industry, which needed the full power of our framework.
Traffic-Dependent Session Types. Conor McBride, Strathclye University.
Session types describe communications protocols, that is, the structure of traffic. The values of earlier traffic can affect the structure of later traffic: in classic session types, this is achieved by the & operator for protocols offering a choice and the + operator for protocols selecting. But the general idea of earlier traffic determining later structure provokes one to hope/fear that the session type setup could be streamlined by dependent types, which seem rather suited to that sort of contextualisation. After a certain amount of initial perplexity, I can now make a positive preliminary report. The key clue-question is “What is the stuff that session types classify, upon which other session types might depend?”. The answer is before us.
Using Dependent Types to Reason about Structured Parallel Programs. David Castro, St. Andrews University.
Despite the increasing importance of multi-core/many-core computers, much treatment of parallel programmimg is still very informal. There is a clear need for a formal, language-level treatment of parallelism that marries high-level abstractions with strong reasoning. This talk explores the use of dependent types to capture the structure, semantics and execution costs of parallel programs, so enabling formal reasoning about their run-time and functional behaviour. This formal reasoning allows us to apply fully automatic, and provably correct, transformations between functionally-equivalent programs with different parallel structures, and also to rationally choose between different parallel implementations, with varying execution costs, directly through their types.
Program Shaping for Parallelism. Adam Barwell, St. Andrews University.
Whilst the ubiquity of multicore processors has all but necessitated the leverage of parallelism for ever greater performance, the task of its introduction remains predominantly difficult, tedious, and error-prone. To help simplify this process, multiple approaches, such as Algorithmic Skeletons, have been developed. Yet, regardless of the method chosen, a program must fit a certain shape (i.e. fulfil certain requirements) before any such parallel components may be introduced. Most programs must therefore undergo a reshaping stage first, which, at present, must be done by hand. We propose the (semi-)automation of this stage via refactoring and the use of refactoring tools, making reshaping both simpler and safer, and illustrate a set of such refactorings that work with the Erlang skeleton library Skel.
The organiser of this event is Rob Stewart, Heriot-Watt University.
