FP
The Chalmers FP wiki is part of the CSE dept. wiki.
Recent Changes
edit SideBar

Want to give a Functional Programming related talk? Talk to Alex Gerdes (alexg at chalmers dot se) to book a slot. We usually have a talk every Friday at 10:00.
Google Calendar Links
Planned talks
20181026, 10:00, EDIT EA
 Speaker
 Josef Sveningsson, Ericsson
 Title
 TBA (gradual typing)
 Abstract
 TBA
 Slides
 hughes_statistical_properties.pdf
Past Meetings
20181005, 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 propertybased tests, based on work that Nick Smallbone and I have done recently, with inspiration from a Quviq customer.
20180928, 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 dryrun of a talk I will be giving at the PLAS workshop colocated with CCS.
[1] A Core Calculus of Dependency  Abadi et al.
[2] Embedding DCC in Haskell  Algehed and Russo
20180921, 10:00, EDIT Analysen
 Speaker
 Nachiappan Valliappan, Chalmers
 Title
 Typing the Wild in Erlang, HindleyMilner 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 HindleyMilner type system for Erlang which strives to remain sound without being too restrictive. Our type checker—unlike contemporary implementations of HindleyMilner—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 dryrun 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
20180914, 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' distributionsspecially when it comes to userdefined 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 compiletime) 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 realworld applications. When generating random values, our synthesized QuickCheck generators show improvements in code coverage when compared with those automatically derived by stateoftheart tools.
Link: https://arxiv.org/abs/1808.01520
20180912, 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.
20180907, 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 dryrun 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
20180608, 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 parametricitybased 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 datatypes from the programmer. In our formulation, the M language constitutes both metalanguage and trusted computing base.
[1] Proofs for Free, J.P. Bernardy, P. Jansson, R. Patterson, JFP 2012
20180601, 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' donotation. It does this by looking at interstatement 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 datafetching 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' donotation Into Applicative Operations (Marlow, PeytonJones, Kmett, & Mokhov, Haskell Symposium 2016) Haxl was introduced with There Is No Fork (Marlow, Brandy, Coens, & Purdy, ICFP 2014)
20180525, 10:00, EDIT EA
 Speaker
 Matthías Páll Gissurarson, Chalmers
 Title
 Suggesting Valid Hole Fits for TypedHoles (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 TypedHoles" and present a lightweight, practical extension to the typedholes of GHC that improves user experience and facilitates a style of programming called "TypeDriven Development".
20180518, 10:00, EDIT 3364
 Speaker
 Süleyman Savas, Högskolan i Halmstad
 Title
 Designing DomainSpecific 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 socalled 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 domainspecific 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 networkonchip. 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 handwritten 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
20180420, 10:00, EDIT 3364
 Speaker
 Troels Henriksen, DIKU, Copenhagen University
 Title
 Design and implementation of the Futhark programming language
 Abstract
 Futhark is a dataparallel programming language under development at DIKU. The language supports (regular) nested dataparallelism 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.
20180309, 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 nonexpert)
 Abstract
 Many domainspecific 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 compilarfor 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 difficulttopenetrate 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 simpletyped lambda terms and another for CCC and show how to translate programs form one into the othera wellknown 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 callbyvalue semantics. Hence, we also show how to execute CCC programs via the categorical abstract machine (CAM). Moreover, we extend our implementation of simpletyped 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 jointwork with Alejandro Russo.
20180302, 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 effectrelated 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, realworld examples.
 Slides
 https://github.com/dorchard/effectfulexplanationstalk
20171215, 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.
20171208, 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 languageagnostic manner.
20171201, 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.
20171103, 10:00, EDIT 3364
 Speaker
 Aarne Ranta
 Title
 Explainable Machine Translation
 Abstract
 Explainable Artificial Intelligence (XAI) is an attempt to mitigate the blackbox character of machine learning based AI techniques. A prime example of such techniques is Neural Machine Translation (NMT), which works via an endtoend string transformation where the intermediate stages are machinecreated 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.
