When: Wednesday, 2013-Apr-03, 11h30-12h00
Where: FCUL-DI, room C6.3.38
Presenter: Joana Campos
Abstract:
In this smalltalk, I will present a simple dependently typed object-oriented language. Dependent types are types defined in terms of values that challenge the conventional distinction between the typechecking (compile-time) phase and execution (run-time) phase. I will discuss the language design based on a syntax-split approach that preserves a clear phase distinction. I will then go on to demonstrate how dependent types may be used in objects to specify and verify some kinds of properties. I will conclude with some ideas for extensions to handle mutable state and effects, as well as non-uniform dependencies involving multiple objects.