Gregory Malecha
gmalecha@cs.harvard.edu
 |
Harvard University |
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
- Reflecting Modular Automation @ Inria Rocquencourt (slides)
- Verified Proof Procedures for Separation Logic (under submission)
- Building Bedrock: Verifying a Program Verifier (talk) (Coq Workshop)
- Bedrock: A Framework for Verifying Low-Level Programs (talk) (IBM PL Day)
- Past Activities
- Coq ExtLib
- Coq Compiler
- Compiling Coq in Coq @ Inria Paris VII (slides)
- Mechanized Verification with Sharing (ICTAC 2010) [Publisher's Link]
- Trace Based Verification of Imperative Programs with I/O (JSC-WWV) [Publisher's Link]
- Verification with Sharing and Aliasing (Qualifing Exam Presentation) [Slides]
- Sharing in Ynot (UPenn Talk) [Slides]
- Toward a Verified Relational Database Management System (POPL 10) [Code] [Publisher's Link]
- Effective Interactive Proof of Higher Order Imperative Programs (ICFP 09) [Publisher's Link]
- Certified Web Services in Ynot (WWV 09) [Citeseer]
- Certified Systems Development in Ynot (NEPLS 09) [Abstract] [Slides]
- Stanford Research Institute - Natarajan Shankar (Menlo Park, CA. 2011)
- Microsoft Research - Operating Systems and Networking Team, Chris Hawblitzel (Redmond, WA. 2010)
- Peerium Inc. - Compiler & Library Development (Cambridge, MA. 2008)
- Google Inc. - PicasaWeb Team (Santa Monica, CA. 2007)
- Microsoft Corp. - Windows SE Team (Redmond, WA. 2006)
- Pointwise Inc. - Script Developer & Testing (Fort Worth, TX. 2003-04)
- FunkyMon: Functional Monitoring in Haskell - with Kelly Heffer [code]
- Spculative Parallelism in Cilk++ - with Ruben Perez
- Maximum Entropy Part-of-Speech Tagging in NLTK - with Ian Smith [code]
- Experiments in Knowledge Infusion
- Teaching
- 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.
| I'm working on low-level program verification with Bedrock
|
| 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.
|
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.