20171027, 10:00, EDIT 3364
 Speaker
 Emil Axelsson
 Title
 Rhino  a DSL for datacentric applications
 Abstract
 n this talk I will present our development of Rhino at Mpowered Business Solutions. Rhino is a functional DSL/framework targeting datacentric 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 thirdparty plugins (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.
20171006, 10:00, EDIT 3364
 Speaker
 JeanPhilippe 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 higherorder 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
20170915, 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 lookup 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 floatingpoint 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.
20170901, 10:00, EDIT 8103
 Speaker
 Anton Ekblad
 Title
 A MetaEDSL for Distributed Web Applications
 Abstract
 We present a domainspecific 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 thirdparty EDSLs, and enables typesafe, accesscontrolled 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 finegrained 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.
20170825, 10:00, EDIT EF
 Speaker
 Markus Aronsson
 Title
 Hardware Software CoDesign in Haskell
 Abstract
 I'll present a library in Haskell for programming Field Programmable Gate Arrays (FPGAs), including hardware software codesign. Code for software (C) and hardware (VHDL) is generated from a single program. The library is however open in that our typebased 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.
20170616, 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 wellscoped.
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 wellscoped, 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!
20170609, 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 cuttingedge theorem provers use structural induction, which makes it impossible for them to prove properties about nonstructurally 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 nonstructurally recursive functions.
20170602, 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.
20170519, 10:00, EDIT EA
 Speaker
 Alejandro Russo
 Title
 Securing Lazy Programs
 Abstract
 InformationFlow Control libraries exists in the functional programming language Haskell as embedded domainspecific 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 sharedresources which can be invoked by the library, e.g., references. With lazy evaluation in place, variables introduced by letbindings and function applicationwhich cannot be controlled by LIObecome 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 valuesome 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 subexpression which they might depend on. We provide a formalization of the security MAC library and lazyDup in the form of a concurrent callbyneed 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).
20170512, 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, subjectmatter experts are aware of additional relevant type information, but this information is ignored by the information system. Consequently, “typesafe” expressions can produce nonsensical answers, which could have been avoided, had typechecking 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 typesafety issues in advance of the expression being evaluated against the data. To illustrate our approach, we have implemented rulebased software that performs this enhanced typechecking on SQL queries that contain complex arithmetic expressions, including statistical aggregation functions.
What we have NOT done is to develop a more generalpurpose solution where this kind of type inference is incorporated into a suitable functional programming language.
20170505, 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 domainspecific language for expressing cognitive skills and problem solving procedures. A strategy for a cognitive skill can be used to give feedback, hints, and workedout 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, tracebased 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
20170428, 10:00, EDIT 8103
 Speaker
 SvenBodo Scholz, HeriotWatt University
 Title
 A LambdaCalculus 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 / listbased setting.
20170421, 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 informationflow 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 workinprogress with Alejandro Russo.
20170407, 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.
20170331, 10:00, EDIT 3364
 Speaker
 Alejandro Russo
 Title
 Building Secure Embedded Systems Using Languagebased Techniques
 Abstract
 Lowlevel 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 typesystem 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.
20170317, 10:00, EDIT 3364
 Speaker
 Alejandro Russo
 Title
 Choose your own adventure: MultiFaceted Value Semantics, Secure MultiExecution 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 typesystems) to dynamic ones (as execution monitors). Despite when possible leaks are detected, such techniques raise false alarmsan aspect that is endemic to almost any enforcement. Secure MultiExecution (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 MultiFaceted 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 elsebranch) 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 multiexecutions) 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 samesomething 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 stuckwe hope that the FP crowd could provide us with some enlightenment on how to proceed forward.
This talk is based on a workinprogress with Thomas Schmitz, Cormac Flanagan, Nataliia Beilova, and Tamara Rezk.
20170310, 10:00, EDIT 8103
 Speaker
 Jurriaan Hage
 Title
 DomainSpecific Type Error Diagnosis in Haskell
 Abstract
 A challenge in type error diagnosis for general purpose languages suitable for embedding domainspecific 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.
20170303, 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 wellformedness conditions satisfied by construction. The dependentlytyped 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 (PiWare) with a lowlevel, 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.
20170224, 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, objectprogram 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 domainspecific 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 languagerelated education and knowledge management.
 Slides
 http://softlang.unikoblenz.de/book/slides/HsSleMp.pdf
20170217, 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 singlethreaded 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
20170210, 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
20170203, 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 multimillion 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 nutsandbolts involved in applying formal verification in industry.
 Slides
 FVinPractice.pdf
20170127, 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 everincreasing diversity of hardware and many new application scenarios for software, such as cyberphysical 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 upfront 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 VRfunded project that aims at building a method and tool suite supporting a truly incremental development of variantrich systems, exploiting a spectrum between both opposing approaches. I will present the main underlying idea, important concepts of variantrich 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.
20170120, 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
20161209, 13:00, EDIT 8103
 Speaker
 Patrik Jansson
 Title
 Sequential decision problems, dependent types and generic solutions,
 Abstract
 We present a computerchecked generic implementation for solving finitehorizon sequential decision problems. This is a wide class of problems, including intertemporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle timestep dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, nondeterministic, 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 computerchecked 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_201611_preprint.pdf
