FPWeeklyMeeting

The FP talks are now reachable from the new (2023) FP Group homepage.

Old page below

Want to give a Functional Programming related talk? Talk to Anton Ekblad (antonek at chalmers dot se) to book a slot. We usually have a talk every Friday at 10:00.

Google Calendar Links

Planned talks

None

Past Meetings

2019-11-29, 10:00, EDIT 8103

Speaker: Koen Claessen, Chalmers University of Technology
Title: Building and Testing a Synthesizer from LTL properties
Abstract: I am in the process of building a "synthesizer", which is a tool that, given a specification of a system as Linear Temporal Logic (LTL) properties, can automatically compute a state machine that satisfies all those LTL properties. In the spirit of "more talks about ongoing work" I will present how far I've come and the problems I am facing right now.
In particular, I need to have an effective way of testing some of the components of the tool I am building. One of these components translates from LTL to an automaton, is very hard to get efficient and right, obviously needs to be correct, and is very hard to test! LTL semantics deals with infinite traces which are hard to deal with in the context of executable properties.
The talk assumes no working knowledge of LTL in members of the audience. Everything will be explained :)

2019-09-13, 10:00, EDIT Analysen

Speaker: Abraham Wolk, University of Copenhagen
Title: Towards a physically realistic universal model of parallel computation
Abstract: Physical laws and the geometry of 3-dimensional Euclidean space put limitations on (1) the speed of information transmission and (2) the scalability of network topologies. Prevailing models of parallel computation do either not take these limitations into account, or they relegate them to free parameters of the model that may be instantiated according to the application at hand. While the latter option may yield useful insights when analyzing an algorithm intended to be run on a /particular/ machine for which the parameters may be approximated, it does not yield insight into the scalability of an algorithm beyond the particular machine in a physically realistic way.
In this talk I will present ideas towards the development of a model of parallel computation in which computation is conceived of as a program executing on top of an underlying parallel universal machine that can plausibly be realized physically. The hope is that by measuring the resource consumption (both time and hardware resources) of the underlying universal machine, one obtains a realistic prediction of the actual resources required to execute an algorithm, as well as an understanding of how the resource consumption scales in a physically realistic manner.

2019-09-6, 10:00, EDIT Analysen

Speaker: Moa Johansson, Chalmers
Title: Learning and automated reasoning – informal thoughts and new ideas
Abstract: This talk will be very informal, and my aim is to see if I can find someone else who is interested in discussing and working on an interesting problem – how to combine learning and reasoning in theorem proving.
No one has missed the rapid development and popularity of machine learning (deep learning in particular) in many areas, including Natural Language Processing. What successful machine learning systems manage to do well is to in some sense capture some aspect of human intuition – even though not always perfect. E.g. a Google translate translation is often understandable, but perhaps not perfect.
Naturally, there is also growing intrested in machine learning in the automated reasoning community, in particular in finding out if machine learning can contribute towards tasks needing human intuition and interaction (such as choosing the next tactic to advance a proof in an interactive theorem prover) or tasks which are now guided by heuristics (such as selecting clauses, strategies etc. in an automated prover).
One specific question which I’ve been thinking about is how to best represent theorem proving concepts (e.g. functions, constants, datatypes, conjectures, subgoals etc) in order to make them amenable for machine learning models – which wants vectors or matricies of numerical values as inputs. In the literature, the techniques used are either hand-crafted features (based on heurisitics) or techniques from NLP, treating the symbols as more or less words in natural language. However, there are fundamental differences between “words” in theorem proving languages (functions, constants, types etc) and NL words. The former does have a formal semantics – which should be exploited! Furthermore, in theorem provers, users add new “words” routinely e.g. whenever they define a new function This happens less often in natural languages. This has largely been ignored by the learning theorem proving community but is a problem. So, how do we create a representation which is cheap add new “words” to?
Popular methods from NLP such as word2vec, which are trained to learn a vector representation can be expensive to train and need lots of data, so there is a question about how suitable they are if we often need to update the learned vector representation. Are there existing methods?

2019-08-30, 10:00, EDIT Analysen

Speaker: Hendrik van Antwerpen, Delft University
Title: Spoofax Language Workbench
Abstract: Meta-languages exist to improve the development of (domain specific) programming languages. Language engineers define aspects of the language by writing a high-level, declarative specification. A language implementations is derived from the specification. In this talk I will talk about (a) Statix, a meta-language for name binding and typing rules, and (b) ongoing work on generating random program terms from Statix specifications.
Immediately after the talk is a small workshop to play with Spoofax, the language workbench that contains, among other things, an implementation of Statix. We will do some interactive language development and play with some of the meta-languages of Spoofax by extending an existing language definition for STLC-with-Records with new syntactic constructs and typing rules. It is best to install Spoofax and get the workspace I prepared for this workshop beforehand, so we can focus on some hacking. See for instructions: https://hendrik.van-antwerpen.net/talks/20190830-chalmers/

2019-08-16, 10:00, EDIT Analysen

We are going to fire up our Functional Programming talks again and this Friday we start with a bang! We are going to have no less than four FP talks, which are dry run ICFP presentations. We have come up with the following program:

10:00 - 10:30 Simple Noninterference from Parametricity, Maximilian Algehed
10:30 - 11:00 Hailstorm : A static typed functional languages for systems, Abhiroop Sarkar
11:00 - 11:30 Coffee break
11:30 - 12:00 Scoping Monadic Relational Database Queries, Anton Ekblad
12:00 - 12:30 TBA, Markus Aronsson

The presentations are going to take place in EDIT Analysen. You can find some abstracts below. All welcome!

Simple Noninterference from Parametricity, Maximilian Algehed

In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of Abadi et al. in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructionsand the encoding of data abstraction using existential types.This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.

—

Hailstorm : A static typed functional languages for systems, Abhiroop Sarkar

This talk provides an introduction to a work in progress functional language implementation which is designed primarily for programming embedded systems.

—

Scoping Monadic Relational Database Queries, Anton Ekblad

We present a novel method for ensuring that relational database queries in monadic embedded languages are well-scoped, even in the presence of arbitrarily nested joins and aggregates. Demonstrating our method, we present a simplified version of Selda, a monadic relational database query language embedded in Haskell, with full support for nested inner queries. To our knowledge, Selda is the first relational database query language to support fully general inner queries using a monadic interface. In the Haskell community, monads are the de facto standard interface to a wide range of libraries and EDSLs. They are well understood by researchers and practitioners alike, and they enjoy first class support by the standard libraries. Due to the difficulty of ensuring that inner queries are well-scoped, database interfaces in Haskell have previously either been forced to forego the benefits of monadic interfaces, or have had to do without the generality afforded by inner queries.

2019-05-03, 10:00, EDIT Analysen

Speaker: Troels Henriksen, DIKU
Title: Compiler transformations for a GPU-targeting purely functional array language
Abstract: Futhark is a small programming language designed to be compiled to efficient parallel code. It is a statically typed, data-parallel, and purely functional array language, and comes with a optimising ahead-of-time compiler that generates GPU code via OpenCL and CUDA. Futhark is not designed for graphics programming, but instead uses the compute power of the GPU to accelerate data-parallel array computations (“GPGPU”).
This talk presents the design of the Futhark language, as well as outlines several of the key compiler optimisations that have enabled performance comparable to hand-written GPU code. Through the use of a functional source language, we obtain strong invariants that simplify and empower the application of traditional compiler optimisation techniques. In particular, I will discuss (i) handling of high-level features like modules, polymorphism, and higher-order functions, (ii) loop interchange and distribution to extract flat parallel kernels from nested parallel source programs, (iii) multi-versioned code generation that exploits as much parallelism as necessary and efficiently sequentialises the rest, and (iv) data layout transformations to ensure coalesced memory access on GPUs.

2019-04-12, 10:00, EDIT 8103

Speaker: Herbert Lange, Chalmers
Title: Restricting grammars to reduce ambiguity
Abstract: Formal grammars are useful tools to describe languages both in computer science and computational linguistics. To describe natural languages large-scale grammars are necessary, e.g. the Grammatical Framework Resource Grammar Library. But with increasing size and complexity of a grammar, more and more ambiguity in the analyses arises, which is undesirable for specific applications.
In this talk I will look at restricting a formal grammar in a way that it describes exactly a language-specific fragment of the original language and this fragment can be given in the form of a set of examples. The resulting grammars will be specifically optimised to avoid ambiguous analyses. The focus of the talk will be on natural language applications but the methods I will present are generic and can be of general interest.

2019-01-18, 10:00, EDIT Analysen

Speaker: Joel Svensson, RISE
Title: A Lisp-like interpreter on ZYNQ ARM+FPGA
Abstract: This talk, more of a demonstration perhaps, is about a just-for-fun hobby project that I work on as an educational exercise for myself. I am working on an interpreter for a lisp-like language that I intend to run on a ZYNQ ARM+FPGA (on the ARM core). Apart from learning about implementation of lisp-like languages I hope to gain the benefit of having a bare-metal REPL to assist me when I play with my development board. This is work-in-progress so tips and ideas are greatly appreciated.

