The fourth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? Type theory without universes? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control.
MSFP 2012 will be held on 25 March. This time around, we're delighted to be affiliated with ETAPS 2012, running 24 March - 1 April in Tallinn, Estonia.
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.
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.
| 09.00-10.00 |
Invited talk Fibred Data Types Neil Ghani |
| 10.00-10.30 |
Step-Indexed Normalization for a Language with General Recursion Chris Casinghino, Vilhelm Sjöberg and Stephanie Weirich |
| 10.30-11.00 | Coffee |
| 11.00-11.30 | An Investigation of the Laws of Traversals Mauro Jaskelioff and Ondrej Rypacek |
| 11.30-12.00 | Evaluation strategies for monadic computations Tomas Petricek |
| 12.00-12.30 | Tracing monadic computations and representing effects Maciej Piróg and Jeremy Gibbons |
| 12.30-14.00 | Lunch |
| 14.00-15.00 | Invited talk Dependently typed continuation monads as models in Logic Danko Ilik |
| 15.00-15.30 | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine Wouter Swierstra |
| 15.30-16.00 | Coffee |
| 16.00-16.30 | Parametric Compositional Data Types Tom Hvitved and Patrick Bahr |
| 16.30-17.00 | A Formal Comparison of Approaches to Datatype-Generic Programming José Pedro Magalhães and Andres Löh |
| 17.00-17.30 | Irrelevance, Heterogenous 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 |
Submissions were welcomed on, but by no means restricted to, topics such as:
The proceedings have been published by EPTCS as EPTCS 76. Participants of the workshop will receive a print copy of the ETPCS volume.
After the workshop, there might be an opportunity to publish selected papers in a journal special issue.
| Submission of papers | 23 December |
| Notification | 25 January |
| Final versions due | 6 February |
| Workshop | 25 March |
|
|
The inaugural MSFP Workshop was held in July 2006, in Kuressaare, Estonia, a fine curtain-raiser for MPC and AMAST. It was organized by Conor McBride and Tarmo Uustalu, and featured invited talks from John Power and Andrzej Filinski. The proceedings were published in the British Computer Society's "Electronic Workshops in Computing" Series, available here.
Revised selected papers (with a full re-refereeing process) have appeared as a special issue of the Journal of Functional Programming Volume 19 Issue 3-4.
The second MSFP Workshop was held in July 2008, at Reykjavik University, Iceland as part of ICALP 2008. It was organized by Conor McBride and Venanzio Capretta, and featured invited talks from Andrej Bauer and Dan Piponi. The proceedings were published in Electronic Notes in Theoretical Computer Science, v. 229, n. 5, available here.
The third MSFP Workshop was held in September 2010, in Baltimore, Maryland as before ICFP 2010. It was organized by Venanzio Capretta and James Chapman, and featured invited talks from Martín Escardó and Amy Felty. The proceedings were published by ACM Press, available here.
Last modified 2 March 2012 by James Chapman