Luau, Gradual Typing and Semantic Subtyping

Add to your list(s) Download to your calendar using vCal

• Alan Jeffrey
• Friday 09 February 2024, 14:00-15:00
• GN06, Computer Laboratory.

If you have a question about this talk, please contact nk480.

This talk has been canceled/deleted

This paper presents recent work on the Luau programming language which is used for, amongst other reasons, scripting games. We talk about the human aspects of the Luau type system, and in particular, how large the heterogeneous developer community is for Luau. We then talk about two recent developments in Luau, in particular gradual type and semantic subtyping.

Our presentation of gradual typing is different from others and uses type error suppression.

Our definition of “pragmatic semantic subtyping” drops the set theoretic requirement from the original development of semantic subtyping, resulting in a simpler presentation of an algorithm for subtyping.

These recent developments have been implemented in production Luau, and mechanically verified in Agda for a core Luau.

Anyone who wants to ask about recent work, or the last 30 years of a varied CS career, should feel free.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.