2018-10-26, 10:00, EDIT EA

Speaker: Josef Svenningsson, Ericsson
Title: A Gradual Type System for Erlang
Abstract: This talk introduces a new type system for Erlang based on Gradual Typing. The principles of Gradual Typing has emerged in the type system research community over the last decade and has resulted in several new type system for existing languages. Gradual Typing is tailored to mix static and dynamic code. The type system provides pay-as-you-go static checking: the more type annotation in the program, the more static checking will be performed.
The tool we've developed uses Erlang's current syntax for specs, and it works on existing code bases without change. I will go through the design principles used when developing our new gradual type system for Erlang. No prior knowledge of gradual typing will be assumed.
Dialyzer is currently the most popular tool for the static checking of Erlang. Our gradual type system turns out to be somewhat complementary to Dialyzer. While Dialyzer aims to give no false positives, our type system always reports an error whenever a type spec doesn't match the code. We'll provide an in-depth comparison of the two tools.
This talk is an extended version of a presentation given at Code Beam this year.

2018-10-05, 10:00, EDIT Analysen

Speaker: John Hughes, Chalmers
Title: Testing Statistical Properties
Abstract: Randomised algorithms (such as QuickCheck itself!) require choices to be made with a given probability. Such algorithms are harder to test, because testing requires estimating probabilities in a statistically sound way. In this talk I’ll explore ways to include statistical properties in property-based tests, based on work that Nick Smallbone and I have done recently, with inspiration from a Quviq customer.
Slides: hughes_statistical_properties.pdf

2018-09-28, 10:00, EDIT 8103

Speaker: Maximilian Algehed, Chalmers
Title: A Perspective on the Dependency Core Calculus
Abstract: I will presents a simple but equally expressive variant on the terminating fragment of the Dependency Core Calculus (DCC) of Abadi et al. [1]. DCC is a concise and elegant calculus for tracking dependency. The calculus has applications in, among other areas, information flow control, slicing, and binding time analysis. However, in this paper we show that it is possible to replace a core technical device in DCC with an alternative, simpler, formulation. The calculus has a denotational semantics in the same domain as DCC, using which we prove that the two calculi are equivalent. As a proof of concept to show that our calculus provides a simple analysis of dependency we implement it in Haskell, obtaining a simpler implementation compared to previous work [2].
This will be a dry-run of a talk I will be giving at the PLAS workshop co-located with CCS.
[1] A Core Calculus of Dependency - Abadi et al. [2] Embedding DCC in Haskell - Algehed and Russo

2018-09-21, 10:00, EDIT Analysen

Speaker: Nachiappan Valliappan, Chalmers
Title: Typing the Wild in Erlang, Hindley-Milner style
Abstract: Developing a static type system suitable for Erlang has been of ongoing interest for almost two decades now. The challenge with retrofitting a static type system onto a dynamically typed language, such as Erlang, is the loss of flexibility in programming offered by the language. In light of this, many attempts to type Erlang trade sound type checking for the ability to retain flexibility. In this talk, I'll present an implementation of a Hindley-Milner type system for Erlang which strives to remain sound without being too restrictive. Our type checker—unlike contemporary implementations of Hindley-Milner—is flexible enough to allow overloading of data constructors, branches of different types etc. Further, to allow Erlang’s dynamic type behaviour, we employ a program specialization technique called partial evaluation. Partial evaluation simplifies programs prior to type checking, and hence enables the type system to type such behaviour under certain restricted circumstances.
Note: This talk is a dry-run of my presentation at the upcoming Erlang Workshop, based on my master thesis work at Chalmers supervised by John Hughes.
Link to paper: http://nachivpn.me/ew18.pdf

2018-09-14, 11:00, EDIT Analysen

Speaker: Agustín Mista, Chalmers
Title: Branching Processes for QuickCheck Generators
Abstract: In QuickCheck (or, more generally, random testing), it is challenging to control random data generators' distributions---specially when it comes to user-defined algebraic data types (ADT). In this paper, we adapt results from an area of mathematics known as branching processes, and show how they help to analytically predict (at compile-time) the expected number of generated constructors, even in the presence of mutually recursive or composite ADTs. Using our probabilistic formulas, we design heuristics capable of automatically adjusting probabilities in order to synthesize generators which distributions are aligned with users' demands. We provide a Haskell implementation of our mechanism in a tool called DRaGen and perform case studies with real-world applications. When generating random values, our synthesized QuickCheck generators show improvements in code coverage when compared with those automatically derived by state-of-the-art tools.
Link: https://arxiv.org/abs/1808.01520

2018-09-12, 13:15, EDIT 8103

Speaker: Andrey Mokhov, Newcastle University
Title: Algebraic Graphs
Abstract: Are you tired of fiddling with sets of vertices and edges when working with graphs? Would you like to have a simple algebraic data type for representing graphs and manipulating them using familiar functional programming abstractions? In this talk, we will learn a new way of thinking about graphs and a new approach to working with graphs in a functional programming language like Haskell. The ideas presented in the talk are implemented in the Alga library: https://github.com/snowleopard/alga. I hope that after the talk you will be able to implement a new algebraic graph library in your favourite programming language in an hour.

2018-09-07, 10:00, EDIT Analysen

Speaker: Sólrún Halla Einarsdóttir, Chalmers
Title: Into the Infinite - Theory Exploration for Coinduction
Abstract: Theory exploration is a technique for automating the discovery of lemmas in formalizations of mathematical theories, using testing and automated proof techniques. Automated theory exploration has previously been successfully applied to discover lemmas for inductive theories, about recursive datatypes and functions. We present an extension of theory exploration to coinductive theories, allowing us to explore the dual notions of corecursive datatypes and functions. This required development of new methods for testing infinite values, and for proof automation. Our work has been implemented in the Hipster system, a theory exploration tool for the proof assistant Isabelle/HOL.
This talk is a dry-run for my upcoming talk at AISC 2018, based on joint work with Moa Johansson and Johannes Åman Pohjola.
Link to paper: http://www.cse.chalmers.se/~slrn/papers/into_infinite.pdf

2018-06-08, 10:00, EDIT EA

Speaker: Maximilian Algehed, Chalmers
Title: Parametricity and Noninterference revisited
Abstract: I will talk about a few new proofs of noninterference for variants of System F_\omega which make use of parametricity for dependent types. Unlike previous results I obtain parametricity-based proofs of noninterference for both static and dynamic enforcement of noninterference. The proofs make use of a parametricity formulation for PTS:s by Bernardy et al [1].. In their theory, a term in a PTS O gets translated into a term in another PTS M, O and M for Object and Meta, where the M terms represent theorems and proofs derived from the type and implementation of the terms in O. Our proofs make essential use of this separation of two systems to hide parts of secure data-types from the programmer. In our formulation, the M language constitutes both meta-language and trusted computing base.

[1] Proofs for Free, J.P. Bernardy, P. Jansson, R. Patterson, JFP 2012

2018-06-01, 10:00, EDIT 3364