20161202, 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 typelevel 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/enus/research/wpcontent/uploads/2016/11/treesthatgrow.pdf
20100618, 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 highlevel 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/
20100614, 14h15  15h15, room ED
 Speaker
 Peter A. Jonsson, Luleå University of Technology
 Title
 Supercompilation and CallByValue
 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 callbyvalue 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 higherorder callbyvalue 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.
20100416, 15h15  16h15, EDIT room
 Speaker
 Krasimir Angelov
 Title
 GF as functionallogic 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 CurryHoward 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 functionallogic 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 nqueens 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 nqueens puzzles.
20100326, 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 callbyvalue as evaluation strategy.
20100317, 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 VMbased 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 machinechecked 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 objectoriented, asynchronous and parallel programming. His PhD is from the University of Cambridge, 1998.
20100305, 15h15  16h15, EDIT room
 Speaker
 JeanPhilippe 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 JeanPhilippe's talk at ESOP
20100205, 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 dataparallel programming which can target GPUs, SIMD instructions on x64 multicore processors and FPGA circuits. This system is implemented as a library of dataparallel arrays and dataparallel 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 JITing with other techniques e.g. CUDA which is an offline 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.
20100129, 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 domainspecific 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 threetime winner of the Obfuscated C Code Contest.
20100122, 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 crosssite 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 workinprogress with Juan Jose Conti.
20091211, 15h15  16h15, EDIT room
 Speaker
 Emil Axelsson
 Title
 Feldspar: Functional Embedded Language for DSP and Parallelism
 Abstract
 I will present Feldspar, which is a domainspecific language mainly targeting digital signal processing applications. Feldspar is embedded in Haskell. The deeply embedded core language is lowlevel enough to enable efficient compilation, yet flexible enough to support more highlevel 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 domainspecific combinators based on the vector library.
20091204, 15h00  16h00, EDIT room
 Speaker
 JeanPhilippe 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.
20091127, 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 firstyear 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.
20091120, 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 sizebound 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.
20091111, 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.
20091106, 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.
20091030, 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.
20091023, 15h00  16h00, EDIT room
Plan: Discover FP activity at Chalmers
This workshop aims at uncovering FPrelated 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.
20091016, 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. Languagebased technology have been developed over the years to achieve that purpose, leading to specialpurpose 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 datainvariantlike predicates (e.g. sanitization of data) as well as some ideas about how to enforce informationflow 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 workinprogress with Albert Diserholt.
20091009, 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 highlevel 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 nonstandard interpretations and analyses we have implemented, and talk you through some of our motivating examples.
20091002, 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.
20090925, 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 23 talks and be able to quickly summarise them and tell his/her opinion about the talk/paper.
20090612, 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.
20090604, 10h00  11h00, room 5453
Plan: Talk of 40 minutes
 Speaker
 JeanPhilippe 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.
20090529, 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 nonstrict, functional programming languages. It relies on a new concept in which function arguments are handled more lazily than in existing graphreduction based models. This leads to a new type of abstract machine that promises very efficient program execution. A proofofconcept implementation demonstrates the applicability of the approach.
20090515, 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 datatypegeneric 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, HindleyMilnerinspired type systems with algebraic datatypes make it difficult to express fixed points for anything but regular datatypes. Many reallife 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 fixedpoint view for systems of mutually recursive datatypes. I will also present examples, most prominently the Zipper, that demonstrate that the approach is widely applicable.
20090508, 15h00  16h00, EDIT room
Plan: Talk of 40 minutes
 Speaker
 Neil Jones
 Title
 Termination Analysis of the Untyped lambdaCalculus
 Abstract
 An algorithm is developed that, given an untyped lambdaexpression, can certify that its callbyvalue evaluation will terminate. It works by an extension of the ``sizechange principle'' earlier applied to firstorder programs. The algorithm is sound (and proven so) but not complete: some lambdaexpressions may in fact terminate under callbyvalue evaluation, but not be recognised as terminating.
The intensional power of sizechange 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 lambdaCalculus" by Neil D. Jones and Nina Bohr, DIKU, University of Copenhagen and IT University of Copenhagen
20090424, 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.
20090403, 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 untypedqueries 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 welltyped 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 welltyped 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.
20090327, 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 errorprone 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 caseswhatever that means, which is an interesting question in its own right.
20090320, 15h00  16h00, room 5453
 Speaker
 Michał Pałka
 Title
 Finding Race Conditions in Erlang with QuickCheck and PULSE
 Abstract
 I will present a userlevel 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.
20090313, 15h00  16h00, EDIT room
Plan: Two talks of 20 minutes
Talk 1
 Speaker
 JeanPhilippe 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 HighLevel Domain Descriptions in Haskell  A DomainSpecific Library for Computational Vulnerability Assessment
 Abstract
 See ComputationalVulnerabilityAssessment
20090306, 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.
