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

The metatheory of Scala’s core type system—the \emph{Dependent Object Types (DOT)} calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a \emph{semantics-first} approach to develop a logical relations model for a new version of DOT, called \textbf{guarded DOT (gDOT)}. Our logical relations model makes use of an abstract form of \emph{step-indexing}, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.

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 - 14:45
Talk
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI
14:45 - 15:00
Talk
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI
15:00 - 15:15
Talk
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI
15:15 - 15:30
Talk
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI
15:30 - 15:45
Talk
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI
15:45 - 16:00
Talk
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print
16:00 - 16:15
Talk
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI
16:15 - 16:25
Day 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 - 02:45
Talk
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
DOI
02:45 - 03:00
Talk
ICFP Program
Paolo G. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft University of Technology
DOI
03:00 - 03:15
Talk
ICFP Program
Matúš TejiščákUniversity of St Andrews
DOI
03:15 - 03:30
Talk
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI
03:30 - 03:45
Talk
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI
03:45 - 04:00
Talk
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print
04:00 - 04:15
Talk
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI
04:15 - 04:25
Day closing
ICFP Program
Stephanie WeirichUniversity of Pennsylvania