Speaker: Edvard Hübinette and Fredrik Thune, Chalmers
Title: Better Implicit Parallelism (MSc Thesis presentation)
Abstract: ApplicativeDo tries to remove the Monad binds where possible when desugaring Haskells' do-notation. It does this by looking at inter-statement dependencies and using the Applicative operator when it can; this introduces implicit parallelism in the code. Deciding which structure to generate is tricky, since many different are usually possible. Currently, this is solved with simple minimum cost analysis with an unit cost model, assuming each statement takes the same amount of time to evaluate.
At Facebook, Marlow et. al developed [Haxl](https://github.com/facebook/haxl), a data-fetching library that can use applicative expressions for free parallelism. To our knowledge, it is the only library that does automatic parallelism on Applicative expressions.
By extending the cost model inside the ApplicativeDo algorithm for variable evaluation costs, and implementing weight annotations through optional programmer pragmas in GHC, we do smarter generation of code by prioritising parallelisation of heavy statements. This leads to quite nice speedups when using Haxl, with very little extra work for the programmer.
ApplicativeDo was introduced with Desugaring Haskells' do-notation Into Applicative Operations (Marlow, Peyton-Jones, Kmett, & Mokhov, Haskell Symposium 2016) Haxl was introduced with There Is No Fork (Marlow, Brandy, Coens, & Purdy, ICFP 2014)

2018-05-25, 10:00, EDIT EA

Speaker: Matthías Páll Gissurarson, Chalmers
Title: Suggesting Valid Hole Fits for Typed-Holes (Master Thesis defence)
Abstract: Most programs are developed from some sort of specification, and type systems allow programmers to communicate part of this specification to the compiler via the types. The types can then be used to verify that the implementation matches this partial specification. But can the types be used to aid programmers during development, beyond verification? In this talk I will defend my master's thesis, titled "Suggesting Valid Hole Fits for Typed-Holes" and present a lightweight, practical extension to the typed-holes of GHC that improves user experience and facilitates a style of programming called "Type-Driven Development".

2018-05-18, 10:00, EDIT 3364

Speaker: Süleyman Savas, Högskolan i Halmstad
Title: Designing Domain-Specific Heterogeneous Architectures from Dataflow Programs
Abstract: The last ten years have seen performance and power requirements pushing computer architectures using only a single core towards so-called manycore systems with hundreds of cores on a single chip. To further increase performance and energy efficiency, we are now seeing the development of heterogeneous architectures with specialized and accelerated cores. However, designing these heterogeneous systems is a challenging task due to their inherent complexity. We propose an approach for designing domain-specific heterogeneous architectures based on instruction augmentation through the integration of hardware accelerators into simple cores. These hardware accelerators are determined based on their common use among applications within a certain domain. The objective is to generate heterogeneous architectures by integrating many of these accelerated cores and connecting them with a network-on-chip. The proposed approach aims to ease the design of heterogeneous manycore architectures—and, consequently, exploration of the design space—by automating the design steps. To evaluate our approach, we enhanced our software tool chain with a tool that can generate accelerated cores from dataflow programs. This new tool chain was evaluated with the aid of two use cases: radar signal processing and mobile baseband processing. We could achieve an approximately 4x improvement in performance, while executing complete applications on the augmented cores with a small impact (2.5–13%) on area usage. The generated accelerators are competitive, achieving more than 90% of the performance of hand-written implementations.
In this talk I will give an overview of our design method for developing heterogeneous architectures with custom extensions generated automatically by our tool chain. The tool chain takes dataflow applications as input and generates custom hardware in a functional programming language which then can be translated to verilog.
Slides: savas.pdf

2018-04-20, 10:00, EDIT 3364

Speaker: Troels Henriksen, DIKU, Copenhagen University
Title: Design and implementation of the Futhark programming language
Abstract: Futhark is a data-parallel programming language under development at DIKU. The language supports (regular) nested data-parallelism and features an optimising compiler under rapid development. This presentation gives an introduction to Futhark and its compiler, 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, I will discuss various tradeoffs of the code generation, and how a new versioning technique can defer to runtime the decision between different parallelisation strategies.

2018-03-09, 10:00, EDIT 3364

Speaker: Solène Mirliaz and Elisabet Lobo, Chalmers
Title: Interpreting Lambda Calculus via Category Theory (A pragmatic programming guide for the non-expert)
Abstract: Many domain-specific languages are often implemented in a deep embedded fashion in order to enable optimizations. Many of the techniques for EDSL soon or later end up repeating the work of the host compilar---for this pearl, that would be GHC. Recently, a new approach called Compiling to Categories has emerged and promises to avoid such replication of work. It relies on understanding the categorical model of Cartesian Closed Category (CCC). That means that, to use this new technique, it becomes necessary to understand basic category theory and CCC. Unfortunately, when learning about such topics and its relation to functional programs, one faces the risk of diving into mathematical books with difficult-to-penetrate notation, getting lost into abstract notions, and eventually giving up. Instead, this pearl aims to guide Haskell developers to the understanding of all of such abstract concepts via Haskell code. We present two EDSLs in Haskell: one for simple-typed lambda terms and another for CCC and show how to translate programs form one into the other---a well-known result by Lambek in 1985. To achieve the translation, our implementation relies on GHC closed type families. By going into CCC, it becomes possible to give many interpretations to lambda terms, but in this work we only focus on a traditional call-by-value semantics. Hence, we also show how to execute CCC programs via the categorical abstract machine (CAM). Moreover, we extend our implementation of simple-typed lambda calculus with primitive operators, branching, and fix points via appropriated enhancements to CCC and CAM based on category theory concepts. All this journey is going to be grounded in Haskell code, so that developers can experiment and stop fearing such abstract concepts as we did.
This talk is based on a joint-work with Alejandro Russo.

2018-03-02, 10:00, EDIT 8103

Speaker: Dominic Orchard, University of Kent
Title: Programs that explain their effects (in Haskell)
Abstract: The traditional approach to writing effectful programs in Haskell is to use monads and the 'do' notation. In the talk, I will show two richer structures for capturing effects: parameterised monads and graded monads. Both provide a way to capture more information about the side effects of a program in the program's types, which can be used for detecting effect-related bugs. These structures can be programmed with directly in GHC/Haskell due to an extension which allows the 'do' notation to be rebound to different structures other than a monad. There will also be concrete, real-world examples.
Slides: https://github.com/dorchard/effectful-explanations-talk

2017-12-15, 10:00, EDIT 3364

Speaker: Matthías Páll Gissurarson
Title: Suggesting Valid Substitutions For Typed Holes
Abstract: A common problem when working large software libraries is how to discover functions and constants within those libraries. Typed holes are a feature in Haskell, where programmers can specify “holes” in expressions and have the compiler relate information about those holes inferred from the context. Our contribution is an extension to the functionality of these holes where type directed search is used to suggest valid substitutions for those holes to the programmer. This extension has been accepted into GHC.

2017-12-08, 10:00, EDIT 3364

Speaker: Maximilian Algehed
Title: SessionCheck, Bidirectional Testing of Communicating Systems
Abstract: I will present a new tool called SessionCheck. This tool helps programmers write distributed applications that work correctly. SessionCheck is designed to help rid programmers of the tedium of maintaining more than one specification and test suite for multiple application components. SessionCheck does this by borrowing ideas from session types and domain specific languages in order to provide a simple yet expressive and compositional specification language for communication protocols. Specifications written in the SessionCheck specification language can be used to test both client and server implementations of the same protocol in a completely language-agnostic manner.

2017-12-01, 10:00, EDIT 3364

Speaker: Nicola Botta
Title: Responsibility, influence and sequential decision problems
Abstract: Attributing responsibility -- e.g. for units of greenhouse gas emissions -- in a consistent way is crucial for fair burden sharing and even compensation schemes but also for effective decision making: one would like to invest computational or human resources in decisions that truly matter. But how can we compute which decisions really do matter? We argue that a dependently typed formalization of optimal decision making under uncertainty is a good starting point for deriving measures of influence/responsibility.

2017-11-03, 10:00, EDIT 3364

Speaker: Aarne Ranta
Title: Explainable Machine Translation
Abstract: Explainable Artificial Intelligence (XAI) is an attempt to mitigate the black-box character of machine learning based AI techniques. A prime example of such techniques is Neural Machine Translation (NMT), which works via an end-to-end string transformation where the intermediate stages are machine-created vectors of floating point numbers. While NMT has reached average scores higher than older methods, its problem is that the resulting translations are sometimes completely wrong, and it is hard tell good translations from bad ones without knowing both the source and the target language.
Explainable Machine Translation (XMT) applies the XAI idea to the field of translation. It is inspired by Kurt Mehlhorn’s notion of certifying algorithms: algorithms that don’t just produce a result but a certificate - a piece of evidence that can be inspected by the user. The certificate that we propose is a formula in constructive type theory, which encodes the semantic and abstract syntactic structure of the translatable content. The formula is obtained by a parser, which itself may be a black box, but which has a formally defined relation to the source and target text. In our implementation of the idea, the parser is a neural dependency parser returning Universal Dependency (UD) trees. These trees are interpreted as type theoretical formulas, which form a translation interlingua. As the final step, the interlingua linearized into the target language by using the Grammatical Framework (GF). The last step is defined by formal rules and therefore easy to verify, whereas the parsing step - which involves interpretation of unrestricted human language - is a natural playground for machine learning approaches. By producing a formula as the outcome of this step, we can increase the reliability of the entire translation process.

2017-10-27, 10:00, EDIT 3364

Speaker: Emil Axelsson
Title: Rhino -- a DSL for data-centric applications
Abstract: n this talk I will present our development of Rhino at Mpowered Business Solutions. Rhino is a functional DSL/framework targeting data-centric applications such as compliance calculations, which involve managing potentially large amounts of data and presenting reports from calculations on this data. The goal is a fully declarative framework where the programmer can focus on the structure and logic of the application rather than details of how it is going to run. We envision several advantages of a declarative system: (1) rapid development; (2) easy to use for domain experts; (3) tractability to include third-party plug-ins (due to lack of side effects); etc.
Rhino is very much work in progress. The talk will focus on the pure functional calculation and query languages used in Rhino. I will also share some lessons learned from an early attempt to implement Rhino as an embedded DSL in Haskell.
Mpowered's core product is a toolkit for measuring compliance with South African legislation for diversity in companies. Rhino aims to improve the existing implementation by factoring out the business logic in order to get a more maintainable system and to allow calculations to be written by domain experts. With some luck, Rhino may even be useful to other businesses in the same domain.

2017-10-06, 10:00, EDIT 3364

Speaker

Jean-Philippe Bernardy

Title

TypedFlow: the HOT parts

Abstract

TensorFlow™ is an open source software library for numerical computation using data flow graphs. Nodes in the graph represent mathematical operations, while the graph edges represent the multidimensional data arrays (tensors) communicated between them. TensorFlow graphs can be efficiently evaluated on GPUs and is a popular choice to implement deep learning applications.

TypedFlow is a higher-order and typed (HOT) frontend to tensorflow, written in (Glasgow) Haskell.

In this talk I will:

briefly explain what TensorFlow is and how it applies to deep learning
recall the advantages of a HOT approach
expose some example programs written using TypedFlow
demonstrate how tensorflow functions can be given precise types, using GHC extensions
discuss some the difficulties of doing so

2017-09-15, 14:15, EDIT EB

Speaker: Erik Hertz
Title: Methodologies for Approximation of Unary Functions and Their Implementation in Hardware
Abstract: Applications in computer graphics, digital signal processing, communication systems, robotics, astrophysics, fluid physics and many other areas have evolved to become very computation intensive. Algorithms are becoming increasingly complex and require higher accuracy in the computations. In addition, software solutions for these applications are in many cases not sufficient in terms of performance. A hardware implementation is therefore needed. A recurring bottleneck in the algorithms is the performance of the approximations of unary functions, such as trigonometric functions, logarithms and the square root, as well as binary functions such as division. The challenge is therefore to develop a methodology for the implementation of approximations of unary functions in hardware that can cope with the growing requirements. The methodology is required to result in fast execution time, low complexity basic operations that are simple to implement in hardware, and – since many applications are battery powered – low power consumption. To ensure appropriate performance of the entire computation in which the approximation is a part, the characteristics and distribution of the approximation error are also things that must be possible to manage.
The new approximation methodologies presented are of the type that aims to reduce the sizes of the look-up tables by the use of auxiliary functions. They are founded on a synthesis of parabolic functions by multiplication – instead of addition, which is the most common.
For some functions, such as roots, inverse and inverse roots, a straightforward solution with an approximation is not manageable. Since these functions are frequent in many computation intensive algorithms, it is necessary to find very efficient implementations of these functions. New methods for this are also presented. They are all founded on working in a floating-point format, and, for the roots functions, a change of number base is also used. The transformations not only enable simpler solutions but also increased accuracy, since the approximation algorithm is performed on a mantissa of limited range.

2017-09-01, 10:00, EDIT 8103

Speaker: Anton Ekblad
Title: A Meta-EDSL for Distributed Web Applications
Abstract: We present a domain-specific language for constructing and configuring web applications distributed across any number of networked, heterogeneous systems. Our language is embedded in Haskell, provides a common framework for integrating components written in third-party EDSLs, and enables type-safe, access-controlled communication between nodes, as well as effortless sharing and movement of functionality between application components. We give an implementation of our language and demonstrate its applicability by using it to implement several important components of distributed web applications, including RDBMS integration, load balancing, and fine-grained sandboxing of untrusted third party code.
This is a dry run for my talk at Haskell Symposium '17, so please bring an extra helping of comments and opinions.

2017-08-25, 10:00, EDIT EF

Speaker: Markus Aronsson
Title: Hardware Software Co-Design in Haskell
Abstract: I'll present a library in Haskell for programming Field Programmable Gate Arrays (FPGAs), including hardware software co-design. Code for software (C) and hardware (VHDL) is generated from a single program. The library is however open in that our type-based techniques for embedding allows for the implementation of more than two embedded domain specific language (EDSL). Code is generation is implemented as a series of translations between progressively smaller, typed EDSLs, safeguarding against errors that arise in untyped translations.
If you're familiar with Feldspar, consider this a redesign that supports compilation to both VHDL and C.

2017-06-16, 10:00, EDIT 8103

Speaker: Anton Ekblad
Title: Scoping Monadic Relational Database Queries
Abstract: In this talk I present Selda, a monadic DSL for relational database queries embedded in Haskell, using the semantics of the list monad as a base. Selda improves upon the current state of the art in database DSLs by including joins and aggregation over fully general inner queries. To this end, I present a simple yet novel method to guarantee that inner queries are well-scoped.
In the Haskell community, monads are the de facto standard interface to a wide range of libraries and EDSLs. They are well understood by researchers and practitioners alike, and they enjoy first class support by the standard libraries. Due to the difficulty of ensuring that inner queries are well-scoped, database interfaces in Haskell have either been based on other, less familiar abstractions, or have had to do without the generality afforded by inner queries.
This talk is a dry run for TFP '17. Feedback on everything from slides to talk structure to the content itself is even more welcome than usual!

2017-06-09, 10:00, EDIT 8103

Speaker: Linnéa Andersson and Andreas Wahlström
Title: Evaluation of a new recursion induction principle
Abstract: Structural induction is a powerful tool for proving properties about functions with recursive structure, but it is useless when the functions do not preserve the structure of the input. Many of today's cutting-edge theorem provers use structural induction, which makes it impossible for them to prove properties about non-structurally recursive functions. We introduce a new induction principle, where the induction is done over a function application. This principle makes it possible to prove properties about non-structurally recursive functions.

2017-06-02, 10:00, EDIT 8103

Speaker: Regina Hebig
Title: Building DSLs with Modelling Techniques – What we teach and what our students make out of it
Abstract: We teach DSL development in the software engineering program as well as in the WASP program to master’s students and practitioners. In doing so, we focus on modelling techniques, such as metamodeling, Xtext, OCL, code generation, and model transformation. In the talk we will provide an overview about these techniques and discusses how far students are able to adopt and use them. For that, we will show examples of DSLs that were created during the courses.

2017-05-19, 10:00, EDIT EA

Speaker: Alejandro Russo
Title: Securing Lazy Programs
Abstract: Information-Flow Control libraries exists in the functional programming language Haskell as embedded domain-specific languages. One distinctive feature of Haskell is its lazy evaluation strategy. In 2013, Buiras and Russo show an attack on the LIO library where lazy evaluation is exploited to leak information via the internal timing covert channel. This covert channel manifests by the mere presence of concurrency and shared resources. LIO removes leaks via such covert channel only for public shared-resources which can be invoked by the library, e.g., references. With lazy evaluation in place, variables introduced by let-bindings and function application---which cannot be controlled by LIO---become shared resources and forcing their evaluation corresponds to affecting threads’ timing behavior. A naïve way to avoid such leaks is by simply forcing the evaluation of variables which might be shared among threads. Unfortunately, this solution goes against one of the core purpose of lazy evaluation: avoid evaluation of unneeded expressions! More importantly, it is not always possible to evaluate expressions to their denoted value---some of them could denote infinite structures. Instead, this work presents a novel approach to explicitly control, at the programming language level, the sharing introduced by lazy evaluation. We design a new primitive called lazyDup which lazily duplicates unevaluated expressions as well as any sub-expression which they might depend on. We provide a formalization of the security MAC library and lazyDup in the form of a concurrent call-by-need calculus with sharing and mutable references. We support our formal results with mechanized proofs in Agda. Although we focus on MAC, our results are also applicable to other IFC libraries like LIO and HLIO.
This talk is based on a joint work with Marco Vassena and Joachim Breitner (it would be presented in the IEEE Computer Security Symposium in August).

2017-05-12, 10:00, EDIT 8103

Speaker: Peter Thanisch and Jyrki Nummenmaa
Title: How can we enhance type safety for data expressions?
Abstract: Information systems, such as database systems, statistics packages, and spreadsheet programs, allow the user to extract aggregated data, specified by expressions containing statistical functions, typically in a declarative language and typically with little more type information than can be gleaned from primitive type declarations. Often, subject-matter experts are aware of additional relevant type information, but this information is ignored by the information system. Consequently, “type-safe” expressions can produce nonsensical answers, which could have been avoided, had type-checking utilized that additional type information. We have identified a small set of metadata items, along with type inference rules, that can be used to provide an enhanced notion of type safety. This allows us to perform static checking on data expressions in order to identify potential type-safety issues in advance of the expression being evaluated against the data. To illustrate our approach, we have implemented rule-based software that performs this enhanced type-checking on SQL queries that contain complex arithmetic expressions, including statistical aggregation functions.
What we have NOT done is to develop a more general-purpose solution where this kind of type inference is incorporated into a suitable functional programming language.

2017-05-05, 10:00, EDIT 8103

Speaker: Johan Jeuring
Title: An extensible strategy language for describing cognitive skills
Abstract: Students learn cognitive skills for solving problems in many domains. During the last decade, we have developed a strategy language: a domain-specific language for expressing cognitive skills and problem solving procedures. A strategy for a cognitive skill can be used to give feedback, hints, and worked-out solutions to a student interacting in a learning environment, an intelligent tutoring system, or a serious game. We frequently extend the strategy language to capture new patterns that occur when describing strategies. Examples of such extensions include a preference combinator, to express that one strategy is preferred above another strategy, and a combinator for describing that any initial part of a strategy is also accepted.
In this talk I will discuss the fundamental requirements for our strategy language, and show how we can extend the strategy language while preserving these requirements. We present a precise, trace-based semantics for a minimal strategy language. With this semantics, we study the algebraic properties of the strategy language. We describe several language extensions, specify new combinators and their algebraic properties, and discuss the implication of their introduction for the strategy language and its requirements. The language extensions are illustrated by giving actual examples from learning environments, intelligent tutoring systems, and serious games.
Slides: ExtensibleStrategy.pdf

2017-04-28, 10:00, EDIT 8103

Speaker: Sven-Bodo Scholz, Heriot-Watt University
Title: A Lambda-Calculus for Transfinite Arrays - Towards Unifying Streams and Arrays
Abstract: Arrays and streams seem to be fundamentally at odds: arrays require their size to be known in advance, streams are dynamically growing; arrays offer direct access to all of their elements, streams provide direct access to the front elements only; the list goes on. Despite these differences, many computational problems at some point require shifting from one paradigm to the other. The driving forces for such a shift can be manifold. Typically, it is a shift in the task requirements at hand or it is motivated by efficiency considerations. In this talk, we present a basis for a unified framework for dealing with arrays and streams alike. We introduce an applied lambda calculus whose fundamental data structure is a new form of array, named "Transfinite Array". Transfinite arrays maintain properties from finite array calculi yet incorporate support for infinite arrays. As it turns out, it is even possible to maintain recursive specifications as they are typically found in a traditional stream / list-based setting.

2017-04-21, 10:00, EDIT EF

Speaker: Maximilian Algehed
Title: A fresh look at Dependency Core Calculus
Abstract: Dependency Core Calculus (DCC) is a calculus for statically tracking dependency in functional programs that has been around for many years. DCC is useful for studying multiple program analyses such as call tracking, binding time analysis, slicing, and information flow control.
In this talk, I will present a new implementation of DCC in Haskell with a focus on applying information-flow control. The talk will present three novel main contributions that result from this implementation, i.e., (i) the implementation itself, (ii) how to safely add monad transformer into DCC to model effects, and (iii) a new, alternative, formulation of DCC that generalises some of the ideas from the original paper.
This talk is based on a joint work-in-progress with Alejandro Russo.

2017-04-07, 10:00, EDIT 8103

Speaker: Jurriaan Hage
Title: Customized Type Error Message in GHC
Abstract: The focus of this final presentation during my sabbatical at Chalmers will be showing what we have accomplished in the context of the Glasgow Haskell Compiler for the customization of type errors. In this work we employ type level programming to implement our customizations taking advantage of a number of recent additions to the compiler. A distinct advantage of this approach is code and diagnosis all live inside Haskell, and we can employ all methods of abstraction provided to us by the language. This is very recent work, in fact the paper was written while I was visiting Chalmers.

2017-03-31, 10:00, EDIT 3364

Speaker: Alejandro Russo
Title: Building Secure Embedded Systems Using Language-based Techniques
Abstract: Low-level languages, such as C / C ++, are highly used in industry to develop embedded systems. How to program these systems Involve internal details of the computer such as the use of memory pointers and manual handling of dynamic memory. The history of software development shows us that among the most common and difficult to correct errors is the presence of dangling pointers, that is, pointers that refer to invalid memory locations or that are no longer in use. When embedded systems are also concurrent, there are also race conditions problems. Wouldn't be beneficial for programmers that the compiler can help them to avoid such problems? (thus building a more secure system).
Rust is a language recently developed by Mozilla to develop systems that require high performance and a small execution environment (runtime). Part of the Firefox browser is already implemented in this language. Rust uses principles of programming languages and implements a type-system capable to detect the possibility of entering invalid pointers and handles allocation of memory automatically without a garbage collector. In this talk, I will talk about the principles and philosophy behind Rust and how these could be used to build secure systems.

2017-03-17, 10:00, EDIT 3364

Speaker: Alejandro Russo
Title: Choose your own adventure: Multi-Faceted Value Semantics, Secure Multi-Execution and many other possible endings
Abstract: There exist many programming languages techniques to certify that sensitive information is not leaked when manipulated by untrusted code. They range from static enforcements (like type-systems) to dynamic ones (as execution monitors). Despite when possible leaks are detected, such techniques raise false alarms---an aspect that is endemic to almost any enforcement. Secure Multi-Execution (SME) is a technique which allows to reduce the number of false alarms practically to zero! The price to pay is executing programs many times, one for each security level (e.g., public, secret, top secret, etc). In the presence of many security levels, SME might be nonviable. As an alternative, researchers propose the technique of Multi-Faceted Value semantics (MF), where each piece of data has as many "views" (values) as security levels. MF runs instructions once as much as possible, while simultaneously computing on different views. The exception to this rule are branches: MF repeats the execution of branches if the branch to be taken (i.e., then- or else-branch) depends on the view being considered. Although MF has been referred to as "an optimization of SME", researchers have recently shown that they provide different security guarantees. There is still no final judgment about which method is better (in terms of reducing false alarms) or more performing (less multi-executions) if both methods are to offer the same security guarantees.
Inspired by the comparison of SME and MF, we will present a calculus which, depending how it gets interpreted, it runs programs under SME, MF, or a combination of both! Importantly, the type signature of all the interpreters is the same---something that gives us hope that these two approaches could be unified. We have implemented our ideas as a EDSL in Haskell, where the code (and types) help us to discover a common root between both approaches. This talk will also show some venturous ideas where we got stuck---we hope that the FP crowd could provide us with some enlightenment on how to proceed forward.
This talk is based on a work-in-progress with Thomas Schmitz, Cormac Flanagan, Nataliia Beilova, and Tamara Rezk.

2017-03-10, 10:00, EDIT 8103

Speaker: Jurriaan Hage
Title: Domain-Specific Type Error Diagnosis in Haskell
Abstract: A challenge in type error diagnosis for general purpose languages suitable for embedding domain-specific languages is to have errors explained in terms of the domain, not the underlying encoding into the host language. In this talk I discuss work we have done in the Helium compiler back in previous decade and discuss recent results for Haskell beyond Haskell 98.

2017-03-03, 10:00, EDIT 8103

Speaker: João Pizani
Title: Hardware circuit description and verification in Agda
Abstract: There is a tradition of DSLs for hardware modelling inspired by functional programming (with a considerable effort originating in Chalmers). In our work, we build upon this tradition, using dependent types to ensure that circuits have some well-formedness conditions satisfied by construction. The dependently-typed host of our DSLs also allows proofs of circuit behaviour to be written in the same language (and checked by the same compiler) as the circuit model itself.
In this talk we present two Agda EDSLs for circuit description, one (Pi-Ware) with a low-level, architectural view of circuits, and another (Lambda1) with syntax and types more closely resembling the familiar λ-calculus. We comment on what restrictions are imposed upon these languages to ensure that they only contain terms with a "reasonably direct" mapping to hardware, and give some examples of how to model and verify circuits in each.

2017-02-24, 10:00, EDIT 8103

Speaker: Ralf Lämmel
Title: The Haskell Road to Software Language Engineering and Metaprogramming
Abstract: In this talk, I would like to sketch my upcoming textbook on software languages http://www.softlang.org/book while putting on the hat of a Haskell programmer. Overall, the book addresses many issues of software language engineering and metaprogramming: internal and external DSLs, object-program representation, parsing, template processing, pretty printing, interpretation, compilation, type checking, software analysis, software transformation, rewriting, attribute grammars, partial evaluation, program generation, abstraction interpretation, concrete object syntax, and a few more. Haskell plays a major role in the book in that Haskell is used for the implementation for all kinds of language processors, even though some other programming languages (Python, Java, and Prolog) and domain-specific languages (e.g., for syntax definition) are leveraged as well. I hope the talk will be interactive and help me to finish the material and possibly give the audience some ideas about FP- and software language-related education and knowledge management.
Slides: http://softlang.uni-koblenz.de/book/slides/HsSleMp.pdf

2017-02-17, 10:00, EDIT 8103

Speaker: Carl Seger
Title: From Abstract Specification to Detailed Implementation: How to Get Accelerator Based Code Right
Abstract: In the last decade, the rapid growth in single-threaded performance of computers has drastically slowed down. One approach to speed up a single threaded application is to use custom hardware for part of it. Unfortunately, fully custom hardware is extremely expensive to develop, becomes obsolete quickly, and is very inflexible. Field Programmable Gate Arrays (FPGAs) have emerged providing a good compromise between the generality of CPUs and the performance of custom hardware. As FPGAs have started to be more tightly integrated with CPUs, it has become feasible to achieve several orders of magnitude speedup on specific single threaded application and such accelerators are starting to be widely deployed. A very real challenge for these mixed software/hardware systems is how to ensure the correctness of the solution. Compounding this is the difficulty of debugging custom hardware (be it FPGA or ASIC based). In this talk I will discuss an approach, inspired by earlier work on effective hardware design, that I am pursuing during my visit here. More specifically I am advocating an integrated design and verification approach so that when a final implementation is reached, then so is a formal proof of its correctness. The talk is very much describing work in progress and I hope for many questions!
Slides: CarlSeger20170217.pdf

2017-02-10, 10:00, EDIT 8103

Speaker: Jurriaan Hage
Title: Type Error Diagnosis in Helium (part I: constraints and heuristics)
Abstract: This is an introductory talk on how we do type error diagnosis in the Helium Haskell compiler. We consider a constraint based formulation of the type system, and how that enables us to build type graphs and heuristics that can be defined on type graphs that look for causes of mistakes.
Slides: hagetedtalk.pdf

2017-02-03, 10:00, EDIT hörsal EE

Speaker: Carl Seger
Title: Formal Hardware Verification: Theory meets Practice
Abstract: Modern microprocessors contain several billion transistors and implement very complex algorithms. Ensuring that such designs are correct is a challenging and expensive task. Traditional simulation is rapidly becoming inadequate for this task and even multi-million dollar emulation hardware is rapidly losing the race against complexity. Formal hardware verification marries discrete mathematics and theoretical computer science concepts with effective heuristic to prove that some part of a chip implements exactly the function provided as a specification. In this talk I will briefly discuss the major building blocks used in formal hardware verification, discuss current industrial use of the technology and focus on the nuts-and-bolts involved in applying formal verification in industry.
Slides: FVinPractice.pdf

2017-01-27, 10:00, EDIT 8103

Speaker: Thorsten Berger
Title: Virtual Platform - Flexible and Truly Incremental Engineering of Highly Configurable Systems
Abstract: Customisation is a general trend. An ever-increasing diversity of hardware and many new application scenarios for software, such as cyber-physical systems, demand software systems that support variable stakeholder requirements. Two opposing approaches are commonly used to create variants: software clone&own and software configuration. Organizations often start with the former, which is cheap, flexible, and supports quick innovation, but leads to redundancies and does not scale. The latter scales by establishing an integrated platform that shares software assets between variants, but requires high up-front investments or risky migration processes. So, could we have a robust approach that allows an easy transition or even combines the benefits of both approaches?
In the talk, I will discuss the virtual platform a VR-funded project that aims at building a method and tool suite supporting a truly incremental development of variant-rich systems, exploiting a spectrum between both opposing approaches. I will present the main underlying idea, important concepts of variant-rich systems, and the project plan. I will also present some of my previous research in the area of variability modeling, model synthesis, and static program analysis that is relevant for the project.

2017-01-20, 11:00, EDIT 3364

Speaker: Maximilian Algehed
Title: SpecCheck: Monadic specification and property based testing of network protocol
Abstract: We present SpecCheck, a simple monadic specification language for property based testing of concurrent systems. We present an approach to specification making use of elementary results from session types which allows one specification to be used as a test oracle and a mockup for both client and server code. We also show how we can discover inconsistent SpecCheck specifications.
Slides: MaxSlides.pdf

2016-12-09, 13:00, EDIT 8103

Speaker: Patrik Jansson
Title: Sequential decision problems, dependent types and generic solutions,
Abstract: We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.
Slides: 20161209_140028.jpg
Paper: http://www.cse.chalmers.se/~patrikj/papers/CompTheoryPolicyAdviceAvoidability_JFP_2016-11_preprint.pdf

2016-12-02, 11:00, EDIT 3364

Speaker: Shayan Najd
Title: Trees That Grow
Abstract: I'll talk about my recent work with Simon Peyton Jones on extensible data types in Haskell. We study the notion of extensibility in functional data types, as a new approach to the problem of decorating abstract syntax trees with additional information. We observed the need for such extensibility while redesigning the data types representing Haskell abstract syntax inside Glasgow Haskell Compiler (GHC). Specifically, we describe a programming idiom that exploits type-level functions to allow a particular form of extensibility. The approach scales to support existentials and generalised algebraic data types, and we can use pattern synonyms to make it quite convenient in practice.
Slides: Attach:FPDec2016.pdf
Paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/trees-that-grow.pdf

2010-06-18, 15h15 - 16h15, EDIT room

Speaker: Karin Kejizer
Title: Raising Feldspar to a Higher Level
Abstract: Feldspar [1] is a domain specific language (DSL) for digital signal processing (DSP) initially designed with baseband telecommunication systems in mind. Feldspar is a strongly typed high level functional language which during compilation is translated to hardware specific C code via an intermediate core language. Because it is a high level functional language it raises the level of abstraction for programmers compared to the language C.
During my thesis, I focused on developing high-level combinators for DSP functions (like the finite impulse response filter) and designing and implementing a matrix module for writing algebraic descriptions of transforms (like the discrete Fourier transform) in Feldspar. During this presentation I will show my results.
[1] http://feldspar.inf.elte.hu/feldspar/

2010-06-14, 14h15 - 15h15, room ED

Speaker: Peter A. Jonsson, Luleå University of Technology
Title: Supercompilation and Call-By-Value
Abstract: Clear and concise programs written in functional programming languages often suffer from poor performance compared to their counterparts written in imperative languages such as Fortran or C. Supercompilation is a program transformation that can mitigate many of these problems by removing intermediate structures and perforing program specialization.
Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to call-by-value programs. This hides looping bugs from the programmer, and changes the behavior of a program depending on whether it is optimized or not. We present a supercompilation algorithm for a higher-order call-by-value language and we prove that the algorithm both terminates and preserves termination properties. We also present a stronger variant of the same supercompilation algorithm that removes more intermediate structures as well as give an overview of our current work.

2010-04-16, 15h15 - 16h15, EDIT room

Speaker: Krasimir Angelov
Title: GF as functional-logic language
Abstract: Grammatical Framework (GF) is a domain specific language for describing natural language grammars. Despite that GF is language with very specific application domain, it is also Turing complete and could be used to solve nontrivial tasks in a surprising way. The design of the language has a lot of common with other functional and logic programming languages, most notably: Agda, Haskell, Curry and Lambda Prolog. Curry is an interesting language which combines in a neat way the functional and the logical paradigms but still from type theoretic point of view this is not satisfactory because it doesn't exploit the Curry-Howard isomorphism. Thanks to the dependent types of GF, which relates it to Agda, and thanks to some other specifics in the type system, GF could also be classified as functional-logic language but the two paradigms in GF are combined in the expected way. The execution model of GF also has a lot of common with Lambda Prolog but to cover the full semantics of GF the virtual machine should work in two modes: narrowing and residuation. The residuation mode is something that could be seen in the virtual machine of Curry but not in Lambda Prolog.
In this seminar I will talk about my work in progress on a virtual machine for running GF applications. Not everything is in place yet but the pieces are starting to stick together. As a demo I will show how to solve the classical n-queens problem in GF. From the logical programming paradigm I use backtracking and from the functional paradigm I use efficient deterministic computations. From type theoretical point of view I define the type of all n-queens puzzles.

2010-03-26, 15h15 - 16h00, EDIT room

Speaker: Anders Mörtberg
Title: Implementing a functional language with type inference
Abstract: I have implemented a small functional programming language with type inference as a project in the Advanced Functional Programming course. The type system has unit, product and sum types. The language also supports general recursion and uses call-by-value as evaluation strategy.

2010-03-17, 15h15 - 16h15, Room EC

Speaker: Don Syme, Microsoft Research Cambridge
Title: Parallel and Asynchronous Programming with F#
Abstract: F# is a succinct and expressive typed functional programming language in the context of a modern, applied software development environment (.NET), and Microsoft will be supporting F# as a first class language in Visual Studio 2010. F# makes three primary contributions to parallel, asynchronous and reactive programming in the context of a VM-based platform such as .NET:
(a) functional programming greatly reduces the amount of explicit mutation used by the programmer for many programming tasks
(b) F# includes a powerful “async” construct for compositional reactive and parallel computations, including both parallel I/O and CPU computations, and
(c) “async” enables the definition and execution of lightweight agents without an adjusted threading model on the virtual machine.
In this talk, we’ll look at F# in general, including some general coding, and take a deeper look at each of these contributions and why they matter.
Don Syme is a Principal Researcher at Microsoft Research, Cambridge, and is responsible for the design of the F# programming language. He has contributed extensively to the design of the .NET platform through.NET and C# generics and has a background in verification and machine-checked proof. His research focuses on the technical aspects of programming language design and implementation needed to make functional languages that are simpler to use, interoperate well with other languages and which incorporate aspects of object-oriented, asynchronous and parallel programming. His PhD is from the University of Cambridge, 1998.

2010-03-05, 15h15 - 16h15, EDIT room

Speaker: Jean-Philippe Bernardy
Title: Testing Polymorphic Properties
Abstract: (Joint work with Koen Claessen and Patrik Jansson.)
How can one test a polymorphic property? The issue is that testing can only be performed on specific monomorphic instances, whereas parametrically polymorphic functions are expected to work for any type.
We present a schema for constructing a monomorphic instance for a polymorphic property, such that correctness of that single instance implies correctness for all other instances. We also give a formal definition of the class of polymorphic properties the schema can be used for. Compared with the standard method of testing such properties, our schema leads to a significant reduction of necessary test cases.
The talk is a preview of Jean-Philippe's talk at ESOP

2010-02-05, 15h15 - 16h15, room EC

Speaker: Satnam Singh, Microsoft Research
Title: An Embedded DSL for the Data Parallel Programming of Heterogeneous Systems
Abstract: This presentation introduces an embedded domain specific language (DSL) for data-parallel programming which can target GPUs, SIMD instructions on x64 multicore processors and FPGA circuits. This system is implemented as a library of data-parallel arrays and data-parallel operations with implementations in C++ and for .NET languages like C#, VB.NET and F#. We show how a carefully selected set of constraints allow us to generate efficient code or circuits for very different kinds of targets. Finally we compare our approach which is based on JIT-ing with other techniques e.g. CUDA which is an off-line approach as well as to stencil computations. The ability to compile the same data parallel description at an appropriate level of abstraction to different computational elements brings us one step closer to finding models of computation for heterogonous multicore systems.
Satnam Singh is a senior researcher at Microsoft Research. His work includes research on synthesis of FPGA circuits, hardware design using synchronous languages, heterogenous manycore architectures and concurrent and parallel programming in Haskell.

2010-01-29, 15h15 - 16h15, room EC

Speaker: Lennart Augustsson, Standard Chartered Bank
Title: O, Partial Evaluator, Where Art Thou?
Abstract: Partial evaluation is now a quite old idea, and it has been implemented many times. Partial evaluation is also very widely applicable; almost every problem in computing could use it. But widely used partial evaluators are nowhere to be seen. Why is that? In this talk I will give some examples of where I have used partial evaluation during 15 years of using Haskell commercially. I will give my wish list for a partial evaluator I could actually use (instead of rewriting it over and over), and also contrast this with what is done in the research community.
Lennart Augustsson is a person that turns research in programming languages into practice. He currently works at the Modelling and Analytics Group at Standard Chartered Bank designing domain-specific programming languages used for quantitative modelling. He is known as the author of Cayenne programming language, one of the first Haskell compilers - HBC and as coauthor of Bluespec, a hardware description language. He is also a three-time winner of the Obfuscated C Code Contest.

2010-01-22, 15h15 - 16h15, EDIT room

Speaker: Alejandro Russo
Title: Towards a taint mode in Python via a library
Abstract: Vulnerabilities in web applications present threats to online systems. SQL injection and cross-site scripting attacks (XSS) are among the most common vulnerabilities found nowadays. Popular scripting languages used by the web community (e.g. Ruby, PHP and Python) provide a taint mode approach to discover such vulnerabilities. Taint modes are usually implemented using static analysis or execution monitors. In the latter case, Ruby, PHP, and Python interpreters are modified to include a taint mode.
In this talk, we present a library in Python that provides a taint mode. In this manner, it is possible to avoid any modification of the Python's interpreter. The concepts of decorators and overloading, as well as the presence of references, makes our solution lightweight and particularly neat.
This talk is based on a work-in-progress with Juan Jose Conti.

2009-12-11, 15h15 - 16h15, EDIT room

Speaker: Emil Axelsson
Title: Feldspar: Functional Embedded Language for DSP and Parallelism
Abstract: I will present Feldspar, which is a domain-specific language mainly targeting digital signal processing applications. Feldspar is embedded in Haskell. The deeply embedded core language is low-level enough to enable efficient compilation, yet flexible enough to support more high-level interfaces implemented through shallow combinators. One such interface is a vector library that provides a data type quite similar to Haskell's list type. I will also present our current effort to implement more domain-specific combinators based on the vector library.

2009-12-04, 15h00 - 16h00, EDIT room

Speaker: Jean-Philippe Bernardy
Title: Parametricity and Dependent Types
Abstract: (Joint work with Patrik Jansson and Ross Paterson)
In the paper "Theorems for Free", Phil Wadler has famously shown how to translate the types of System F to logical relations. This translation effectively makes the types available as theorems, that you can use to reason in a higher logic framework.
I will show how the idea generalizes to dependent types. In that case, the source language is powerful enough to represent logical relations, so it serves as target as well. One striking property is that we not only get theorems "for free" but their proofs as well.

2009-11-27, 15h00 - 16h00, EDIT room

Speaker: Koen Claessen
Title: FUI - A Functional GUI Library
Abstract: In this talk, I present ongoing work (well, results after a few afternoons of hacking) on FUI, a new GUI library for Haskell. There have been many designs and implementations of GUI libraries for Haskell over the years. Some are functional/declarative in spirit(such as Fudgets, Gadgets, and solutions based on Functional ReactiveProgramming (FRP)), others give an imperative (IO) interface (such as TkGofer/Yahu, Haggis, WxHaskell, and Gtk2Hs). The aim of FUI is to combine the good ideas from Fudgets, Gadgets, and FRP (declarative feel), and to avoid the more cumbersome features (loop combinators, mixing layout with functionality). The main motivation for FUI is because it is so much fun hacking on these things, but a secondary motivation is that I tried to create a GUI library that would be possible to use in a first-year course on Haskell. I will also discuss the requirements on the library if it is going to be used for teaching, and if I feel they have been met or not.

2009-11-20, 15h00 - 16h00, EDIT room

Speaker: Jonas Duregård
Title: AGATA – Automatic generators for QuickCheck (Master project presentation)
Abstract: In this talk I present Agata, the subject of my master thesis. Agata automates the process of writing test data generators in Haskell. Agata contributes a novel definition of size. This solves the scalability issues of some QuickCheck generators, where the absolute size of test cases grow exponentially to the size-bound provided by QuickCheck. Agata also introduces distribution strategies. By applying a distribution strategy to a generator, the tester can imbue it with specific properties, without changing the code of the generator. Agata is also implemented as an extension to the BNF Converter tool, enabling automatic generation of syntactically correct test data for any context free language.

2009-11-11, 13h15 - 14h30, EDIT room (joint FP + ProgLog talk)

Speaker: Ross Paterson
Title: Applicative functors from left Kan extensions
Abstract: Applicative functors define an interface that is more general, and correspondingly weaker, than that of monads. First used in parser libraries, they are now seeing a wide range of applications. Left Kan extensions, familiar to functional programmers as a kind of existential type, are a source of a range of applicative functors that are not also monads. There is also a generalized form involving arrows, which appears in the permutation parsers of Baars, Loh and Swierstra.

2009-11-06, 15h00 - 16h00, EDIT room

Speaker: Joel Svensson
Title: Obsidan: GPU Computing using Haskell
Abstract: Obsidian is an embedded domain specific language for GPGPU (General Purpose computations on Graphics Processing Units) programming. The Goals of Obsidian is to simplify the implementation of efficient GPU Kernels (the building blocks of larger algorithms on the GPU) by raising the level of abstraction. Still, the programmer should be in control of some of the low level concepts that are important for performance. This presentation will outline the current version of Obsidian, showing some of the strengths and weaknesses of our approach.

2009-10-30, 13h00 - 14h00, room 5453

Speaker: Muhammad Asif
Title: Case Studies in Cryptol (Master project presentation)
Abstract: Digital Signal Processing has become part of many electronic applications these days; confluent to this, domain specific languages are prevailing among practitioners of many engineering domains. Cryptol is a domain specific language for Cryptography, it was designed by Galois and it has been used by NSA since, the time of its invention. Cryptol is a craft of cryptographic specifications; however this project aims at evaluating Cryptol as a domain specific language for digital signal processing algorithms. It also includes a proposal for extensions to Cryptol to make it applicable to DSP algorithms. This thesis derives its motivation from DSL for DSP research that the Functional Programming group has started with Ericsson. The project involved implementing a set of DSP algorithms in Cryptol and analyzing applicability of Cryptol from the experiences in this new domain. This study shows that Cryptol is too specific for Cryptographic algorithms and it is not possible to specify, run or verify many DSP algorithms in Cryptol. However there is a special class of DSP algorithms that are far easier to code in Cryptol than in C or Java. Thin overlap with the DSP algorithm was natural since DSLs are customized for a certain problem area. Evaluation of Cryptol in DSP domain revealed that some enhancements are necessary to make it applicable to DSP algorithms.

2009-10-23, 15h00 - 16h00, EDIT room

Plan: Discover FP activity at Chalmers

This workshop aims at uncovering FP-related projects at our department. We would also like to come up with a HCAR entry. If you are doing something related to FP, using FP in your project or in teaching, please speak up and add yourself to the HCAR sketch area.

2009-10-16, 15h00 - 16h00, room 5453

Speaker: Alejandro Russo
Title: Integrity policies via a library in Haskell
Abstract: Protecting critical data has become increasingly important for computing systems. Language-based technology have been developed over the years to achieve that purpose, leading to special-purpose languages that, in most of the cases, guarantee confidentiality of data, i.e. that secrets are not leaked. The impact of these languages in practice has been rather limited. Nevertheless, rather than producing a new language from scratch, it has been shown that confidentiality can be also guaranteed via a library, which makes this technology more likely to be adopted. Following this line, this work extends a library that provides confidentiality in order to consider another important aspect of security: integrity of data. Integrity of data seeks to prevent that programs destroy, accidentally or maliciously, information. We describe how to enforce two different kind of integrity policies: access control (e.g. certain files should not be written) and data-invariant-like predicates (e.g. sanitization of data) as well as some ideas about how to enforce information-flow integrity policies (e.g. user data does not corrupt or affect critical data pieces). A library that combines confidentiality and integrity policies has not been previously considered. Augmenting the set of enforceable policies develops further the changes for the library to be attractive for programmers. To evaluate our ideas, we propose the implementation of a case study.
This talk is based on a joint work-in-progress with Albert Diserholt.

2009-10-09, 15h00 - 16h00, EDIT room

Speaker: Wouter Swierstra
Title: Chalk: a language for architecture design
Abstract: Before I leave Sweden, I'd like to give one last talk about the work I've done here over the last months. Koen, Mary, and I have been working on designing a language to give high-level descriptions of computer architectures. One of the things that makes architecture design so hard is the many different design constraints: how much will an extra cache speed up this design? How much power will the cache use? Architects lack the language to explore and evaluate such design decisions early in the design process – this is precisely the problem we address. In this talk, I'll give a quick outline of our ideas, discuss some of the non-standard interpretations and analyses we have implemented, and talk you through some of our motivating examples.

2009-10-02, 15h00 - 16h00, EDIT room

Plan: Discussion about FP in education at the department

We will have a discussion about the role of functional programming in the education of students at the department. Students are very welcome to attend the discussion as we would like to hear opinions from their side.

2009-09-25, 15h00 - 16h00, room 6128 (later changed to EDIT room)

Plan: Discussion about some of the ICFP talks

Each person that attended the ICFP should select 2-3 talks and be able to quickly summarise them and tell his/her opinion about the talk/paper.

2009-06-12, 15h00 - 16h00, EDIT room

Plan: Talk of 40 minutes

Speaker: Wouter Swierstra
Title: Data types à la carte
Abstract: In this talk, I will describe a technique in Haskell for assembling both data types and functions from isolated individual components. Time permitting, I'd like to show how the same technology can be used to combine free monads and, as a result, structure Haskell's monolithic IO monad.

2009-06-04, 10h00 - 11h00, room 5453

Plan: Talk of 40 minutes

Speaker: Jean-Philippe Bernardy
Title: Testing Polymorphic Functions: The Initial View
Abstract: Many useful functions are parametrically polymorphic. Testing can only be applied to monomorphic instances of polymorphic functions. If we verify correctness of one instance, what do we know of all the other instances? We present a schema for constructing a monomorphic instance such that correctness of that single instance implies correctness for all other instances.
This is joint work with Koen Claessen and Patrik Jansson.

2009-05-29, 15h00 - 16h00, room 5453

Plan: Talk of 40 minutes

Speaker: Jan Rochel
Title: Very Lazy Evaluation
Abstract: In the talk I will present my diploma thesis, which introduces a new execution model for non-strict, functional programming languages. It relies on a new concept in which function arguments are handled more lazily than in existing graph-reduction based models. This leads to a new type of abstract machine that promises very efficient program execution. A proof-of-concept implementation demonstrates the applicability of the approach.

2009-05-15, 15h00 - 16h00, EDIT room

Plan: Talk of 40 minutes

Speaker: Andres Löh
Title: Generic programming with fixed points for mutually recursive datatypes
Abstract: Many datatype-generic functions need access to the recursive positions in the structure of the datatype, and therefore adopt a fixed point view on datatypes. Examples include variants of fold that traverse the data following the recursive structure, or the Zipper data structure that enables navigation along the recursive positions. However, Hindley-Milner-inspired type systems with algebraic datatypes make it difficult to express fixed points for anything but regular datatypes. Many real-life examples such as abstract syntax trees are in fact systems of mutually recursive datatypes and therefore excluded. In the talk, I will desceribe a technique that allows a fixed-point view for systems of mutually recursive datatypes. I will also present examples, most prominently the Zipper, that demonstrate that the approach is widely applicable.

2009-05-08, 15h00 - 16h00, EDIT room

Plan: Talk of 40 minutes

Speaker: Neil Jones
Title: Termination Analysis of the Untyped lambda-Calculus
Abstract: An algorithm is developed that, given an untyped lambda-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the ``size-change principle'' earlier applied to first-order programs. The algorithm is sound (and proven so) but not complete: some lambda-expressions may in fact terminate under call-by-value evaluation, but not be recognised as terminating.
The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF.
Based on a paper "Termination Analysis of the Untyped lambda-Calculus" by Neil D. Jones and Nina Bohr, DIKU, University of Copenhagen and IT University of Copenhagen

2009-04-24, 15h00 - 16h00, room 5453

Plan: A talk by Nick, 40 minutes including questions

Speaker: Nick Smallbone
Title: QuickSpec: Formal Specifications for Free
Abstract: I will talk about QuickSpec, a tool developed by Koen, John and me that generates algebraic specifications from functional programs. QuickSpec uses no theorem proving, only simple techniques based on testing.

2009-04-03, 15h00 - 16h00, room 5453

Plan: A talk by Ulf, 40 minutes including questions

Speaker: Ulf Norell
Title: A Dependently Typed Database Binding
Abstract: Interfacing to a database is a common task in systems development and any self respecting programming language comes with libraries for doing this. However, these libraries are in most cases untyped--queries sent to the database are either strings or some simple structured representation that has no relation to the actual layout of the database being queried. An exception is the HaskellDB library which supports well-typed interaction with the database, but requires a tool to be run at compile time to generate Haskell types corresponding to the database tables.
I will show a simple dependently typed database library for Agda, based on ideas by Nicolas Oury and Wouter Swierstra (2008)[1], where queries are guaranteed to be well-typed with respect to the database being queried and which doesn't require the database to be queried at compile time. It also supports changing the database layout during the execution of a program.
[1] Oury and Swierstra, The Power of Pi. ICFP 2008.

2009-03-27, 15h00 - 16h00, room 5453

Plan: A talk by John, 40 minutes including questions; Discussion about the website

Speaker: John Hughes
Title: eqc_fsm: State machine specifications in QuickCheck
Abstract: I'll talk about eqc_fsm, a new module developed for Quviq's QuickCheck as part of the ProTest project. It is designed for expressing state machine diagrams, along the lines of UML state charts, as QuickCheck specifications. Compared to QuickCheck's previous state machine support, eqc_fsm permits more concise and less error-prone specifications, and can offer help in analysing the distribution of the generated random tests, and indeed, automating the assignment of suitable weights to achieve a "best" distribution of test cases--whatever that means, which is an interesting question in its own right.

2009-03-20, 15h00 - 16h00, room 5453

Speaker: Michał Pałka
Title: Finding Race Conditions in Erlang with QuickCheck and PULSE
Abstract: I will present a user-level scheduler which, in combination with QuickCheck and a trace visualizer, can be used to debug concurrent Erlang programs giving a high chance for finding concurrency bugs in unit testing.

2009-03-13, 15h00 - 16h00, EDIT room

Plan: Two talks of 20 minutes

Talk 1

Speaker: Jean-Philippe Bernardy
Title: Purely Functional Incremental Parsing
Abstract: I'll give a summary of the techniques used in the parsing library developed for the Yi editor. Then I propose to detail how both incremental and lazy parsing can be combined in a combinator library.

Talk 2

Speaker: Patrik Jansson
Title: Generic Libraries in C++ with Concepts from High-Level Domain Descriptions in Haskell - A Domain-Specific Library for Computational Vulnerability Assessment
Abstract: See ComputationalVulnerabilityAssessment

2009-03-06, 15h00 - 16h00, EDIT room

Plan: One talk of 60 minutes

Talk

Speaker: Wouter Swierstra
Title: The Hoare State Monad
Abstract: Monads help structure functional programs. Yet proofs about monadic programs often start by expanding the deﬁnition of return and bind. This seems rather wasteful. If we exploit this structure when writing programs, why should we discard it when we writing proofs? I will show how to verify functional programs inhabiting the state monad, with the express aim of taking advantage of the monadic structure of our programs to guide the veriﬁcation process.