Contact Info
- Email:
- my-first-name-goes-here at cs.cmu.edu
- Mailing Address:
- Aleksey Kliger
Computer Science Department
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213 USA
- Office:
- 8114 Wean
- Phone:
- 1 412 268-3056
Research Interests
Some of my interests are: type theory, programming language design, logical frameworks, certified code (typed assembly languages and proof-carrying code), garbage collection, parametricity and safety. I am advised by Karl Crary.
Currently I am working on a logic suitable for reasoning about low-level memory managers such as garbage collectors. By building on this logic, we hope to take the garbage collector out of the trusted computing base of a certified code framework and treat it like any other untrusted component. A draft of my proposal is available (Last updated: Apr 23).
Previously I worked on a logically-motivated type system for secure information flow. By starting with a logical (i.e. monadic) account that treats effects explicitly, we can take a store-oriented view of security suitable as a foundation to low-level secure intermediate languages. Some results appear below.
I am a member of the ConCert project: a framework for trustless grid computing via certified code.
As an undergraduate at Cornell, I did some hacking on polyglot: an extensible Java source-to-source translator for experimenting with extensions to the Java language. If you have to work with Java, polyglot is a good starting point.
Papers
Information Flow
Karl Crary, Aleksey Kliger, Frank Pfenning, A Monadic Analysis of Information Flow Security with Mutable State. (Abstract)
- 2005 (March). Journal of Functional Programming 15(2), 249–291. (BibTeX, pdf, errata)
© 2005 Cambridge University Press. - A short preliminary summary appeared in Foundations of Computer Security Workshop (FCS'04). Turku, Finland, July 2004. (pdf)
- Originally, CMU Technical Report CMU-CS-03-164, July 2003. (available as pdf and ps)
Talks
- Secure information flow with monadic types:
- Based on our work on a monadic analysis of information flow security. This talk is available in two flavors:
- A more general, less technical version. (presented in October 2005 at the Student Seminar Series at CMU)
- A more detailed, slightly technical version. (presented in April 2006 at the Secure Systems Seminar at Stevens)
Teaching
I was a teaching assistant for 15-814, the graduate intro to type systems, on two occasions: Fall 2003, Fall 2002.
In the spring of 2007, I was a teaching assistant for 15-213, an undergraduate introduction to computer systems. A subset of my recitation notes are available.
Hobbies, &tc.
For a few years, I was involved with the No Parking Players improvisation comedy organization at CMU. NPP runs improv workshops open to all members of the CMU community. In addition, a subset of NPP (dubbed the "performance group") puts on regularly scheduled improv performances during the academic year.
In the past, I juggled with the UPitt juggling club and occasionally with the sporadically-meeting CMU juggling club. As an undergrad, I was involved with the Cornell Juggling club.
Also, I make bad puns, such as this one about the Curry-Howard Isomorphism.
My sporadically updated personal webpage has more about my non-academic side.
