Jakov Kucan: Research Summary

  • My primary research interests are in mathematical foundations of programming languages. In particular, I have been studying different typed lambda calculi, their models, and connections between logic and computation.

  • In the work on my doctoral thesis I have been exploring ways of using types in a typed lambda calculus to derive equations that are provable in the equational theory of the calculus. In particular my thesis focuses on two different ways of using types to achieve this goal.

    In the first part, Retraction Approach to CPS Transform (presented at the CW97), a relation between direct style and continuation passing style (CPS) semantics of a call-by-value computational lambda calculus is given via a $\lambda$-definable retraction. In this example types play a central role in defining the retractions. Moreover, type inference system is given a semantics that allows us to prove desired properties of the retractions.

    The second part, Another Look at ``Theorems for Free!'' (to be submitted for publication as a joint work with H.Mairson and A.Meyer), defines a framework which explores types-as-propositions paradigm to prove some useful theorems about polymorphic functions (so called ``free theorem'') as equations by convertibility. In this case (polymorphic) types are interpreted as higher order predicates over lambda terms, and the desired equalities between terms are derived as theorems of the higher order logic. By comparing models of the the higher order logic, and the equational logic of $\lambda\beta\eta$-theory, we conclude that the equalities hold by convertibility.

  • During the semester I spent at Lotus Development, I focused on a entirely different kind of research. I was involved in a design and implementation of a prototype system that would support development of synchronous multi-user applications. Together with J.Patterson and M.Day, we designed a protocol for the Notification Server, the so called Notification Server transfer Protocol (NSTP), as well as implemented a prototype server. The NSTP is intended to complement widely used HTTP by providing support for writing networked synchronous multi-user applications. The Notification Server provides clients with central shared state and gives clients the ability to maintain a consistent content of the state. The uniqueness of our design is in the fact that the server does minimal work in maintaining the state, and the task of updating and interpreting the content of the state is left up to the clients.

  • In my current work I am focusing on Linear Logic (LL), Lambda Calculus and Optimal Graph Reduction. In recent years much of attention has been focused on Optimal Graph Reduction as a technology for efficient evaluation of functional programs. It has been suggested that there is a tight connection between LL and Sharing Graphs. In our opinion the apparent similarities between the two formalisms have not been satisfactory explained. To do so, we search for a third unifying formalism that can help us better understand both LL, and Optimal Graph Reduction, as well as connection between the two. In particular we are interested in the models such as Game Semantics, Context Semantics and Geometry of Interaction.

  • Some of the topics that I would like to pursue in the future are: extending existing frameworks for reasoning about programs to programs written in a more realistic programming language (e.g. with side effects, I/O, etc.), development of a framework for reasoning about intentional aspects of functional programs (e.g. time and space complexity), further exploring benefits of representing programs as Sharing Graphs in program analysis.


    For more details, and to access some of my published work, look at my bibliography.

    To find out about my education and work experience look up my curriculum vitae.