Published: 11th February 2012
DOI: 10.4204/EPTCS.76
ISSN: 2075-2180


Proceedings Fourth Workshop on
Mathematically Structured Functional Programming
Tallinn, Estonia, 25 March 2012

Edited by: James Chapman and Paul Blain Levy

James Chapman and Paul Blain Levy
Invited Presentation: Fibred data types
Neil Ghani
Invited Presentation: Dependently typed continuation monads as models in logic
Danko Ilik
Parametric Compositional Data Types
Patrick Bahr and Tom Hvitved
Step-Indexed Normalization for a Language with General Recursion
Chris Casinghino, Vilhelm Sjöberg and Stephanie Weirich
An Investigation of the Laws of Traversals
Mauro Jaskelioff and Ondrej Rypacek
A Formal Comparison of Approaches to Datatype-Generic Programming
José Pedro Magalhães and Andres Löh
Evaluation strategies for monadic computations
Tomas Petricek
Tracing monadic computations and representing effects
Maciej Piróg and Jeremy Gibbons
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump and Stephanie Weirich
From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
Wouter Swierstra


This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012.

MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. As the range of papers presented in this year's workshop shows, this is a fruitful interface.

We are honoured to host the following invited speakers: We are grateful to our programme committee:

and to Andreas Abel, Yoichi Hirai, Peter Morris and Keiko Nakata for additional refereeing. We would also like to thank the ETAPS 2012 organizers, and the EPTCS staff.

MSFP 2012 was supported by the Estonian Centre of Excellence in Computer Science (EXCS), a project financed by the European Regional Development Fund (ERDF).

James Chapman and Paul Blain Levy, February 2012

Fibred data types

Neil Ghani

We believe that data types are about to undergo a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. Historically, in the 1970s a foundational theory of data types emerged in the shape of inductive types; in the 1990s a more expressive theory of data types emerged based upon inductive families where every piece of data comes with an index. Crucially, these indexes are fixed in advance of the inductive definition of the data.

The next generation of data types will consist of indexed types where, crucially, the indexes are generated inductively at the same time as the data. Inspired by the theory of fibrations which provides an elegant abstract framework to model different type theories, we develop a new theory of these data types that we call fibred data types. I'll describe this work while being sensitive to those who are allergic to fibrations.

Dependently typed continuation monads as models in logic

Danko Ilik

Since Griffin in 1990 remarked that one can extend the Curry-Howard correspondence to classical logic by assigning to call/cc the type of Peirce's Law, it has been thought that computation with control operators (and computational effects, more generally) corresponds to reasoning in classical logic, while pure effect-free computation corresponds to reasoning in intuitionistic logic. However, in recent works of Herbelin and the speaker, it has been shown that by using delimited control operators for proving Σ01-formulas, one can obtain logical systems that are constructive (preserve the disjunction and existence properties of intuitionistic logic), yet can prove principles which are independent of intuitionistic logic, like the predicate- logic versions of Markov's Principle and the Double-negation Shift schema.

In this talk we will see one precursor to those works, the notions of model based on dependently typed continuation monads, that are complete for classical and for intuitionistic predicate logic. These completeness proofs, together with a corresponding evaluator, can be used as a normalization-by-evaluation procedure for the underlying proof-term λ-calculi. We will also see how the method is extended to show normalization-by-evaluation for a constructive system of delimited control operators that can prove Double- negation Shift.