Scottish Programming Languages Seminar

Tuesday 5 June 2018
12:00 - 18:00
Cairn Auditorium, PG G.01, Postgraduate Centre (detailed directions below)
Heriot-Watt University

Please register so that catering can be ordered: doodle poll (mark only the 5 June column).
Any dietary requirements email Rob Stewart (R.Stewart@hw.ac.uk) by Friday 11 May.

Talks

  • 12:00 - Lunch

  • 12:30 - Multi-level parallelism for high performance combinatorics
    Florent Hivert, University Paris-Sud
    [slides]

    In this talk, I will report on several experiments around large scale enumerations in enumerative and algebraic combinatorics.
    I'll describe a methodology used to achieve large speedups in several enumeration problems. Indeed, in many combinatorial structures (permutations, partitions, monomials, young tableaux), the data can be encoded as a small sequence of small integers that can often efficiently be handled by a creative use of processor vector instructions. Through the challenging example of numerical monoids, I will then report on how Cilkplus allows for a extremely fast parallelization of the enumeration. Indeed, we have been able to enumerate sets with more that 10^15 elements on a single multicore machine.


  • 13:00 - AnyDSL: Building Domain-Specific Languages for Productivity and Performance
    Roland Leißa, Saarland University

    Nowadays, the computing landscape is becoming increasingly heterogeneous and this trend is currently showing no signs of turning around. In particular, hardware becomes more and more specialized and exhibits different forms of parallelism. For performance-critical codes it is indispensable to address hardware-specific peculiarities. Because of the halting problem, however, it is unrealistic to assume that a program implemented in a general-purpose programming language can be fully automatically compiled to such specialized hardware while still delivering peak performance.
    In this talk, we present AnyDSL. This framework allows to embed a so-called domain-specific language (DSL) into a host language. On the one hand, a DSL offers the application developer a convenient interface; on the other hand, a DSL can perform domain-specific optimizations and effectively map DSL constructs to various architectures. In order to implement a DSL, one usually has to write or modify a compiler. With AnyDSL though, the DSL constructs are directly implemented in the host language while a partial evaluator removes any abstractions that are required in the implementation of the DSL.


  • 13:30 - Taking Linear Logic Apart
    Wen Kokke, University of Edinburgh

    Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there has been a mismatch between the rules for constructing proofsand the term constructors of the π-calculus. We introduce the Hypersequent Classical Processes (HCP),which addresses this mismatch by using hypersequents (collections of sequents) to register parallelism inthe typing judgements. We prove that HCP enjoys deadlock-freedom and a series of properties that relate it back to CP.


  • 14:00 - Refreshments

  • 14:30 - The Syntax and Semantics of Quantitative Type Theory
    Bob Atkey, University of Strathclyde.

    I will talk about Quantitative Type Theory, a Type Theory that records usage information for each variable, refining a system by McBride. The additional usage information means that it is possible to assign a computational meaning to each term of the theory that is appropriately "resource sensitive". Practically, this means that we can compile type theory to environments where resources are scarce. Formally, it is a realisability semantics over a variant of Linear Combinatory Algebras. The semantics is defined in terms of Quantitative Categories with Families, a novel extension of Categories with Families for modelling resource sensitive type theories.


  • 15:00 - Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
    Franta Farka, Heriot-Watt University

    First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem.


  • 15:30 - Python Dynamic Source Fuzzing using Aspects
    Tom Wallis, University of Glasgow

    Aspect oriented programming is an interesting paradigm which allows a separation of cross-cutting concerns from a problem domain. Standard examples of cross-cutting concerns are things like logging or debugging code, which can be separated out from core programming logic. We produce an aspect orientation library — “ASP” — for Python 2, and demonstrate the mechanisms which help it to work — and then demonstrate that variance can be treated as a cross-cutting concern, where alterations to processes can be applied using aspects. We demonstrate that, using ASP’s mechanisms, process fuzzing libraries can be built which apply random process mutation as a cross-cutting concern. We show that this can be used for accurate modelling of socio-technical behaviour, and then demonstrate some more advanced process fuzzing aspects which can be used for the implementation of things like genetic programming.


  • 16:00 - Refreshments

  • 16:30 - Announcement
    Jeremy Singer, University of Glasgow

  • 16:35 - The language of stratified sets, Quine’s NF, rewriting, and higher-order logic: A brief tour
    Jamie Gabbay, Heriot-Watt University

    Russell's paradox is a famous inconsistency in naive set theory, that there is a set R such that R is a member of itself if and only if it is not a member of itself. Three solutions to this problem are: ZF set theory, higher-order logic, and Quine's NF.
    I will motivate and describe Quine's NF, which is a simple system to define and which depends on a beautiful and mysterious "stratification condition". I will give an accessible account of this stratification condition, embed it into higher-order logic to help make sense of it, and then approach NF from the point of view of term-rewriting to note that it has some nice properties.
    The interested reader can read a bit more in a paper just published in LMCS:
    http://www.gabbay.org.uk/papers.html#lanssc
    https://arxiv.org/abs/1705.07767

    The language of Stratified Sets is confluent and strongly normalising.


    Directions

    This map shows the location of the Post Graduate building (SPLS location):

    See full screen

    The 34 bus enters the campus via the research park. Get off at the stop indicated at the red mark above. Alternative bus services are the 25 and 45 (see below).

    SPLS is happening in G.01 (ground floor) of the postgraduate building, which looks like this:

    By bus

    Heriot-Watt is served by numerous buses. 25, 34 and 45 serve the route between the city centre and the university, with the 25 passing Haymarket Station and all three stopping near Waverley station. The cost is £1.70 per trip, and you need to have the exact fare.

  • 34 route get off at the penultimate stop on campus. The Post Graduate building is opposite the Earl Mountbatten (Computer Science) building.
  • 45 route get off at the penultimate stop on campus (same as 34).
  • 25 route get off on the final stop and enjoy the walk over The Loch.

    By train

    The closest stations to Heriot-Watt are Curriehill (where some trains to/from Glasgow Central stop), Edinburgh Park (where trains to/from the west, including some Glasgow trains, and Stirling trains stop) and Edinburgh Gateway (where trains to/from the north, including Aberdeen, Inverness and Perth trains stop). There is no public transport from any of these stations to the university, so you will need to take a taxi (5-10 minute journey) from the station. You may be able to pick one up at the station, but it is advisable to book one in advance.
    If your train doesn’t stop at any of these stations, you can get off at Haymarket and take the 25 bus from there. If you are coming from the south, you can get the 25, 34 or 45 from near Waverley.

    Social

    The upstairs area in the Haymarket Pub has been booked from 18:15. The pub is opposite the Haymarket train station, easy for onwards rail travellers.

    It's easier to get there using the 25 bus service. To get to a bus top for the 25 from the Postgraduate centre:


    There is a stop very close to the Haymarket pub.

    Alternatively, if you wish to use the 34 bus service, then the Haymarket pub is a short walk: