Date/Time
Date(s) - 05/06/2018
12:00 pm - 8:00 pm
Location
Earl Mountbatten Building, Heriot Watt University
The SICSA Theory, Modelling and Computation Research Theme is pleased to be sponsoring the next Scottish Programming Languages Seminar (SPLS) which is being held on 5th June 2018 at Heriot Watt University.
The Scottish Programming Languages Seminar is a forum for discussion of all aspects of programming languages. We meet for a day or afternoon once every few months, at some congenial location in Scotland. Talks by Scots and by visitors are welcome. Please contact us if you would like to host a meeting or give a talk.
Meetings are open, and all are welcome to attend. If you are travelling far or if you do not subscribe to the mailing list, you are advised to contact the organiser to check that there have been no last-minute changes.
Talks
12:00 – Lunch
12:30 – Multi-level parallelism for high performance combinatorics
Florent Hivert, University Paris-Sud
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 – 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.
Please register so that catering can be ordered: doodle poll (mark only the 5 June column).
SPLS receives financial support from the Theory, Modelling and Computation theme of SICSA, the Scottish Informatics and Computer Science Alliance.
