16. ICFP 2011: Tokyo, Japan

Keynote

• Andrzej Filinski:
  Towards a comprehensive theory of monadic effects. 1
  

Monads

• Jeremy Gibbons, Ralf Hinze:
  Just do it: simple monadic equational reasoning. 2-14
  
• Nikhil Swamy, Nataliya Guts, Daan Leijen, Michael Hicks:
  Lightweight monadic programming in ML. 15-27
  
• Emily G. Mitchell:
  Functional programming through deep time: modeling the first complex ecosystems on earth. 28-31
  

Monads and control

• Tom Schrijvers, Bruno C. d. S. Oliveira:
  Monads, zippers and views: virtualizing the monad stack. 32-44
  
• Neelakantan R. Krishnaswami, Nick Benton:
  A semantic model for graphical user interfaces. 45-57
  
• Olin Shivers, Aaron Joseph Turon:
  Modular rollback through control logging: a pair of twin functional pearls. 58-68
  

Continuations

• Dimitrios Vardoulakis, Olin Shivers:
  Pushdown flow analysis of first-class control. 69-80
  
• Marek Materzok, Dariusz Biernacki:
  Subtyping delimited continuations. 81-93
  

Parametric polymorphism and subtyping

• Giuseppe Castagna, Zhiwu Xu:
  Set-theoretic foundation of parametric polymorphism and subtyping. 94-106
  
• Nils Gesbert, Pierre Genevès, Nabil Layaïda:
  Parametric polymorphism and semantic subtyping: the logical connection. 107-116
  

Functional computation

• Akimasa Morihata, Kiminori Matsuzaki:
  Balanced trees inhabiting functional parallel programming. 117-128
  
• Yan Chen, Joshua Dunfield, Matthew A. Hammer, Umut A. Acar:
  Implicit self-adjusting computation for purely functional programs. 129-141
  

Keynote

• Makoto Takeyama:
  Programming assurance cases in Agda. 142
  

Proof assistance

• Dominique Devriese, Frank Piessens:
  On the bright side of type classes: instance arguments in Agda. 143-155
  
• José Pedro Magalhães, Bas de Haas:
  Functional modelling of musical harmony: an experience report. 156-162
  
• Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer:
  How to make ad hoc proof automation less ad hoc. 163-175
  

Implementation

• Tim Disney, Cormac Flanagan, Jay McCarthy:
  Temporal higher-order contracts. 176-188
  
• Matthew Might, David Darais, Daniel Spiewak:
  Parsing with derivatives: a functional pearl. 189-195
  
• Katsuhiro Ueno, Atsushi Ohori, Toshiaki Otomo:
  An efficient non-moving garbage collector for functional languages. 196-208
  

Derivation and synthesis

• Andy Gill, Andrew Farmer:
  Deriving an efficient FPGA implementation of a low density parity check forward error corrector. 209-220
  
• Dan R. Ghica, Alex Smith, Satnam Singh:
  Geometry of synthesis iv: compiling affine recursion into static hardware. 221-233
  

Types

• Ki Yung Ahn, Tim Sheard:
  A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences. 234-246
  
• C. Barry Jay, Jens Palsberg:
  Typed self-interpretation by pattern matching. 247-258
  
• Frédéric Chyzak, Alexis Darrasse:
  Using camlp4 for presenting dynamic mathematics on the web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the web. 259-265
  

Distributed programming

• Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang:
  Secure distributed programming with value-dependent types. 266-278
  
• Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, David Walker:
  Frenetic: a network programming language. 279-291
  

Applications

• Kathleen Fisher, Nate Foster, David Walker, Kenny Qili Zhu:
  Forest: a language and toolkit for programming with filestores. 292-306
  
• Atsushi Ohori, Katsuhiro Ueno:
  Making standard ML a practical database programming language. 307-319
  

Naming

• Nicolas Pouillard:
  Nameless, painless. 320-332
  
• Stephanie Weirich, Brent A. Yorgey, Tim Sheard:
  Binders unbound. 333-345
  
• Andrei Popescu, Elsa L. Gunter:
  Recursion principles for syntax with bindings and substitution. 346-358
  

Semantics

• Ralf Hinze, Daniel W. H. James:
  Proving the unique fixed-point principle correct: an adventure with category theory. 359-371
  
• Marco Gaboardi, Luca Paolini, Mauro Piccolo:
  Linearity and PCF: a semantic insight! 372-384
  

Program transformation

• Shin-Cheng Mu, Akimasa Morihata:
  Generalising and dualising the third list-homomorphism theorem: functional pearl. 385-391
  
• Meng Wang, Jeremy Gibbons, Nicolas Wu:
  Incremental updates for efficient bidirectional transformations. 392-403
  

Imperative programming

• Alexey Gotsman, Hongseok Yang:
  Modular verification of preemptive OS kernels. 404-417
  
• Arthur Charguéraud:
  Characteristic formulae for the verification of imperative programs. 418-430
  

Correctness

• Amal Ahmed, Matthias Blume:
  An equivalence-preserving CPS translation via multi-language semantics. 431-444
  
• Jacob Thamsborg, Lars Birkedal:
  A kripke logical relation for effect-based program transformations. 445-456
  

Last update Fri May 24 02:54:45 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page