HIPERFITHIPERFIT Workshop
HIPERFIT Technical Workshop
On November 16, 2017, HIPERFIT is hosting a workshop for HIPERFIT partners, faculty, and other people interested in technical topics related to HIPERFIT activities. The presentations will include presentations both by researchers external to HIPERFIT and by HIPERFIT researchers themselves.
This event, together with the HIPERFIT Summit held on November 17, 2017, marks the end of the HIPERFIT research center, as we know it. We will, continue to operate under the name of HIPERFIT, but funding for a number of the research projects are ending, which, of course, opens up avenues to new opportunities.
The Venue
DIKU, Aud 3, HCØ, Universitetsparken 5, DK-2100 Copenhagen.
Schedule November 16, 2017
- 08:55
- Welcome (Fritz Henglein, DIKU)
- 09:00
- Partial Evaluation and Formalisation (Chair: Cosmin Oancea)
- 09:00
- Object-oriented partial evaluation and the expression problem (Alan Mycroft, U. of Cambridge)
- 09:30
- Nominal techniques in Coq (Danil Annenkov, DIKU)
- 10:00
- Coffee Break
- 10:30
- Finance (Chair: Mogens Steffensen)
- 10:30
- Special FX (Rolf Poulsen, MATH)
- 11:00
- Household finance (Maj-Britt Nordfang, MATH)
- 11:30
- Modelling stochastic volatility in forward markets (Fred Esben Benth, U. of Oslo)
- 12:00
- Lunch
- 13:00
- Blockchain Technology (Chair: Martin Elsman)
- 13:00
- Automated execution of financial contracts on blockchain (Omri Ross, DIKU)
- 13:30
- Mini Coffee Break
- 13:45
- Streaming and Life-Insurance on GPUs (Chair: Ken Friis Larsen)
- 13:45
- Streaming data-parallelism (Andrzej Filinski, DIKU)
- 14:15
- Stream fusion: from staging to ahead-of-time compilation through Scala Native (Aggelos Biboudis, École Polytechnique Fédérale de Lausanne)
- 14:45
- Domain-specific languages and GPGPUs in life insurance and pensions (Peter Sestoft, ITU)
- 15:15
- Coffee Break
- 15:45
- Data-parallel Programming (Chair: Fritz Henglein)
- 15:45
- Design and implementation of the Futhark programming language (Troels Henriksen, DIKU)
- 16:15
- Futhark: Challenges and Future Research Directions (Cosmin Oancea, DIKU)
- 16:45
- APL on GPUs--a progress report with a touch of machine learning (Martin Elsman, DIKU)
- 17:15
- Closing Remarks (Fritz Henglein, DIKU)
- 17:20
- Chat and Snacks
(Updates and Changes to the program may occur.)
Abstracts for Talks on November 16, 2017
09:00-10:00 Partial Evaluation and Formalisation
Object-oriented partial evaluation and the expression problem (Alan Mycroft, U. of Cambridge)
Object-oriented and functional languages rest on differing foundations and the ‘expression problem’ captures the idea that their inter-translation (‘transpilation’) is non-modular; this suggests that automated transpilation is likely to be ad-hoc or clumsy.
We show this to be false. By creating a partial evaluator for a pure Java-like language with a focus on class specialisation and applying it to an interpreter for an ML-like language we show that the seemingly idiomatic transformation from sum types to a class hierarchy arises naturally.
In common with many partial-evaluation tools, our initial translation is untyped, but we also show how slightly richer analysis can produce a typed translation which is close to what a human might produce.
Nominal techniques in Coq (Danil Annenkov, DIKU)
Variables and binding are ubiquitous concepts in programming language research. In pen-and-paper proofs about programming language semantics one usually applies Barendregt’s informal variable convention: all bound variables can be chosen to be different from the free variables. This convention allows for reasoning in the presence of restrictions on freshness of bound variables involved in a proof. It is essential to give a formal justification for the variable convention at least for two reasons. First, applying the convention may lead to unsound reasoning. Second, it is impossible to formalise proofs, which use the informal variable convention. In this talk we present a theory of nominal sets (Gabbay, Pitts 2002) and techniques for dealing with bound variables based on this theory. We discuss applications of these techniques to development of proofs in the Coq proof assistant, show examples in simply-typed lambda calculus, and outline some applications to ongoing work on module system formalisation.
10:30-12:00 Finance
Special FX (Rolf Poulsen, MATH)
Special events call for special techniques – also in quantitative finance. In this talk I look at two such fairly recent events from the world of exchange rates (FX): The Swiss Floor and Brexit/Trump.
Household finance (Maj-Britt Nordfang, MATH)
What is the optimal mortgage and how are pension savings optimally invested? In this presentation I will discuss the design of financial contracts in relation to the preferences of individual household consumers.
Modelling stochastic volatility in forward markets (Fred Esben Benth, U. of Oslo)
TBA.
13:00-13:30 Blockchain Technology
Automated execution of financial contracts on blockchain (Omri Ross, DIKU)
In this presentation we outline how certain financial contracts can be managed and executed automatically on the Ethereum block-chain system. The system is based on a domain-specific language for financial contracts that is capable of expressing complex multi-party derivatives and is conducive to automated execution. We propose an architecture for separating contractual terms from contract execution. A contract engine encapsulates the syntax and semantics of financial contracts without actively performing contractual actions; such actions are handled by user-definable contract managers that administer strategies for the execution of contracts. Hosting contracts and contract managers on a distributed ledger, side-by-side with digital assets, facilitates automated settlement of commitments without the need for an intermediary. We discuss how the proposed technology may change the way financial institutions, regulators, and individuals interact in a financial system based on distributed ledgers.
13:45-15:15 Streaming and Life-Insurance on GPUs
Streaming data-parallelism (Andrzej Filinski, DIKU)
TBA.
Stream fusion: from staging to ahead-of-time compilation through Scala Native (Aggelos Biboudis, École Polytechnique Fédérale de Lausanne)
Stream processing is mainstream (again): Widely-used stream libraries are now available for virtually all modern OO and functional languages, from Java to C# to Scala to OCaml to Haskell. Yet expressivity and performance are still lacking. In this talk we present two topics. Firstly, we present the strymonas library, the first approach that represents the full generality of stream processing and eliminates overheads, via the use of staging. It is based on an unusually rich semantic model of stream interaction. We support any combination of zipping, nesting (or flat-mapping), sub-ranging, filtering, mapping-of finite or infinite streams. Secondly, gaining inspiration from Futhark we present our vision for Scala Native enhanced with capabilities to offload computations to GPGPU supporting fusion and fission. Scala Native is the ahead-of-time compiler for Scala developed at EPFL and in this talk we will introduce a possible common ground for ideas to flow between the two worlds.
Domain-specific languages and GPGPUs in life insurance and pensions (Peter Sestoft, ITU)
The pension and life insurance industry works with a very long-term financial contracts where payments depend on the life state of the insured individual(s). We present a domain-specific language called the Actulus Modelling Language for Products (AML-P) for describing the payment streams of life insurance and pension contracts, and the envisioned uses of this language, including the computation of net present value, future cashflows and so on. The latter quantities can be estimated by numerical solution of (Thiele) differential equations, and we highlight the computational flexibility obtained by using a domain-specific language to separate specification and implementations. This reflects work done in the Actulus project 2011-2016, a collaboration between Edlund A/S, Copenhagen University and the IT University of Copenhagen. We also sketch some ideas for further development.
15:45-17:15 Data-parallel Programming
Design and implementation of the Futhark programming language (Troels Henriksen, DIKU)
Futhark is a data-parallel programming language under development at HIPERFIT. The language supports nested data-parallelism and features an optimising compiler under rabit development. This presentation gives a status update on recent Futhark development, with a particular focus on generation of efficient OpenCL GPU kernels and the steps automatically taken by the Futhark compiler to ensure fusion and efficient memory accesses. In the presentation, we will discuss various tradeoffs of the code generation, and how a new versioning technique can defer to runtime the decision between different parallelisation strategies.
Futhark: Challenges and Future Research Directions (Cosmin Oancea, DIKU)
The study of programming-model technology that can effectively utilize modern hardware is an open, hard, and fundamental topic of research. The previous talk has introduced such a data-parallel language – in summary, Futhark has already brought a number of research contributions and has already demonstrated its potential for efficiently utilizing heterogeneous GPGPU hardware on a number of applications, but one could remark that so far, Futhark’s design has followed a rather conventional path. We believe that currently, Futhark merely provides a solid foundation for studying and experimenting with novel and aggressive techniques in the language and compiler-construction fields.
This talk outlines several such research opportunities: First, we use the motivating example of trinomial pricing to show how locality of reference can be optimised by using inspector-executor techniques coupled with a more aggressive flattening of nested parallelism. Second, we demonstrate how the large-memory footprint and the significant copying overhead inherent to purely-functional approaches can be optimised by combining ideas from region-based memory management and register allocation (the later is lifted to operate on arrays rather than scalars). Finally, we discuss language extensions for (automatically) supporting module systems, automatic differentiation, and relational algebra.
APL on GPUs–a progress report with a touch of machine learning (Martin Elsman, DIKU)
We give a status report of the APL->TAIL->Futhark compiler, which compiles a subset of APL into code executable on GPUs. The compiler handles quite a number of APL functions and operators and is, for the subset of APL it supports, highly compatible with code written for Dyalog APL. Besides reporting on the performance of a number of APL benchmarks, we demonstrate, by example, how the APL compiler tool chain can be used to teach efficiently a neural network to recognise handwritten digits.