Gregory Malecha

gmalecha@cs.harvard.edu
SEAS

Harvard University
School of Engineering and Applied Sciences
Maxwell Dworkin 309


I am a computer science Ph.D. candidate in the Programming Languages Group at Harvard. My research focus is on program verification, formal semantics, and type theory. I also enjoy machine learning. I am co-advised by Greg Morrisett and Adam Chlipala.

Current Activities
Modular proof engineering
  • Compositional and Customizable Reflective Proofs (at DTP'13, slides)
  • MirrorShard: Proof by Computational Reflection with Verified Hints (arXiv)
  • Reflecting Modular Automation @ Inria Rocquencourt (slides)
  • Verified Proof Procedures for Separation Logic (under submission)
I'm working on low-level program verification with Bedrock

Past Activities
A library & compiler for Coq
I worked on designing secure systems with CRASH
I worked on building certified systems software with Ynot.
I worked on information flow type systems with Stephen Chong
I've interned with:
Unpublished course-related reports.

Teaching

Harvard University, CS 51: Abstraction and Design, Teaching Fellow, Spring 2011.

Harvard University, CS 152: Programming Languages, Teaching Fellow, Spring 2010.

Harvard University, CS 153: Principles of Programming Languages and Compilation, Teaching Fellow, Fall 2009.

Rice University, COMP 210: Principles of Computing and Programming, Teaching Assistant, Fall 2007.

Rice University, COMP 210: Principles of Computing and Programming, Teaching Assistant, Fall 2006.

Rice University, COMP 210: Principles of Computing and Programming, Teaching Assistant, Fall 2005.


Random Programming
Coq "With" Theory
A Coq theory that makes it easier to update individual fields in a record.
Url-Rewrite
A Google Chrome plugin which rewrites urls based on regular expressions. It is useful for handling access to journal sites through the Harvard proxy, which can be accomplished with a simple rule:
http://portal\.acm\.org/(.*)
http://portal.acm.org.ezp1.harvard.edu/\1
Pure SVG Jigsaw Puzzle
A Jigsaw puzzle written using only Javascript, CSS, and SVG. There is no need for any server side pre-processing of images and can be applied to any image that your browser can download.
Pure HTML Sliding Tile Puzzle
A sliding tile puzzle (something like the 15 game) except working with images rather than numbers. This code is much older than the Jigsaw puzzle (read before I learned nice Javascript) but the project was what made me think about the jigsaw puzzle.