Published: 11th February 2012|
|Preface James Chapman and Paul Blain Levy|
|Invited Presentation: Fibred data types Neil Ghani||1|
|Invited Presentation: Dependently typed continuation monads as models in logic Danko Ilik||2|
|Parametric Compositional Data Types Patrick Bahr and Tom Hvitved||3|
|Step-Indexed Normalization for a Language with General Recursion Chris Casinghino, Vilhelm Sjöberg and Stephanie Weirich||25|
|An Investigation of the Laws of Traversals Mauro Jaskelioff and Ondrej Rypacek||40|
|A Formal Comparison of Approaches to Datatype-Generic Programming José Pedro Magalhães and Andres Löh||50|
|Evaluation strategies for monadic computations Tomas Petricek||68|
|Tracing monadic computations and representing effects Maciej Piróg and Jeremy Gibbons||90|
|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||112|
|From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine Wouter Swierstra||163|
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