This is an old revision of the document!


late.jpg

Felipe Bañados Schwerter
Master Student fbanadosATdcc.uchile.cl
PLEIAD Lab Blanco Encalada 2120, of 325
Computer Science Department (DCC) Santiago, Chile
University of Chile phone: +56 2 29784788

About me

After receiving a BESc. in Computer Science from the University of Chile in 2012, I started to work on my Master's Thesis advised by Dr. Éric Tanter, on which I am currently working. I also was a Visiting Scholar at the Computer Science Department at UBC, working with Dr. Ron Garcia.

Research Abstract

From my thesis proposal's abstract

Type-and-effect or effect systems are kinds of type systems that also verify and guarantee side-effect invariants over programs. Examples of effect systems are exceptions or error handling, memory updates and I/O. Generic type-and-effect systems generalize the common patterns among effect systems characterizing effects as 'privileges'. These systems allow static reasoning about a program's execution.

At the same time, gradual type systems bridge the gap between the flexibility provided by dynamic languages, and the guarantees given by static type systems, allowing for a programmer-controlled migration between dynamic and static typing. However, these two programming language features have not been combined theoretically nor through an implementation.

We propose the introduction of gradual typing for generic type-and-effect systems. Currently, static type-and-effect systems only allow a one-step migration which can be risky or costly in ongoing software projects. A gradual approach would ease these kind of migrations by giving programmers the flexibility to decide when and where to insert the required type annotations.