Recent Changes - Search:

FP


The Chalmers FP wiki is part of the CSE dept. wiki.

Recent Changes


edit SideBar

FP /

FPWeeklyMeeting

Want to five 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

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

Speaker
Matthías Páll Gissurarson
Title
TBA
Abstract
TBA

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.

Past Meetings

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 definition 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 verification process.
Edit - History - Print - Recent Changes - Search
Page last modified on November 16, 2017, at 12:16 PM