Write a Blog >>
ECOOP 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Wed 14 Jul 2021 19:10 - 19:30 at ECOOP 1 - Types (time band 1) Chair(s): Sam Tobin-Hochstadt
Fri 16 Jul 2021 11:00 - 11:20 at ECOOP 1 - Types / Program Analysis (time band 3) Chair(s): George Fourtounis

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.

Lecturer in Computer Science at the University of St Andrews

Wed 14 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

18:30 - 19:30
Types (time band 1)ECOOP Technical Papers at ECOOP 1
Chair(s): Sam Tobin-Hochstadt Indiana University
18:30
20m
Talk
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types
ECOOP Technical Papers
Anish Tondwalkar University of California, San Diego, Matthew Kolosick University of California, San Diego, Ranjit Jhala University of California at San Diego
DOI
18:50
20m
Talk
Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers
ECOOP Technical Papers
Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology
DOI File Attached
19:10
20m
Talk
Idris 2: Quantitative Type Theory in Practice
ECOOP Technical Papers
Edwin Brady University of St Andrews, UK
DOI Media Attached

Fri 16 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:00 - 11:20
Types / Program Analysis (time band 3)ECOOP Technical Papers at ECOOP 1
Chair(s): George Fourtounis University of Athens
10:00
20m
Talk
Accelerating Object-Sensitive Pointer Analysis by Exploiting Object Containment and Reachability
ECOOP Technical Papers
Dongjie He University of New South Wales, Jingbo Lu UNSW Sydney, Yaoqing Gao Huawei Canada, Jingling Xue UNSW
DOI Pre-print
10:20
20m
Talk
Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow AnalysisDistinguished Paper
ECOOP Technical Papers
Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann Technical University Dortmund, Eric Bodden University of Paderborn; Fraunhofer IEM
Link to publication DOI Pre-print
10:40
20m
Talk
Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers
ECOOP Technical Papers
Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology
DOI File Attached
11:00
20m
Talk
Idris 2: Quantitative Type Theory in Practice
ECOOP Technical Papers
Edwin Brady University of St Andrews, UK
DOI Media Attached