ICFP 2011
40 papers
- A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences
- A kripke logical relation for effect-based program transformations
- A semantic model for graphical user interfaces
- An efficient non-moving garbage collector for functional languages
- An equivalence-preserving CPS translation via multi-language semantics
- Balanced trees inhabiting functional parallel programming
- Binders unbound
- Characteristic formulae for the verification of imperative programs
- Deriving an efficient FPGA implementation of a low density parity check forward error corrector
- Forest: a language and toolkit for programming with filestores
- Frenetic: a network programming language
- Functional modelling of musical harmony: an experience report
- Functional programming through deep time: modeling the first complex ecosystems on earth
- Generalising and dualising the third list-homomorphism theorem: functional pearl
- Geometry of synthesis iv: compiling affine recursion into static hardware
- How to make ad hoc proof automation less ad hoc
- Implicit self-adjusting computation for purely functional programs
- Incremental updates for efficient bidirectional transformations
- Just do it: simple monadic equational reasoning
- Lightweight monadic programming in ML
- Linearity and PCF: a semantic insight!
- Making standard ML a practical database programming language
- Modular rollback through control logging: a pair of twin functional pearls
- Modular verification of preemptive OS kernels
- Monads, zippers and views: virtualizing the monad stack
- Nameless, painless
- On the bright side of type classes: instance arguments in Agda
- Parametric polymorphism and semantic subtyping: the logical connection
- Parsing with derivatives: a functional pearl
- Programming assurance cases in Agda
- Proving the unique fixed-point principle correct: an adventure with category theory
- Pushdown flow analysis of first-class control
- Recursion principles for syntax with bindings and substitution
- Secure distributed programming with value-dependent types
- Set-theoretic foundation of parametric polymorphism and subtyping
- Subtyping delimited continuations
- Temporal higher-order contracts
- Towards a comprehensive theory of monadic effects
- Typed self-interpretation by pattern matching
- 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