PPDP 2014

PPDP 2014

I attended PPDP 2014, in Canterbury, England a few weeks ago.  Some notes about papers of interest there:

• Stefan Mehner, Daniel Seidel, Lutz Straßburger and Janis Voigtländer.  "Parametricity and Proving Free Theorems for Functional-Logic Languages".  Translates core Curry programs to a functional language with a built-in (not necessarily finite) set type.  As I understand it, this should also apply to pure (typed) logic programming as well, but not necessarily to higher-order logic programming.
• Danko Ilik. "Proofs in Continuation-Passing Style: normalization of Gödel's System T  extended with sums and delimited control operators."  One of several "distilled tutorials" at PPDP.  Gives an overview of double-negation proof technique for normalization by evaluation in the presence of recursion and sums, accompanied by proofs in Agda (and exercises).
• Hugo Pacheco, Tao Zan and Zhenjiang Hu. "BiFluX: A Bidirectional Functional Update Language for XML."  Develops a bidirectional language for XML based on an update language I worked on in an ICFP 2008 paper.  Interestingly, they extend the language with features that talk about both the source and view at the same time, and how they are to be matched up.  Also interestingly, they do not talk about how to translate view updates to source updates; this might be an area for further work.
• Ulrich Schöpp. "Organising Low-Level Programs using Higher Types." This paper looks at compilation from a high-level language with linear features to LLVM.  It builds on a line of work by Schopp and others using linear type systems for resource-bounded programming (e.g. to capture low complexity classes).  One really nice thing about this is that one gets a fair amount of denotational semantics and reasoning principles about the low0level programs for free.  There seem to be interesting (unexplored in the paper) connections to previous work on typed low-level languages (my abortive work with Greg Morrisett on Linear TAL, and work by Vanderwaart and Crary)
• Tom Schrijvers, Nicolas Wu, Benoit Desouter and Bart Demoen. "Heuristics entwined with handlers combined."  This paper applies ideas from the recent line of work on handlers and algebraic effects (see e.g. Kammar et al. and citations) to Prolog, to allow interpreting the same (pure) Prolog program using different proof search strategies (e.g. breadth-first or iterative deepening, rather than Prolog's built-in depth first search).  I need to dig deeper, but this seems promising as a way of generalizing away from Prolog's fixed search strategy and perhaps allowing for principled programmability of search behaviors orthogonally to specific programs.