ICFP 2017
Proc. ACM Program. Lang., Vol. 1, No. ICFP
Powered by
Conference Publishing Consulting

Proc. ACM Program. Lang., Vol. 1, No. ICFP, September 3–9, 2017, Oxford, UK

ICFP 2017 – Advance Table of Contents

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial

Art and Education

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, and Robert Bruce Findler
(Northwestern University, USA)
Article Search Archive submitted (1992 MB)
Testing and Debugging Functional Reactive Programming
Ivan Perez and Henrik Nilsson
(University of Nottingham, UK)
Article Search
Lock-Step Simulation Is Child's Play (Experience Report)
Joachim Breitner and Chris Smith
(University of Pennsylvania, USA; Google, USA)
Preprint Archive submitted (1982 MB)
Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC
Benjamin Canou, Roberto Di Cosmo, and Grégoire Henry
(OCamlPro, n.n.; Inria, France; University of Paris Diderot, France)
Article Search

Functional Programming Techniques

Faster Coroutine Pipelines
Michael Spivey
(University of Oxford, UK)
Article Search Archive submitted (36 MB)
A Pretty But Not Greedy Printer (Functional Pearl)
Jean-Philippe Bernardy
(University of Gothenburg, Sweden)
Preprint
Generic Functional Parallel Algorithms: Scan and FFT
Conal Elliott
(Target, n.n.)
Article Search
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, and Matthew Might
(University of Utah, USA)
Article Search Archive submitted (60 MB)

Applications

Prototyping a Query Compiler using Coq (Experience Report)
Joshua Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and Jerome Simeon
(IBM Research, n.n.)
Preprint Archive submitted (1738 MB) Info
A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, and Benjamin Pierce
(University of Pennsylvania, USA)
Preprint Archive submitted (0 MB) Info
Symbolic Conditioning of Arrays in Probabilistic Programs
Praveen Narayanan and Chung-chieh Shan
(Indiana University, USA)
Article Search Archive submitted (15 MB)

Effects

Abstracting Definitional Interpreters (Functional Pearl)
David Darais, Nicholas Labich, Phúc C. Nguyễn, and David Van Horn
(University of Maryland, USA)
Article Search Info
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar
(Saarland University, Germany; University of Cambridge, UK; University of Oxford, UK; University of Edinburgh, UK; University of Ljubljana, Slovenia)
Article Search
Imperative Functional Programs That Explain Their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney
(University of Edinburgh, UK; University of Glasgow, UK)
Article Search Archive submitted (737 MB)
Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, and Hanne Riis Nielson
(DTU, Denmark)
Article Search

Low-Level and Systems Programming

Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente
(Sinusoidal Engineering, n.n.)
Preprint Archive submitted (729 MB) Info
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy
(Microsoft Research, USA; Inria, France; Microsoft Research, India; Massachusetts Institute of Technology, USA; Microsoft Research, UK)
Article Search
Verifying Efficient Function Calls in CakeML
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, and Yong Kiam Tan
(University of Kent, UK; Data61 at CSIRO, Australia; Australian National University, Australia; UNSW, Australia; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA)
Article Search
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland
(Drexel University, USA)
Article Search Archive submitted (2682 MB)

Foundations of Higher-Order Programming

Foundations of Strong Call by Need
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner
(LRI, France; University of Paris-Sud, France; University of Buenos Aires, Argentina; IRIF, France; University of Paris Diderot, France; CONICET, Argentina; Universidad Nacional de Quilmes, Argentina)
Article Search
A Relational Logic for Higher-Order Programs
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub
(IMDEA Software Institute, Spain; University at Buffalo, USA; SUNY, USA; MPI-SWS, Germany; École Polytechnique, n.n.)
Article Search Archive submitted (1 MB)
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Makoto Hamana
(Gunma University, Japan)
Article Search
No-Brainer CPS Conversion (Functional Pearl)
Milo Davis, William Meehan, and Olin Shivers
(Northeastern University, USA)
Article Search

Tools for Verification

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and NA Arvind
(Massachusetts Institute of Technology, USA)
Article Search Archive submitted (3633 MB)
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock
(University of Washington, USA; Stanford University, USA)
Article Search
Local Refinement Typing
Benjamin Cosman and Ranjit Jhala
(University of California at San Diego, USA)
Article Search

Program Construction

Compiling to Categories
Conal Elliott
(Target, n.n.)
Article Search
Visitors Unchained
François Pottier
(Inria, France)
Article Search
Staged Generic Programming
Jeremy Yallop
(University of Cambridge, UK)
Article Search

SRCs and DSLs

Super 8 Languages for Making Movies (Functional Pearl)
Leif Andersen, Stephen Chang, Asumu Takikawa, and Matthias Felleisen
(Northeastern University, USA; Igalia, n.n.)
Article Search Archive submitted (2473 MB)

Dependently Typed Programming

A Specification for Dependent Types in Haskell
Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg
(University of Pennsylvania, USA; Ecole Polytechnique, n.n.; University of Campinas, Brazil; Bryn Mawr College, USA)
Article Search Archive submitted (0 MB) Info
Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese
(KU Leuven, Belgium; Chalmers University of Technology, Sweden)
Article Search Archive submitted (449 MB)
Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, and Theo Winterhalter
(University of Gothenburg, Sweden; Chalmers University of Technology, Sweden; ENS Paris-Saclay, France)
Article Search
A Metaprogramming Framework for Formal Verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura
(Vienna University of Technology, Austria; KIT, Germany; University of Washington, USA; Carnegie Mellon University, USA; Microsoft Research, USA)
Article Search

Contracts and Sessions

Chaperone Contracts for Higher-Order Sessions
Hernán Melgratti and Luca Padovani
(University of Buenos Aires, Argentina; University of Turin, Italy)
Article Search Archive submitted (0 MB)
Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Christos Dimoulas, and Stephen Chong
(Harvard University, USA)
Article Search Archive submitted (322 MB) Info
Manifest Sharing with Session Types
Stephanie Balzer and Frank Pfenning
(Carnegie Mellon University, USA)
Article Search
Gradual Session Types
Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler
(Kyoto University, Japan; University of Freiburg, Germany; University of Lisbon, Portugal; University of Edinburgh, UK)
Article Search Info

Integrating Static and Dynamic Typing

Theorems for Free for Free: Parametricity, With and Without Types
Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler
(Northeastern University, USA; Indiana University, USA; University of Edinburgh, UK)
Article Search Archive submitted (631 MB)
On Polymorphic Gradual Typing
Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi
(Kyoto University, Japan; IBM Research, Japan)
Article Search Archive submitted (2450 MB)
Gradual Typing with Union and Intersection Types
Giuseppe Castagna and Victor Lanvin
(CNRS, France; University of Paris Diderot, France; ENS Cachan, France)
Preprint Archive submitted (0 MB)

Inference and Analysis

Constrained Type Families
J. Garrett Morris and Richard A. Eisenberg
(University of Edinburgh, UK; Bryn Mawr College, USA)
Article Search Archive submitted (0 MB)
Automating Sized-Type Inference for Complexity Analysis
Martin Avanzini and Ugo Dal Lago
(University of Innsbruck, Austria; University of Bologna, Italy; Inria, France)
Article Search
Inferring Scope through Syntactic Sugar
Justin Pombrio, Shriram Krishnamurthi, and Mitchell Wand
(Brown University, USA; Northeastern University, USA)
Article Search Archive submitted (1 MB)

proc time: 3.16