Write a Blog >>
ECOOP 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Thu 15 Jul 2021 01:40 - 02:00 at ECOOP 1 - Types (time band 2) Chair(s): Werner Dietl
Thu 15 Jul 2021 09:10 - 09:30 at ECOOP 1 - Potpourri (time band 3) Chair(s): Viktor Kunčak

The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λBg, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λBr, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi type safety is proved. Furthermore we show that the semantics of λBg is sound with respect to the semantics of the blame calculus, and that λBr comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.

Type Directed Operational Semantics for Gradual Typing (ecoop2021_6.28.pdf)337KiB

Thu 15 Jul

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

01:40 - 02:20
Types (time band 2)ECOOP Technical Papers at ECOOP 1
Chair(s): Werner Dietl University of Waterloo
01:40
20m
Talk
Type-Directed Operational Semantics for Gradual Typing
ECOOP Technical Papers
Wenjia Ye The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuejing Huang The University of Hong Kong
DOI Media Attached File Attached
02:00
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
09:10 - 10:10
Potpourri (time band 3)ECOOP Technical Papers at ECOOP 1
Chair(s): Viktor Kunčak EPFL, Switzerland
09:10
20m
Talk
Type-Directed Operational Semantics for Gradual Typing
ECOOP Technical Papers
Wenjia Ye The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuejing Huang The University of Hong Kong
DOI Media Attached File Attached
09:30
20m
Talk
Lambda-based object-oriented programmingPearl
ECOOP Technical Papers
Marco Servetto Victoria University Wellington, New Zealand, Elena Zucca University of Genova
DOI Media Attached
09:50
20m
Talk
ALPACAS: A Language for Parametric Assessment of Critical Architecture Safety
ECOOP Technical Papers
Maxime Buyse Uber ATCP, Remi Delmas Uber ATCP, Youssef Hamadi Uber Elevate
DOI