International Conference on Functional Programming 2017
by Oxford University
ICFP 2017 is the 22nd ACM SIGPLAN International Conference on Functional Programming.ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. This year, there are keynotes from Chris Martens and John Launchbury; unfortunately, Rich Hickey was unable to attend as originally planned.
Episodes
-
Inferring Scope through Syntactic Sugar
Justin Pombrio (Brown University, USA) gives the third talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. Co-written by Shriram Krishnamurthi (Brown University, USA) and Mitchell Wand (Northeastern University, USA). Many languages use syntactic sugar to define...
-
Automating Sized-Type Inference for Complexity Analysis
Martin Avanzini (University of Innsbruck, Austria) gives the second talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients…
more -
Constrained Type Families
Richard A. Eisenberg (Bryn Mawr College, USA) gives the first talk in the fifth panel, Inference and Analysis, on the 3rd day of the ICFP conference. Co-written by J. Garrett Morris (University of Kansas, USA). We present an approach to support partiality in type-level computation without...
-
Gradual Typing with Union and Intersection Types
Victor Lanvin (ENS Cachan, France) gives the third talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Giuseppe Castagna (CNRS, University of Paris Diderot). We propose a type system for functional languages with gradual types and...
-
On Polymorphic Gradual Typing
Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Taro Sekiyama (IBM Research, Japan), Atsushi Igarashi (Kyoto University, Japan). We study an extension of gradual typing--a...
-
Theorems for Free for Free: Parametricity, With and Without Types
Amal Ahmed (Northeastern University, USA) gives the first talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Dustin Jamner (Northeastern University, USA), Jeremy G. Siek (Indiana University, USA), Philip Wadler (University of...
-
Gradual Session Types
Peter Thiemann (University of Freiburg, Germany) gives the fourth talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written by Atsushi Igarashi (Kyoto University, Japan), Vasco Vasconcelos (University of Lisbon, Portugal), Philip Wadler (University of...
-
Manifest Sharing with Session Types
Stephanie Balzer (Carnegie Mellon University, USA) gives the third talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written Frank Pfenning (Carnegie Mellon University, USA). Session-typed languages building on the Curry-Howard isomorphism between linear...
-
Whip: Higher-Order Contracts for Modern Services
Lucas Waye (Harvard University, USA), gives the second talk in the third panel, Contracts and Sessions , on the 3rd day of the ICFP conference. Co-written by Christos Dimoulas (Harvard University, USA), Stephen Chong (Harvard University, USA). Modern service-oriented applications forgo…
more -
A Metaprogramming Framework for Formal Verification
Sebastian Ullrich (KIT, Germany), gives the fourth talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Gabriel Exner (Vienna University of Technology, Austria), Jared Roesch (University of Washington, USA), Jeremy Avigad (Carnegie Mellon...
-
Normalization by Evaluation for Sized Dependent Types
Andreas Abel (University of Gothenburg, Sweden), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Andrea Vezzosi (Chalmers University of Technology, Sweden), Theo Winterhalter (ENS Paris-Saclay, France). Sized types have...
-
A Specification for Dependent Types in Haskell
Antoine Vizard (University of Pennsylvania, USA), gives the first talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Stephanie Weiricc (University of Pennsylvania, USA), Pedro Henrique Azevedo de Amorim (Ecole Polytechnique, University of...
-
Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
Robby Findler (Northwestern University, USA), gives the first talk in the first panel, Domain-Specific Languages, on the 3rd day of the ICFP conference. Co-written by Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Northwestern University. Domain-specific languages are the...
-
Visitors Unchained
Francois Pottier (Inria, France), gives the second talk in the fourth panel, Program Construction, on the 2nd day of the ICFP conference. Traversing and transforming abstract syntax trees that involve name binding is notoriously difficult to do in a correct, concise, modular, customisable manner....
-
Compiling to Categories
Conal Elliott, Target, USA, gives the first talk in the fourth panel, Program Construction, on the 2nd day of the ICFP conference. It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional…
more -
Local Refinement Typing
Benjamin Cosman, University of California at San Diego, USA, gives the third talk in the second panel, Tools for Verification, on the 2nd day of the ICFP conference. Co-written by Ranjit Jhala, University of California at San Diego, USA. We introduce the FUSION algorithm for local refinement type...
-
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Konstantin Weitz (University of Washington, USA) gives the second talk in the second panel, Tools for Verification, on the 2nd day of the ICFP conference. Co-written by Steven Lyubomirsky, University of Washington, USA, Stefan Heule, Stanford University, USA, Emina Torlak, University of…
more -
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Co-written by Joonwon Choi, Benjamin Sherman, Adam Chlipala, Arvind (Massachusetts Institute of Technology, USA). It has become fairly standard in the programming-languages research world to verify...
-
No-Brainer CPS Conversion
Milo Davis (Northeastern University, USA) gives the fourth talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP. Co-written by William Meehan and Olin Shivers (Northeastern University, USA). Algorithms that convert direct-style lambda-calculus terms to…
more -
Foundations of Strong Call by Need
Thibaut Balabonski (LRI, France and University of Paris-Sud, France) gives the third talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. Co-written by Pablo Barenbaum (University of Buenos Aires, Argentina/IRIF, France/University of Paris...
-
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Makoto Hamana (Gunma University, Japan), gives the first talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. We present a general methodology of proving decidability of equational theory of programming language concepts in the framework of...
-
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland (Drexel University, USA) gives the fourth talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Software-defined radio (SDR) promises to bring the flexibility and rapid iterative workflow of software to radio protocol design. Many...
-
Verifying Efficient Function Calls in CakeML
Scott Owens University of Kent, UK, gives the third talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Co-written Michael Norrish, Ramana Kumar (Data61 at CSIRO, Australia and UNSW, Australia), Magnus O. Myreen (Chalmers University of Technology,...
-
A Relational Logic for Higher-Order Programs
Alejandro Aguirre, IMDEA Software Institute, Spain, gives the second talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference. Co-written by Gilles Berthe (IMDEA Software Institute, Spain), Marco Gaboardi (University at Buffalo, SUNY, USA), Deepak...
-
Verified Low-Level Programming Embedded in F
Jonathan Protzen, Microsoft Research, United States, gives the second talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Co-written by Jonathan Protzen (Microsoft Research, United States), Jean-Karim Zinzindohoué (Inria, France), Aseem Rastogi...
-
Persistence for the Masses: RRB-Vectors in a Systems Language
Juan Pedro Bolívar Puente, Independent Consultant, Sinusoidal Engineering, Germany, gives the first talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference. Relaxed Radix Balanced Trees (RRB-Trees) is one of the latest members in a family of persistent…
more -
Assuring AI
John Launchbury, Chief Scientist of Galois Inc, gives the second keynote of the ICFP conference. Somewhat ironically, just as traditional systems software finally comes within reach of detailed mathematical verification, the demand for verification technology is rapidly expanding into domains…
more -
Effect-Driven QuickChecking of Compilers
Jan Midtgaard, gives the fourth presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson, DTU, Denmark. How does one test a language implementation with QuickCheck (aka. property-based...
-
Imperative Functional Programs that Explain their Work
Jan Stolarek, University of Edinburgh, UK, gives the third presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Wilmer Ricciotti, Roly Perera and James Cheney, and University of Edinburgh, UK. Program slicing provides explanations that illustrate how program…
more -
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
Ohad Kammar, University of Oxford, UK, gives the second presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Yannick Forster (Saarland University, Germany and University of Cambridge, UK), Sam Lindley (University of Edinburgh). We compare the expressive power of...
-
Abstracting Definitional Interpreters
David Darais, University of Maryland, USA, gives the first presentation in the fourth panel, Effects, in the ICFP 2017 conference. Co-written by Nicholas Labich, David Van Horn, Phuc C. Nguyen, University of Maryland, USA. In this functional pearl, we examine the use of definitional interpreters…
more -
Symbolic Conditioning of Arrays in Probabilistic Programs
Praveen Narayanan, Indiana University, USA, gives the third presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Chung-Chief Shan, Indiana University, USA. Probabilistic programming systems make machine learning methods modular by automating inference. Recent...
-
A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort University of Pennsylvania, USA, gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Andreas Haeberlen and Aaron Roth, University of Pennsylvania, USA. Differential privacy is a widely studied theory for analyzing…
more -
Prototyping a Query Compiler using Coq (Experience Report)
Louis Mandel (IBM) gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Joshua Auerbach, Martin Hirzel, Avraham Shinnar, Jerome Simeon, IBM Research, USA. Designing and prototyping new features is important in many industrial projects.…
more -
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
William E. Byrd, University of Utah, USA, gives the fourth presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Co-written by Gregory Rosenblatt, Matthew Might, Michael Ballantyne (University of Utah). We present seven programming challenges in Racket,...
-
Generic Functional Parallel Algorithms: Scan and FFT
Conal Elliott, Target, USA United States, gives the third presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Parallel programming, whether imperative or functional, has long focused on arrays as the central data type. Meanwhile, typed functional...
-
A Pretty But Not Greedy Printer (Functional Pearl)
Jean-Philippe Bernardy, University of Gothenburg, gives the second presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. This paper proposes a new specification of pretty printing which is stronger than the state of the art: we require the output to be...
-
Faster Coroutine Pipelines
Mike Spivey, University of Oxford, UK, gives the first presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference. Coroutine pipelines provide an attractive structuring mechanism for complex programs that process streams of data, with the advantage over lazy...
-
Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC
Roberto Di Cosmo (Inria, France and University of Paris Diderot, France), gives the fourth presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Benjamin Canou (OCamlPro) and Gregoire Henry (OCamlPro). This article describes the key innovations used in the...
-
Lock-Step Simulation Is Child's Play (Experience Report)
Joachim Breiner, University of Pennsylvania, United States, gives the third presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Chris Smith Google, USA. Implementing multi-player networked games by broadcasting the player's input and letting each client...
-
Testing and Debugging Functional Reactive Programming
Ivan Perez, University of Nottingham, UK, gives the second presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Henrik Nilsson, University of Nottingham, UK. Many types of interactive applications, including video games, raise particular challenges when…
more -
Super 8 Languages for Making Movies (Functional Pearl)
Leif Andersen (Northeastern University, USA) gives the first presentation in the first panel, Art and Education, in the ICFP 2017 conference. Co-written by Stephen Chang (Northeastern University, USA) and Matthias Felleisen (Northeastern University, USA). The Racket doctrine tells developers to...
-
Compositional Creativity: Some Principles for Talking to Computers
Chris Martens (North Carolina State University, United States) gives the first talk in the ICFP conference. Generativity is an increasingly popular and useful concept, referring to a machine's ability to respond to user input with new constructions not foreseen by the programmer. Yet…
more -
Chaperone Contracts for Higher-Order Sessions
Hernan Melgratti (University of Buenos Aires, Argentina), gives the first talk in the third panel, Contracts and Sessions, on the 3rd day of the ICFP conference. Co-written by Luca Padovani (University of Turin, Italy). Contracts have proved to be an effective mechanism that helps developers in...
About this show
ICFP 2017 is the 22nd ACM SIGPLAN International Conference on Functional Programming.ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. This year, there are keynotes from Chris Martens and John Launchbury; unfortunately, Rich Hickey was unable to attend as originally planned.
Hosted by
Oxford University
Categories