[Agda] [TYPES/announce] ICFP 2013 Call for Participation

Tarmo Uustalu tarmo at cs.ioc.ee
Sat Aug 17 17:13:12 CEST 2013

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

-------------- next part --------------



  18th ACM SIGPLAN International Conference on Functional Programming

  ICFP 2013

  Boston, MA, USA, 25-27 September 2013

  Affiliated events 22-24 September, 28 September 2013



ICFP is a forum for researchers and practitioners to hear about the
latest developments in the art and science of functional
programming. The conference cover the entire spectrum of work, from
theory to practice.

The keynote speakers of ICFP 2013 are Ulf Norell on dependently typed
programming and Simon Peyton Jones on computer science as a school

The 40 contributed papers on all aspects of functional programming
were selected by the program committee from 133 submissions.

Affiliated to ICFP 2013 are:

ACM SIGPLAN Commercial Users of Functional Programming Workshop
ACM SIGPLAN Workshop on Dependently Typed Programming
ACM SIGPLAN Workshop on Functional Art, Music, Modeling and Design
ACM SIGPLAN Workshop on Functional High-Performance Computing
ACM SIGPLAN Erlang Workshop
ACM SIGPLAN Functional Programming in Domain-Specific Languages Workshop
ACM SIGPLAN Workshop on Generic Programming
ACM SIGPLAN Haskell Symposium
ACM SIGPLAN Haskell Implementors Workshop
ACM SIGPLAN Workshop on Higher-Order Programming with Effects
ACM SIGPLAN International Workshop on Logical Frameworks and
     Meta-Languages: Theory and Practice
ACM SIGPLAN Workshop on ML
ACM SIGPLAN OCaml Workshop


The conference will take place at Hilton Boston Logan Airport Hotel.


Registration is available at


*Note that early registration ends 22 August 2013.*


Wednesday, 25 September

9-10 Keynote 1

Interactive Programming with Dependent Types
Ulf Norell (Chalmers University of Technology)

10-1020 Break

1020-1100 Session 1: Verification with Grammars and Automata

Verified Decision Procedures for MSO on Words Based on Derivatives of
Regular Expressions [Functional Pearl]
Dmitriy Traytel and Tobias Nipkow
Christopher Broadbent, Arnaud Carayol, Matthew Hague and Olivier Serre

1100-1130 Break

1130-1230 Session 2

Automatic SIMD Vectorization for Haskell
Leaf Petersen, Dominic Orchard and Neal Glew
Exploiting Vector Instructions with Generalized Stream Fusion
Geoffrey Mainland, Roman Leshchinskiy and Simon Peyton Jones
Optimising Purely Functional GPU Programs
Trevor L. McDonell, Manuel Chakravarty, Gabriele Keller and Ben Lippmeier

1230-14 Lunch

14-15 Session 3: Dependent Types

Type-Theory In Color
Jean-Philippe Bernardy and Guilhem Moulin
Typed Syntactic Meta-programming
Dominique Devriese and Frank Piessens
Mtac: A Monad for Typed Tactic Programming in Coq
Beta Ziliani, Derek Dreyer, Neelakantan Krishnaswami, Aleksandar Nanevski
and Viktor Vafeiadis

15-1530 Break

1530-1630 Session 4: Fun in the Afternoon

Fun with Semirings [Functional Pearl]
Stephen Dolan
Efficient Divide-and-Conquer Parsing of Practical Context-Free Languages
Jean-Philippe Bernardy and Koen Claessen
Functional Geometry and the "Trait? de Lutherie" [Functional Pearl]
Harry Mairson

1630-17 Break

17-1740 Session 5: Handling Effects

Programming and Reasoning with Algebraic Effects and Dependent Types
Edwin Brady
Handlers in Action
Ohad Kammar, Sam Lindley and Nicolas Oury

1740-18 Program Chair's Report

Thursday, 26 September

9-10 Keynote 2

Computer Science as a School Subject
Simon Peyton Jones (Microsoft Research, Cambridge, UK)

10-1020 Break

1020-11 Session 6: Concurrency

Correctness of an STM Haskell Implementation
Manfred Schmidt-Schauss and David Sabel
Programming with Permissions in Mezzo
Francois Pottier and Jonathan Protzenko

11-1130 Break

1130-1230 Session 7: (Co-)Recursion

