| Invited Talks |
| Beluga: Programming with Dependent Types, Contextual Data, and Contexts / Brigitte Pientka |
| Using Static Analysis to Detect Type Errors and Concurrency Defects in Erlang Programs / Konstantinos Sagonas |
| Solving Constraint Satisfaction Problems with SAT Technology / Naoyuki Tamura ; Tomoya Tanjo ; Mutsunori Banbara |
| Refereed Papers |
| Types |
| A Church-Style Intermediate Language for MLF / Didier Rémy ; Boris Yakobowski |
| IIσDependent Types without the Sugar / Thorsten Altenkirch ; Nils Anders Danielsson ; Andres Löh ; Nicolas Oury |
| Haskell Type Constraints Unleashed / Dominic Orchard ; Tom Schrijvers |
| Program Analysis and Transformation |
| A Functional Framework for Result Checking / Gilles Barthe ; Pablo Buiras ; César Kunz |
| Tag-Free Combinatory for Binding-Time Polymorphic Program Generation / Peter Thiemann ; Martin Sulzmann |
| Code Generation via Higher-Order Rewrite Systems / Florian Haftmann ; Tobias Nipkow |
| Foundations |
| A Complete Axiomatization of Strict Equality / Javier Álvez ; Francisco J. López-Fraguas |
| Standardization and Böhm Trees for Λμ-Calculus / Alexis Saurin |
| An Integrated Distance for Atoms / Vicent Estruch ; César Ferri ; José Hernández-Orallo ; M. José Ramírez-Quintana |
| Logic Programming |
| A Pearl on SAT Solving in Prolog / Jacob M. Howe ; Andy King |
| Automatically Generating Counterexamples to Naive Free Theorems / Daniel Seidel ; Janis Voigtländer |
| Applying Constraint Logic Programming to SQL Test Case Generation / Rafael Caballero ; Yolanda García-Ruiz ; Fernando Sáenz-Pérez |
| Evaluation and Normalization |
| Internal Normalization, Compilation and Decompilation for System Fβη / Stefano Berardi ; Makoto Tatsuta |
| Towards Normalization by Evaluation for the βη-Calculus of Constructions / Andreas Abel |
| Defunctionalized Interpreters for Call-by-Need Evaluation / Olivier Danvy ; Kevin Millikin ; Johan Munk ; Ian Zerny |
| Term Rewriting |
| Complexity Analysis by Graph Rewriting / Martin Avanzini ; Georg Moser |
| Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus / Jeroen Ketema ; Jakob Grue Simonsen |
| Proving Injectivity of Functions via Program Inversion in Term Rewriting / Naoki Nishida ; Masahiko Sakai |
| Parallelism and Control |
| Delimited Control in OCaml, Abstractly and Concretely: System Description / Oleg Kiselyov |
| Automatic Parallelization of Recursive Functions Using Quantifier Elimination / Akimasa Morihata ; Kiminori Matsuzaki |
| A Skeleton for Distributed Work Pools in Eden / Mischa Dieterle ; Jost Berthold ; Rita Loogen |
| Author Index |
| Invited Talks |
| Beluga: Programming with Dependent Types, Contextual Data, and Contexts / Brigitte Pientka |
| Using Static Analysis to Detect Type Errors and Concurrency Defects in Erlang Programs / Konstantinos Sagonas |
ＥＢ
