ICFP 2013

42 papers

1. A nanopass framework for commercial compiler development · Andrew W. Keep, R. Kent Dybvig
2. A practical theory of language-integrated query · James Cheney, Sam Lindley, Philip Wadler
3. A short cut to parallelization theorems · Akimasa Morihata
4. Automatic SIMD vectorization for Haskell · Leaf Petersen, Dominic A. Orchard, Neal Glew
5. C-SHORe: a collapsible approach to higher-order verification · Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Olivier Serre
6. Calculating threesomes, with blame · Ronald Garcia
7. Complete and easy bidirectional typechecking for higher-rank polymorphism · Jana Dunfield, Neelakantan R. Krishnaswami
8. Computer science as a school subject · Simon L. Peyton Jones
9. Correctness of an STM Haskell implementation · Manfred Schmidt-Schauß, David Sabel
10. Efficient divide-and-conquer parsing of practical context-free languages · Jean-Philippe Bernardy, Koen Claessen
11. Experience report: applying random testing to a base type environment · Vincent St-Amour, Neil Toronto
12. Experience report: functional programming of mHealth applications · Chris Petersen, Matthias Görges, Dustin T. Dunsmuir, John Mark Ansermino, Guy Albert Dumont
13. Exploiting vector instructions with generalized stream fusio · Geoffrey Mainland, Roman Leshchinskiy, Simon L. Peyton Jones
14. Fun with semirings: a functional pearl on the abuse of linear algebra · Stephen Dolan
15. Functional geometry and the Traité de Lutherie: functional pearl · Harry G. Mairson
16. Functional reactive programming with liveness guarantees · Alan Jeffrey
17. Handlers in action · Ohad Kammar, Sam Lindley, Nicolas Oury
18. Higher-order functional reactive programming without spacetime leaks · Neelakantan R. Krishnaswami
19. Hoare-style reasoning with (algebraic) continuations · Germán Andrés Delbianco, Aleksandar Nanevski
20. Interactive programming with dependent types · Ulf Norell
21. Modular and automated type-soundness verification for language extensions · Florian Lorenzen, Sebastian Erdweg
22. Modular monadic meta-theory · Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira
23. Mtac: a monad for typed tactic programming in Coq · Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
24. Optimising purely functional GPU programs · Trevor L. McDonell, Manuel M. T. Chakravarty, Gabriele Keller, Ben Lippmeier
25. Optimizing abstract abstract machines · Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn
26. Productive coprogramming with guarded recursion · Robert Atkey, Conor McBride
27. Programming and reasoning with algebraic effects and dependent types · Edwin C. Brady
28. Programming with permissions in Mezzo · François Pottier, Jonathan Protzenko
29. Simple and compositional reification of monadic embedded languages · Josef Svenningsson, Bo Joel Svensson
30. Structural recursion for querying ordered graphs · Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano
31. System FC with explicit kind equality · Stephanie Weirich, Justin Hsu, Richard A. Eisenberg
32. Testing noninterference, quickly · Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim + 1 more
33. The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier · Adam Chlipala
34. The constrained-monad problem · Neil Sculthorpe, Jan Bracker, George Giorgidze, Andy Gill
35. Type-theory in color · Jean-Philippe Bernardy, Guilhem Moulin
36. Typed syntactic meta-programming · Dominique Devriese, Frank Piessens
37. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency · Aaron Turon, Derek Dreyer, Lars Birkedal
38. Unifying structured recursion schemes · Ralf Hinze, Nicolas Wu, Jeremy Gibbons
39. Using circular programs for higher-order syntax: functional pearl · Emil Axelsson, Koen Claessen
40. Verified decision procedures for MSO on words based on derivatives of regular expressions · Dmitriy Traytel, Tobias Nipkow
41. Weak optimality, and the meaning of sharing · Thibaut Balabonski
42. Wellfounded recursion with copatterns: a unified approach to termination and productivity · Andreas Abel, Brigitte Pientka