Main Menu |
---|

Functional Programming Lab Seminars |

The Functional Programming Laboratory Seminar programme for the 2013-14 academic year is being administrated by Christian Sattler (cvs at cs.nott....). Please get in contact with him if you would like to present a talk, or have any general comments! ## Friday 28th February 2014, C1, 09.00 Ralf Hinze (Oxford)
## Friday 14th February 2014, C60, 16.00 Neel Krishnaswami (Birmingham) GADTs, or generalized algebraic data types, are a feature found in functional languages like Ocaml and Haskell. Essentially, they permit indexing data types with additional information, so that (for instance) lists may be indexed with their length, or term syntaxes with the type they will evaluate to. In this talk, Ill show how these types have a logical interpretation, in terms of a type-theoretic interpretation of equality type originally introduced by Jean-Yves Girard and Peter Schroeder-Heister to model equality in first-order logic. This equality has a different (and stronger) elimination form than the equality type of Martin-Loef type theory, and leads to a different proof theory -- in particular, it is what justifies the practice of omitting needless cases from pattern match statements. I'll show how this leads to a type inference algorithm whose structure arises from the proof-theoretic notion of focalization. This makes it possible for us to not only give an efficient algorithm, but also to prove it sound and complete with respect to a natural declarative semantics. Along the way, we'll meet new versions of some familiar friends, such as principal types. This is ongoing work with Joshua Dunfield.
## Friday 7th February 2014, C60, 16.00 Edwin Brady (St. Andrews) Idris is an experimental functional programming language with full spectrum dependent types, meaning that types can be predicated on any value. Its syntax is influenced by Haskell. As well as full dependent types it supports records, type classes, tactic based theorem proving, totality checking, and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to programming practitioners while still supporting efficient systems programming via an optimising compiler and interaction with external libraries. In this talk I will introduce dependently typed programming using Idris, and demonstrate its features using several examples including verified compression by run-length encoding, management of state and side-effects and resource correctness proofs.
## Friday 6th December 2013, C60, 12.00 Nicola Gambino (Leeds) Homotopy Type Theory and Voevodsky's Univalent Foundations of Mathematics programme have attracted a significant amount of interest and activity in recent years. A recent conference on these topics, held at the Centre de Recerca Matematica in Barcelona, provided a good overview of the state of the art on the subject. I will report on recent advances presented at the CRM conference and discuss some open problems in the field.
## Friday 29th November 2013, C60, 13.00 Richard Mortier (Nottingham) I will talk about Mirage, a framework for building what we have called unikernels: compact, efficient single-purpose virtual machines for building cloud services. I will elaborate our goals, discuss our design and some implementation details, present some performance results, and give a status update. Mirage was published in ASPLOS'13 "Unikernels: Library Operating Systems for the Cloud".
## Friday 8th February 2013, C01, 16.00 Richard Bird (Oxford) An informal talk, suitable for anyone who has done a first course in functional programming, illustrating how to calculate a simple program using the laws of functional programming. During the talk the audience will be given a chance to think about the problem and to come up with their own solution.
## Monday 21st January 2013, LT1, 12.00 Lennart Augustsson (Standard Chartered Bank)
Domain-specific languages (DSLs) enable domain experts themselves to realise the full potential of computers for solving problems in their domains without the time and cost overhead of involving programmers to develop tailor-made applications. The scope for deploying DSLs is as large and diverse as the domains where computers are or could be used to solve problems, and, with potentially huge payoffs, this is reflected in an upsurge of interest in what also has been termed Language-Oriented Programming. However, developing a high-quality, performant DSL is itself a costly proposition. In this talk, Lennart Augustsson will show how modern, typed, functional programming language technology, exemplified by Haskell, in combination with modern compiler technology (LLVM), can ease this task significantly by implementing a toy DSL as an embedding in Haskell in three steps: first, getting a typed DSL embedded in Haskell; then, executing such a language using an interpreter; finally, using LLVM to generate very efficient code for the DSL. About the speaker: Lennart Augustsson is a computer scientist currently employed at Standard Chartered Bank in London. He has previously worked as a lecturer at Chalmers University of Technology as well as for a number of companies including Sandburst and Credit Suisse. His field of research is functional programming and implementations of functional languages. During his career he has done different things, e.g., written about four Haskell compilers, designed and implemented a hardware design language (Bluespec), written USB device drivers, winning the International Obfuscated C Code Contest three times, and designing packet routing hardware. He also likes to watch total eclipses of the sun.
## Monday 3rd December 2012, C01 (Computer Science), 16.00
## Tuesday 28th August 2012, C60 (Computer Science), 13.00Neil Sculthorpe (Kansas)
The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks. To address this, we have implemented HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimisation pipeline. With HERMIT, users can experiment with optimisations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. Hermit provides a transformation API that can be used to build higher-level rewrite tools. In this talk I will describe one HERMIT application -- a read-eval-print shell for performing transformations using HERMIT. I will also demonstrate using this shell to prototype an optimisation on a specific example, and discuss our initial experiences and remaining challenges.
## Friday 30th March 2012, C60 (Computer Science), 16.00Conor McBride (Strathclyde)
It's a well known fact that a total programming language can't encode its own interpreter. Some advocates and most detractors of total programming note that it comes at the cost of Turing completeness, another well known fact. These well known facts are about as true as the fact that "Haskell can't handle I/O." I shall talk about ways in which total languages can model the risk of nontermination, and show you a method I have found useful, inspired by notions of algebraic effect. If time permits, I shall sketch an appropriate effect-checking type discipline and/or show how to automate the construction of Bove-Capretta domain predicates by recursive computation over the relevant free monad.
## Thursday 15th March 2012, A08 (Business School South), 13.00Cezar Ionescu (Institute of Climate Impact Research, Potsdam) Calculation and Communication "Vulnerability" is an important concept in global change studies. At the Potsdam Institute for Climate Impact Research (PIK), we have come up with a formal model of vulnerability, in order to compare different vulnerability assessments (a task called meta-analysis), but also in order to better structure and test the software used for these assessments, I'd like to present some aspects of this formalisation which are hopefully relevant and/or entertaining. ## Friday 2nd March 2012, C60 (Computer Science), 15.00George Giorgidze (Tubingen) Bringing Back Monad Comprehensions and Extending Database Supported Haskell The first half of my talk will be about a Glasgow Haskell Compiler (GHC) extension that generalises Haskell's list comprehension notation to monads. The monad comprehension notation implemented by the extension supports generator and filter clauses, as was the case in the Haskell 1.4 standard. In addition, the extension generalises the recently proposed parallel and SQL-like list list comprehension notations to monads. I will give a formal definition of the aforementioned generalisations. The extension has been available in GHC since the version 7.2. I will argue why the do notation is not always a good fit for monadic libraries and embedded domain-specific languages, especially for those that are based on collection monads. I will briefly discuss the related GHC extension for the list notation overloading that we are currently working on. The second half of my talk will be about how we use monad comprehensions in Database Supported Haskell (DSH). DSH is a Haskell library that allows execution of idiomatic, list processing program fragments on a relational database management system (RDBMS). DSH can be used to allow existing Haskell programs to operate on large scale data (e.g., larger than the available heap) or to query existing database resident data with Haskell. In addition to the standard list processing combinators, database-executable program fragments can also be written using the monad comprehension notation. At the end of my talk, if time permits, I will briefly describe our ongoing work that uses Haskell's new generic deriving mechanism to extend the database-supported program execution to all algebraic data types.
## Wednesday 11th January 2012, C60 (Computer Science), 15.00Ohad Kammar (Edinburgh)
We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi's monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operational symbols. SLIDES
## Friday 2nd December 2011, A06 (BS-South), 15.00Danel Ahman (Cambridge)
Abbott, Altenkirch, Ghani and others have taught us that many parameterised datatypes (set functors) can be usefully analysed via container representations in terms of a set of shapes and a set of positions in each shape. Our work builds on the observation that datatypes often carry additional structure that containers alone do not account for. We introduce directed containers to capture the common situation where every position in a data structure determines another data structure, informally the sub-data structure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and data structures with a designated position (zippers). While containers denote set functors via a fully-faithful functor, directed containers interpret fully-faithful functors into comonads. But more is true: every comonad whose underlying functor is a container is represented by a directed container. In fact, directed containers are the same as containers that are comonads. We have formalised our development in the dependently typed programming language Agda.
## Friday 25th November 2011, C60 (Computer Science), 15.00-16.00Per Kristian Lehre (Nottingham)
Evolutionary algorithms and related meta-heuristics are widely applied to solve real-world optimisation problems. However, the theoretical foundations behind these heuristics are rather weak. One of the fundamental problems is to derive upper and lower bounds on their expected runtime. The runtime is in this context the random variable describing the number of candidate solutions the evolutionary algorithm investigates before a solution of acceptable quality is found. Runtime analysis can provide insights into how the performance of evolutionary algorithms depends on the parameter-settings of the algorithm, and on the characteristics of the underlying optimisation problem. This talk is an introduction to runtime analysis of evolutionary algorithms. The first part covers the basic definitions, and gives an overview of the results that have been obtained. The second part focusses on the so-called exploration-exploitation balance in evolutionary algorithms. We will see how this balance has an exponentially large impact on the runtime. Finally, I will show how I use OCaml to experiment with evolutionary algorithms.
## Friday 4th November 2011, C60 (Computer Science), 15.00-16.15Ki Yung Ahn (Portland State)
This talk is about the design of a small normalising language Nax, named after Nax P. Mendler. in Nax, you are allowed to introduce arbitrary recursive types and eliminate them by principled iteration/recursion combinators following the style of Mendler. There is a rich family of such combinators whose termination properties are well studied, where some of which are our own contribution (see our ICFP'11 paper here). The motivation for this work is to explore the design space of languages aiming for both (functional) programming and (logical) reasoning. Most typed functional programming languages allow formation of arbitrary recursive types with no guarantee of normalisation. Many of the typed logical reasoning systems are guaranteed to normalise but limit the formation of recursive types. Our language Nax is an attempt to establish a core language with the good properties of both worlds.
## Wednesday 12th January 2011, (Dearing Building B85), 11.00Anil Madhavapeddy (Cambridge) Mirage: a multi-scale, functional operating systemApplications run on all kinds of environments these days: multicore desktops, virtual cloud infrastructures, smart-phones, and web browsers. These diverse environments make it worth rethinking the long-term future of our software stacks; do we really want to continue bundling gigabytes of general-purpose OS software with every single cloud image? Is there any point holding onto decades-old interfaces such as POSIX any more? How do advances in programming languages fit into the way we build operating systems?
## Friday 2010-11-12, C60, 15-16Fredrik Nordvall Forsberg (Swansea)
Induction is a powerful and important principle of definition, especially so in dependent type theory and constructive mathematics. Induction-induction (named in reference to Dybjer and Setzer's induction-recursion) is an induction principle which gives the possibility to simultaneously introduce a set A together with an A-indexed set B (i.e. for every a : A, B(a) is a set). Both A and B(a) are inductively defined, and the constructors for A can also refer to B and vice versa. Shin-Cheng Mu (Academia Sinica, Taiwan) |