International Conference on Functional Programming 2017

International Conference on Functional Programming 2017

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

January 23, 2018 • 17 mins
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 parts of their surface language in terms of a smaller core. Thus some properties of the surface language, like its scoping rules, are no...
Mark as Played

Automating Sized-Type Inference for Complexity Analysis

January 23, 2018 • 18 mins
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: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and constraint solv...
Mark as Played

Constrained Type Families

January 23, 2018 • 16 mins
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 compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For...
Mark as Played

Gradual Typing with Union and Intersection Types

January 23, 2018 • 17 mins
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 set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type ...
Mark as Played

On Polymorphic Gradual Typing

January 22, 2018 • 1084 mins
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 method to integrate dynamic typing and static typing smoothly in a single language--to parametric polymorphism and its theoretical prop...
Mark as Played

Theorems for Free for Free: Parametricity, With and Without Types

January 22, 2018 • 20 mins
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 Edinburgh, UK). The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challeng...
Mark as Played

Gradual Session Types

January 22, 2018 • 20 mins
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 Edinburgh, UK). Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type sys...
Mark as Played

Manifest Sharing with Session Types

January 22, 2018 • 21 mins
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 logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude man...
Mark as Played

Whip: Higher-Order Contracts for Modern Services

January 22, 2018 • 18 mins
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 semantically rich protocols and middleware when composing services. Instead, they embrace the loosely-coupled development and deployment of servic...
Mark as Played

A Metaprogramming Framework for Formal Verification

January 17, 2018 • 16 mins
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 University, USA), Leonardo De Moura (Microsoft Research). Dependent type theory is a powerful framework for interactive theorem proving an...
Mark as Played

Normalization by Evaluation for Sized Dependent Types

January 17, 2018 • 20 mins
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 been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type chec...
Mark as Played

A Specification for Dependent Types in Haskell

January 17, 2018 • 18 mins
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 Campinas, Brazil), Richard A. Eisenberg( Bryn Mawr College, USA). We propose a core semantics for Dependent Haskell, an extension of Ha...
Mark as Played

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)

January 17, 2018 • 20 mins
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 ultimate abstraction, dixit Paul Hudak. But what abstraction should we use to build such ultimate abstractions? What is sauce for the goo...
Mark as Played

Visitors Unchained

January 17, 2018 • 17 mins
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. We address this problem in the setting of OCaml, a functional programming language equipped with powerful object-oriented features. We u...
Mark as Played

Compiling to Categories

January 16, 2018 • 18 mins
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 programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of m...
Mark as Played

Local Refinement Typing

January 16, 2018 • 14 mins
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 inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is con...
Mark as Played

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools

January 15, 2018 • 18 mins
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 Washington, USA, Michael D. Ernst, University of Washington, USA, Zachary Matlock, University of Washington, USA. Many verification tools build ...
Mark as Played

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification

January 15, 2018 • 19 mins
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 functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq lib...
Mark as Played

No-Brainer CPS Conversion

January 15, 2018 • 14 mins
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 their equivalent terms in continuation-passing style (CPS) typically introduce so-called 'administrative redexes' -- useless artifacts of t...
Mark as Played

Foundations of Strong Call by Need

January 15, 2018 • 18 mins
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 Diderot, France), Eduardo Bonelli (CONICET, Argentina/Universidad Nacional de Quilmes, Argentina), Delia Kesner (IRIF/University of Paris Did...
Mark as Played

Popular Podcasts

    On Purpose with Jay Shetty

    On Purpose with Jay Shetty

    I’m Jay Shetty host of On Purpose the worlds #1 Mental Health podcast and I’m so grateful you found us. I started this podcast 5 years ago to invite you into conversations and workshops that are designed to help make you happier, healthier and more healed. I believe that when you (yes you) feel seen, heard and understood you’re able to deal with relationship struggles, work challenges and life’s ups and downs with more ease and grace. I interview experts, celebrities, thought leaders and athletes so that we can grow our mindset, build better habits and uncover a side of them we’ve never seen before. New episodes every Monday and Friday. Your support means the world to me and I don’t take it for granted — click the follow button and leave a review to help us spread the love with On Purpose. I can’t wait for you to listen to your first or 500th episode!

    Las Culturistas with Matt Rogers and Bowen Yang

    Las Culturistas with Matt Rogers and Bowen Yang

    Ding dong! Join your culture consultants, Matt Rogers and Bowen Yang, on an unforgettable journey into the beating heart of CULTURE. Alongside sizzling special guests, they GET INTO the hottest pop-culture moments of the day and the formative cultural experiences that turned them into Culturistas. Produced by the Big Money Players Network and iHeartRadio.

    Crime Junkie

    Crime Junkie

    Does hearing about a true crime case always leave you scouring the internet for the truth behind the story? Dive into your next mystery with Crime Junkie. Every Monday, join your host Ashley Flowers as she unravels all the details of infamous and underreported true crime cases with her best friend Brit Prawat. From cold cases to missing persons and heroes in our community who seek justice, Crime Junkie is your destination for theories and stories you won’t hear anywhere else. Whether you're a seasoned true crime enthusiast or new to the genre, you'll find yourself on the edge of your seat awaiting a new episode every Monday. If you can never get enough true crime... Congratulations, you’ve found your people. Follow to join a community of Crime Junkies! Crime Junkie is presented by audiochuck Media Company.

    The Clay Travis and Buck Sexton Show

    The Clay Travis and Buck Sexton Show

    The Clay Travis and Buck Sexton Show. Clay Travis and Buck Sexton tackle the biggest stories in news, politics and current events with intelligence and humor. From the border crisis, to the madness of cancel culture and far-left missteps, Clay and Buck guide listeners through the latest headlines and hot topics with fun and entertaining conversations and opinions.

    The Bobby Bones Show

    The Bobby Bones Show

    Listen to 'The Bobby Bones Show' by downloading the daily full replay.

Advertise With Us
Music, radio and podcasts, all free. Listen online or download the iHeart App.

Connect

Explore

iHeart

Live Radio

Podcasts

Artist Radio

Exclusives

News

Features

Events

Contests

Photos

Information

About

Advertise

Blog

Brand Guidelines

Contest Guidelines

Subscription Offers

Jobs

Get the App

Automotive

Home

Mobile

Wearables

© 2025 iHeartMedia, Inc.