Tue 22 Oct 2024 17:00 - 17:20 at San Marino - Session 4 on Typing and Its Applications Chair(s): Jeff Smits

Practical metaprogramming applications often involve manipulating open code fragments, which is easy to get wrong in the absence of static verification that all variable occurrences remain correctly bound. Many approaches have been proposed to verify the type- and scope-safety of metaprograms, but these approaches are either incomplete or cumbersome, imposing heavy type annotation or proof obligation burdens on metaprogrammers. In this short paper, we propose a new type system to statically keep track of the context requirements of code fragments. Our system uses a novel combination of Boolean-algebraic subtyping and first-class polymorphic type inference techniques to alleviate the annotation burden. The former provides the ability to encode scope requirements as unions of types and the latter allows these types to be locally quantified through a flexible form of polymorphic subtyping. We formalize this type system and demonstrate its implementation in the nascent MLscript functional and object-oriented programming language.

Tue 22 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:30
Session 4 on Typing and Its ApplicationsGPCE at San Marino
Chair(s): Jeff Smits Delft University of Technology
16:00
30m
Talk
Separate Compilation and Partial Linking: Modules for Datalog IR
GPCE
David Klopp JGU Mainz, André Pacak JGU Mainz, Sebastian Erdweg JGU Mainz
16:30
30m
Talk
On the Soundness of Auto-Completion Services for Dynamically Typed Languages
GPCE
Damian Frölich University of Amsterdam, L. Thomas van Binsbergen University of Amsterdam
DOI Pre-print
17:00
20m
Talk
Seamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)Reusable ArtifactAvailable Artifact
GPCE
Cunyuan Gao HKUST, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
17:20
10m
Day closing
GPCE24 Closing
GPCE
Thomas Thüm Paderborn University, Shigeru Chiba University of Tokyo