Preface

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.

• Neil Ghani, University of Strathclyde, Glasgow, UK
  Fibred data types
• Danko Ilik, Goce Delčev University of Štip, Republic of Macedonia
  Dependently typed continuation monads as models in logic

• Thorsten Altenkirch, University of Nottingham, UK
• Robert Atkey, University of Strathclyde, Glasgow, UK
• James Chapman (co-chair), Institute of Cybernetics, Tallinn, Estonia
• Nils Anders Danielsson, Chalmers University and University of Gothenburg, Sweden
• Martín Escardó, University of Birmingham, UK
• Ichiro Hasuo, University of Tokyo, Japan
• Ralf Hinze, University of Oxford, UK
• Neelakantan Krishnaswami, Microsoft Research, Cambridge, UK
• Paul Blain Levy (co-chair), University of Birmingham, UK
• Daniel R. Licata, Carnegie Mellon University, Pittsburgh, PA
• Ulrich Schöpp, LMU Munich, Germany
• Alex Simpson, University of Edinburgh, UK
• Matthieu Sozeau, INRIA, Paris, France
• Sam Staton, University of Cambridge, UK

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

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

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 Σ⁰₁-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.