Tracking Captures in Types
Despite 100s of publications, effects and resources are not yet widely reflected in type systems. This is at least in part due to the notational overhead imposed by traditional typing approaches, in particular in relation to effect polymorphism. However, the situation can be improved if effects are represented as capabilities. Capabilities can describe both effects and resources. To keep track of resource usage in types, we develop a type system that tracks free capabilities in values. Together with implicit parameters, this allows for flexible and lightweight modelling of effects and resources.
Joint work with Aleksander Boruch-Gruszeki, Jonathan Brachthauser, Edward Lee and Ondrej Lhotak
Slides (cc.pdf) | 5.52MiB |
Martin Odersky is a professor at EPFL in Lausanne, Switzerland. He has been working on programming languages for most of his career. He first studied structured and object-oriented programming as a PhD student of Niklaus Wirth, then fell in love with functional programming while working as a post doc at IBM and Yale. When Java came out, he started to add functional programming constructs to the new platform. This led to Pizza and GJ and eventually to Java 5 with generics. During that time he also developed javac, the current reference compiler for Java.
Over the last 10 years, Martin worked on unifying object-oriented and functional programming in the Scala language. Scala quickly escaped from the research lab and became a popular open source tool and industrial language. He now oversees development of Scala as head of the programming group at EPFL and as academic director of the Scala center.
Mon 6 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | |||
09:00 90mKeynote | Tracking Captures in Types Scala Martin Odersky EPFL File Attached |