Hans-Wolfgang Loidl Ricardo Peña (Eds.) Trends 9 2 in Functional 8 7 S C Programming N L 13th International Symposium, TFP 2012 St. Andrews, UK, June 2012 Revised Selected Papers 123 Lecture Notes in Computer Science 7829 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA AlfredKobsa UniversityofCalifornia,Irvine,CA,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen TUDortmundUniversity,Germany MadhuSudan MicrosoftResearch,Cambridge,MA,USA DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum MaxPlanckInstituteforInformatics,Saarbruecken,Germany Hans-Wolfgang Loidl Ricardo Peña (Eds.) Trends in Functional Programming 13th International Symposium, TFP 2012 St. Andrews, UK, June 12-14, 2012 Revised Selected Papers 1 3 VolumeEditors Hans-WolfgangLoidl Heriot-WattUniversity SchoolofMathematicsandComputerSciences Edinburgh,EH144AS,UK E-mail:[email protected] RicardoPeña UniversidadComplutensedeMadrid FacultaddeInformática c/.ProfesorJoséGarcíaSantesmasess/n 28040Madrid,Spain E-mail:[email protected] ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-40446-7 e-ISBN978-3-642-40447-4 DOI10.1007/978-3-642-40447-4 SpringerHeidelbergNewYorkDordrechtLondon LibraryofCongressControlNumber:2013945452 CRSubjectClassification(1998):D.1.1,D.1.3,D.3,F.3,F.4,E.1 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©Springer-VerlagBerlinHeidelberg2013 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartof thematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation, broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionorinformation storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodology nowknownorhereafterdeveloped.Exemptedfromthislegalreservationarebriefexcerptsinconnection withreviewsorscholarlyanalysisormaterialsuppliedspecificallyforthepurposeofbeingenteredand executedonacomputersystem,forexclusiveusebythepurchaserofthework.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheCopyrightLawofthePublisher’slocation, inistcurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Permissionsforuse maybeobtainedthroughRightsLinkattheCopyrightClearanceCenter.Violationsareliabletoprosecution undertherespectiveCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Whiletheadviceandinformationinthisbookarebelievedtobetrueandaccurateatthedateofpublication, neithertheauthorsnortheeditorsnorthepublishercanacceptanylegalresponsibilityforanyerrorsor omissionsthatmaybemade.Thepublishermakesnowarranty,expressorimplied,withrespecttothe materialcontainedherein. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface With the 13th Symposium on Trends in Functional Programming (TFP 2012), held in St. Andrews, Scotland, the TFP series returned to its origins in Scot- land.TFPistheheirofthesuccessfulseriesofScottishFunctionalProgramming Workshops, which randuring 1999–2002,organizedat severalScottish universi- ties.Reflectingtheincreasinglyinternationalaudienceoftheseevents,from2003 onwards these became the Symposium on Trends in Functional Programming, andwereheldinEdinburgh(2003),inMunich(2004),inTallinn(2005),inNot- tingham (2006), in New York (2007), in Nijmegen (2008), in Komarno (2009), in Oklahoma (2010), and in Madrid (2011). In June 2012 TFP was the main event of a week of functional programming extravaganzaatthe Universityof St. Andrews, attended by more than80 regis- teredparticipants.Co-locatedeventsweretheInternationalWorkshoponTrends in Functional Programming in Education (TFPIE 2012), the Workshop on 70 YearsofLambdaCalculus,anErlangFactoryLite, andatechnicalworkshopon Patterns for Multicores (ParaPhrase/RELEASEprojects). In total, TFP 2012 received 49 submissions for the draft proceedings. After a screening process, 41 of these papers were accepted for the draft proceedings and for presentation at the symposium. The screening process was performed by a subset of the Program Committee and aimed to ensure that all contribu- tions are in scope andcontain relevantinformationfor the TFP audience. After TFP 2012, all authors of presentations were invited to submit full papers to a formal refereeing process, the result of which is presented in these proceedings. The papers in these proceedings have been judged by members of the Program Committee on their contribution to the research area with appropriate criteria applied to each category of paper. For each paper at least three referee reports were produced. Based on these reports, the international Program Committee selectedthe paperspresentedinthese proceedings.Intotal,36papersweresub- mitted for the formal refereeing process and 18 papers were accepted. Additionally to these refereed papers, these proceedings feature a paper by a high-profile member of the research community, David A. Turner, Professor Emeritus at Middlesex University and at the University of Kent. Prof. Turner is the inventor of such influential functional languages as Miranda, KRC and SASL.Prof.Turnerpresentedaninvitedtalkon“TheHistoryofLazyFunctional ProgrammingLanguages”atthesymposiumandgraciouslyagreedtosummarize his insights into the development of functional languages in the first paper in these proceedings. We would like to thank Prof. Turner for his contribution to TFP, which was most appreciated by the attendees. TFPtraditionallypaysspecialattentiontoresearchstudents,acknowledging that students are almost by definition part of new subject trends. A student paper is one for which the authors state that the paper is mainly the work of VI Preface students, the students are listed as first authors, and a student would present the paper.Thesepapersalsoreceiveanextraroundoffeedbackby the Program Committee before they are submitted to the standard review process for formal publication. Inthis way,students canimprovetheir papersbefore they compete within a full formal refereeing process. In 2012, 23 of the 49 papers submitted for the draft proceedings were student papers. Acknowledgingthe contributions by student papers, the TFP Program Committee awards a prize for the best student paper each year. We are delighted to announce that for TFP 2012 the TFP prize for the best student paper was awardedto: Luminous Fennell and Peter Thiemann for the paper “The Blame Theorem for a Linear Lambda Calculus with Type Dynamic.” Weareproudtoannouncethatthisyear,forthefirsttime,anEAPLSBestPaper Awardelevatesoneofthepapersintheseproceedingsasmakinganoutstanding contribution to the field. Based on a short-list of papers provided by the TFP 2012 Program Committee, the EAPLS board made the final selection for this award. We are therefore proud to announce that the EAPLS prize for the best paper of TFP 2012 was awardedto: Josef Svenningsson and Emil Axelsson for the paper “Combining Deep and Shallow Embedding for EDSL.” Finally, we are grateful for the sponsorship by Erlang Solutions Ltd. and the Scottish Informatics and Computer Science Alliance (SICSA). The TFP Best Student Paper award is funded by the TFP series. The EAPLS Best Paper Awardis funded by the EuropeanAssociationfor ProgrammingLanguagesand Systems. March 2013 Hans-Wolfgang Loidl Ricardo Pen˜a Organization Committees Program Chair Hans-Wolfgang Loidl Heriot-Watt University, U.K. Symposium Chair Ricardo Pena Universidad Complutense de Madrid, Spain General Chair Kevin Hammond University of St. Andrews, U.K. Program Committee Peter Achten Radboud University Nijmegen, The Netherlands Jost Berthold University of Copenhagen, Denmark Edwin Brady University of St. Andrews, U.K. Matthias Blume Google, U.S.A. Clemens Grelck University of Amsterdam, The Netherlands Kevin Hammond University of St. Andrews, U.K. Graham Hutton University of Nottingham, U.K. Patricia Johann University of Strathclyde, U.K. Hans-Wolfgang Loidl (PC Chair) Heriot-Watt University, U.K. Jay McCarthy Brigham Young University, Utah, U.S.A. Rex Page University of Oklahoma, U.S.A. Ricardo Pen˜a Complutense University of Madrid, Spain Kostis Sagonas Uppsala University, Sweden Manuel Serrano INRIA Sophia Antipolis, France Mary Sheeran Chalmers, Sweden Nikhil Swamy Microsoft Research, Redmond, U.S.A. Phil Trinder Heriot-Watt University, U.K. Wim A. Vanderbauwhede University of Glasgow, U.K. Marko van Eekelen Radboud University Nijmegen, The Netherlands VIII Organization David Van Horn Northeastern University, U.S.A. Malcolm Wallace Standard Chartered, U.K. Vikt´oria Zs´ok Eo¨tvo¨s Lora´nd University, Hungary Local Organization Kevin Hammond Edwin Brady Vladimir Janjic Table of Contents Invited Talk Some History of Functional Programming Languages (Invited Talk) .... 1 D.A. Turner Contributions Combining Deep and Shallow Embedding for EDSL .................. 21 Josef Svenningsson and Emil Axelsson The Blame Theorem for a Linear Lambda Calculus with Type Dynamic........................................................ 37 Luminous Fennell and Peter Thiemann Higher-Order Size Checking without Subtyping ...................... 53 Attila G´obi, Olha Shkaravska, and Marko van Eekelen Well-Typed Islands Parse Faster ................................... 69 Erik Silkensen and Jeremy Siek Higher-Order Strictness Typing.................................... 85 Sjaak Smetsers and Marko van Eekelen Call-by-Value Semantics for Mutually Recursive First-Class Modules ... 101 Judith Rohloff and Florian Lorenzen The Design of a Practical Proof Checker for a Lazy Functional Language ....................................................... 117 Adam Procter, William L. Harrison, and Aaron Stump Towards a Framework for Building Formally Verified Supercompilers in Coq.......................................................... 133 Dimitur Nikolaev Krustev Matching Problem for Regular Expressions with Variables............. 149 Vladimir Komendantsky OCaml-Java: OCaml on the JVM .................................. 167 Xavier Clerc The Functional Programming Language R and the Paradigm of Dynamic Scientific Programming (Position Paper) ................. 182 Baltasar Tranco´n y Widemann, Carl Friedrich Bolz, and Clemens Grelck X Table of Contents Lingua Franca of Functional Programming (FP) ..................... 198 Peter Kourzanov and Henk Sips Haskell Gets Argumentative....................................... 215 Bas van Gijzel and Henrik Nilsson Repeating History: Execution Replay for Parallel Haskell Programs .... 231 Henrique Ferreiro, Vladimir Janjic, Laura M. Castro, and Kevin Hammond Supervised Workpools for Reliable Massively Parallel Computing ...... 247 Robert Stewart, Phil Trinder, and Patrick Maier RELEASE: A High-Level Paradigm for Reliable Large-Scale Server Software (Project Paper).......................................... 263 Olivier Boudeville, Francesco Cesarini, Natalia Chechina, Kenneth Lundin, Nikolaos Papaspyrou, Konstantinos Sagonas, Simon Thompson, Phil Trinder, and Ulf Wiger Towards Heterogeneous Computing without Heterogeneous Programming.................................................... 279 Miguel Diogo and Clemens Grelck On Using Erlang for Parallelization: Experience from Parallelizing Dialyzer ........................................................ 295 Stavros Aronis and Konstantinos Sagonas Author Index.................................................. 311