drup / icfp2017-papers Goto Github PK

Links to conditionally¹ accepted papers for the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017). Pull requests welcome!

(Similar pages are available for older ICFP (2012, 2013, 2014, 2015, 2016), POPL (2013, 2014, 2015, 2016), and PLDI 2014.)

Note: if you are editing this repository, please remember to use the Markdown syntax for hard line breaks, namely two spaces at the end of the line.

¹: This year is the first year where ICFP uses a journal publication model, with open-access proceedings published in PACM. A two-phase reviewing process is used, so most papers are conditionally accepted with a list of mandatory revisions for authors to perform.

A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, Benjamin C. Pierce
(paper (extended version))

A Relational Logic for Higher-Order Programs
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
(preprint from arXiv)

A Specification for Dependently-Typed Haskell
Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, Richard Eisenberg
(draft)

Automating Sized-Type Inference for Complexity Analysis
Martin Avanzini, Ugo Dal Lago
(preprint from arXiv)

Better Living Through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland

Chaperone Contracts for Higher-Order Sessions
Hernan Melgratti, Luca Padovani
(slides)

Compiling to categories
Conal Elliott
(preprint, website)

Constrained Type Families
J. Garrett Morris, Richard Eisenberg
(preprint)

Definitional Abstract Interpreters for Higher-Order Programming Languages
David Darais, Nicholas Labich, Phúc Nguyễn, David Van Horn
(paper as a webpage!)

Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson
(implementation)

Experience Report: Prototyping a Query Compiler Using Coq
Joshua Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jerome Simeon

Faster Coroutine Pipelines
Mike Spivey
(preprint)

Foundations of Strong Call by Need
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, Delia Kesner

Functional Pearl: A Unified Approach to Solving Seven Programming Problems
William E. Byrd, Michael Ballantyne, Greg Rosenblatt, Matthew Might

Functional Pearl: a pretty but not greedy printer
Jean-Philippe Bernardy
(preprint, github repo)

Generic functional parallel algorithms: Scan and FFT
Conal Elliott
(preprint, website)

Gradual Session Types
Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, Philip Wadler
(slides)

Gradual Typing with Union and Intersection Types
Giuseppe Castagna, Victor Lanvin
(preprint)

Herbarium Racketensis: A Stroll Through the Woods (Functional Pearl)
Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Robby Findler

How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation
Makoto Hamana

Imperative functional programs that explain their work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney
(preprint from arXiv, companion code)

Inferring Scope through Syntactic Sugar
Justin Pombrio, Shriram Krishnamurthi, Mitchell Wand
(paper, extended version, material)

Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind
(website, no preprint yet)

Local Refinement Typing
Benjamin Cosman, Ranjit Jhala
(preprint from arXiv)

Lock-step simulation is child’s play
Joachim Breitner, Chris Smith
(preprint from arXiv)

Manifest Sharing with Session Types
Stephanie Balzer, Frank Pfenning
(preprint)

Metaprogramming with Dependent Type Theory
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura

No-brainer CPS Conversion
Milo Davis, William Meehan, Olin Shivers

Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, Theo Winterhalter
(preprint)

On Polymorphic Gradual Typing
Yuu Igarashi, Taro Sekiyama, Atsushi Igarashi

On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
(preprint from arXiv)

Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, Dominique Devriese
(draft)

Persistence for the masses: RRB-Vectors in a systems language
Juan Pedro Bolívar Puente
(preprint, website, github, cppnow17 talk)

Scaling up Functional Programming Education: under the hood of the OCaml MOOC
Benjamin Canou, Roberto Di Cosmo, Grégoire Henry

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
(technical report)

Staged Generic Programming
Jeremy Yallop
(draft)

Super 8, the Story of Making Movies—A Functional Pearl
Leif Andersen, Stephen Chang, Asumu Takikawa, Matthias Felleisen
(preprint)

Symbolic conditioning of arrays in probabilistic programs
Praveen Narayanan, Chung-chieh Shan
(paper)

Testing and Debugging Functional Reactive Programming
Ivan Perez, Henrik Nilsson

Theorems for Free for Free: Parametricity, With and Without Types
Amal Ahmed, Dustin Jamner, Jeremy Siek, Philip Wadler
(artifact)

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, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
(preprint from arXiv)

Verifying Efficient Function Calls in CakeML
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan

Visitors Unchained
François Pottier
(preprint)

Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Christos Dimoulas, Stephen Chong
(no preprint yet, webpage, language website)

As of writing, the submission process for most ICFP'17 co-located events is not finished. Feel free to send a pull-request with list of accepted papers and contribute links to preprints.

Algebraic Graphs with Class (Functional Pearl)
Andrey Mokhov
(draft, hackage)

Back to the Future: Time Travel in FRP
Ivan Perez

Packrats Parse in Packs
Mario Blažević and Jacques Légaré

Ode on a Random Urn (Functional Pearl)
Leonidas Lampropoulos, Antal Spector-Zabusky, and Kenneth Foner
(pdf)

QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)
Maximilian Algehed, Koen Claessen, Moa Johansson, and Nicholas Smallbone

Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results
Rudy Braquehais and Colin Runciman

Using Coq to Write Fast and Correct Haskell
John Wiegley and Ben Delaware
(abstract)

A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow

Well-Typed Music Does Not Sound Wrong (Experience Report)
Dmitrij Szamozvancev and Michael Gale

The Linearity Monad
Jennifer Paykin and Steve Zdancewic
(draft)

Elaboration on Functional Dependencies
Georgios Karachalias and Tom Schrijvers

Quantified Class Constraints
Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. D. S. Oliveira, and Philip Wadler
(draft)

Composable Network Stacks and Remote Monads
Justin Dawson, Mark Grebe, and Andy Gill

A Meta-EDSL for Distributed Web Applications
Anton Ekblad

Hardware Software Co-Design in Haskell
Markus Aronsson and Mary Sheeran

Streaming Irregular Arrays
Robert Clifton-Everest, Trevor L. McDonell, Manuel M T Chakravarty, and Gabriele Keller

Improving STM Performance with Transactional Structs
Ryan Yates and Michael Scott

Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
Chao-Hong Chen, Vikraman Choudhury, and Ryan Newton