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.