Wellfounded Recursion with Copatterns
Andreas Abel and Brigitte Pientka
Productive Coprogramming with Guarded Recursion
Robert Atkey and Conor McBride
Unifying Structured Recursion Schemes
Ralf Hinze, Nicolas Wu and Jeremy Gibbons

1230-14 Lunch

14-15 Session 8: Functional Reactive Programming (and More)

Higher-Order Functional Reactive Programming without Spacetime Leaks
Neelakantan Krishnaswami
Functional Reactive Programming with Liveness Guarantees
Alan Jeffrey
A Short Cut to Parallelization Theorems
Akimasa Morihata

15-1530 Break

1530-1630 Session 9: Lambda-Calculus

Using Circular Programs for Higher-Order Syntax [Functional Pearl]
Emil Axelsson and Koen Claessen
Weak Optimality, and the Meaning of Sharing
Thibaut Balabonski
System FC with Explicit Kind Equality
Stephanie Weirich, Justin Hsu and Richard A. Eisenberg

1630-17 Break

17-1740 Programming Contest Co-Chairs' Report and Awards
1740-18 ICFP 2003 Most Influential Paper Award

Friday, 27 September

9-10 Session 10: Monads

The Constrained-Monad Problem
Neil Sculthorpe, Jan Bracker, George Giorgidze and Andy Gill
Simple and Compositional Reification of Monadic Embedded Languages
[Functional Pearl]
Josef Svenningsson and Bo Joel Svensson
Structural Recursion for Querying Ordered Graphs
Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato and Keisuke 

10-1020 Break

1020-11 Session 11: Modular Meta-Theory
Modular Monadic Meta-Theory
Benjamin Delaware, Steven Keuchel, Tom Schrijvers and Bruno Oliveira
Modular and Automated Type-Soundness Verification for Language Extensions
Florian Lorenzen and Sebastian Erdweg

11-1130 Break

1130-1230 Session 12: Experience Reports (Chair: John Launchbury)
A Nanopass Framework for Commercial Compiler Development [Experience 
Andrew Keep and R Kent Dybvig
Applying Random Testing to a Base Type Environment [Experience Report]
Vincent St-Amour and Neil Toronto
Functional Programming of mHealth Applications [Experience Report]
Christian Petersen, Matthias Gorges, Dustin Dunsmuir, Mark Ansermino and
Guy Dumont

1230-14 Lunch

14-15 Session 13: Program Logics
Hoare-Style Reasoning with (Algebraic) Continuations
Germ?n Andr?s Delbianco and Aleksandar Nanevski
Unifying Refinement and Hoare-Style Reasoning in a Logic for
Higher-Order Concurrency
Aaron Turon, Derek Dreyer and Lars Birkedal
The Bedrock Structured Programming System
Adam Chlipala

15-1530 Break

1530-1630 Session 14: Language Design
A Practical Theory of Language-Integrated Query
James Cheney, Sam Lindley and Philip Wadler
Calculating Threesomes, with Blame
Ronald Garcia
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
Joshua Dunfield and Neelakantan R. Krishnaswami

1630-17 Break

17-1740 Session 15: Analysis and Optimization
Optimizing Abstract Abstract Machines
J. Ian Johnson, Nicholas Labich, Matthew Might and David Van Horn
Testing Noninterference, Quickly
Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky,
Dimitrios Vytiniotis, Arthur Azevedo de Amorim and Leonidas Lampropoulos

1740-18 ICFP 2014 Advert & Closing

   Greg Morrisett, Harvard University

   Tarmo Uustalu, Institute of Cybernetics, Tallinn

   Thorsten Altenkirch, University of Nottingham
   Olaf Chitil, University of Kent
   Silvia Ghilezan, University of Novi Sad
   Michael Hanus, Christian-Albrechts-Universit?t zu Kiel
   Fritz Henglein, University of Copenhagen

   Mauro Jaskelioff, Universidad Nacional de Rosario
   Alan Jeffrey, Alcatel-Lucent Bell Labs
   Shin-ya Katsumata, Kyoto University
   Shriram Krishnamurthi	Brown University
   John Launchbury, Galois

   Ryan Newton, Indiana University
   Sungwoo Park, Pohang University of Science and Technology
   Sam Staton, University of Cambridge
   Nikhil Swamy, Microsoft Research, Redmond, WA
   Dimitrios Vytiniotis, Microsoft Research, Cambridge

More information about the Agda mailing list