Published: 11th February 2012 DOI: 10.4204/EPTCS.76 ISSN: 2075-2180 |
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: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
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.
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 Σ^{0}_{1}-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.