Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Wed 26 Aug 2020 15:45 - 16:00 at ICFP NY 6 - New York 6 Chair(s): Sukyoung Ryu
Thu 27 Aug 2020 03:45 - 04:00 at ICFP Asia 6 - Asia 6 Chair(s): Sukyoung Ryu

Implicit functions are dependently typed functions, such that arguments are provided (by default) by inference machinery instead of programmers of the surface language. Implicit functions in Agda are an archetypal example. In the Haskell language as implemented by the Glasgow Haskell Compiler (GHC), polymorphic types are another example. Implicit function types are first-class if they are treated as any other type in the surface language. This holds in Agda and partially holds in GHC. Inference and elaboration in the presence of first-class implicit functions poses a challenge; in the context of Haskell and ML-like languages, this has been dubbed "impredicative instantiation'' or "impredicative inference''. We propose a new solution for elaborating first-class implicit functions, which is applicable to full dependent type theories and compares favorably to prior solutions in terms of power, generality and simplicity. We build atop Norell’s bidirectional elaboration algorithm for Agda, and we note that the key issue is incomplete information about insertions of implicit abstractions and applications. We make it possible to track and refine information related to such insertions, by adding a function type to a core Martin-Löf type theory, which supports strict (definitional) currying. This allows us to represent undetermined domain arities of implicit function types, and we can decide at any point during elaboration whether implicit abstractions should be inserted.

Wed 26 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

14:30 - 16:25
New York 6ICFP Program at ICFP NY 6
Chair(s): Sukyoung RyuKAIST

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI Media Attached
14:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI Media Attached
15:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI Media Attached
15:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
15:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
15:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
16:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
16:15
10m
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity of Pennsylvania

Thu 27 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

02:30 - 04:25
Asia 6ICFP Program at ICFP Asia 6
Chair(s): Sukyoung RyuKAIST

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI Media Attached
02:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI Media Attached
03:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI Media Attached
03:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
03:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
03:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
04:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
04:15
10m
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity of Pennsylvania