Sneha Elizabeth Popley
TCU Box 292519
Fort Worth, TX 76129
Email : sneha.e.popley{at}
Phone : (814) 317-6342


Sneha Popley is a Ph.D. student at the University of Chicago. She graduated with a bachelors degree in Computer Science and Math from Texas Christian University (Fort Worth) in May 2010.


Twelf Wiki
Coq Tutorial
A Coq Resource
POP Seminar
UPenn Research: Summer 2008
FROG Recognizer of Gestures
Choosing a PhD program
Personal Statements
Chancellor's Leadership Program PhD Comics


As a Research Assistant at the Institute for Software Research at Carnegie Mellon University, I worked with Dr. Jonathan Aldrich and Rob Simmons to formalize SASyLF in LF. We decided to use M2+ (from Carsten's thesis) and are forming a SASyLF Core Calculus that syntactically resembles M2+ but semantically resembles SASyLF. In spring 10, I continued working on this project (as my Honors thesis) remotely from Texas Christian University. My other committee members included Dr. J. Richard Rinewalt, Dr. Antonio Sanchez, and Dr. Rhonda Hatcher.


May 10 - May 16
So, I leave this Sunday for Pittsburgh. This summer I will be working on formalizing SASyLF, an LF-based educational proof assistant, in Twelf. With the utter chaos of packing, moving thrice within a week, going to the Wildflowers concert (feat. the Spazmatics and Hoobastank.. :) ), researching Pittsburgh, and finishing up paperwork at TCU, I also spent time reading for Monday:

SASyLF paper from FDPE'08: Introduces the language and talks informally about its semantics

A presentation on SASyLF

and more...

May 17 - May 23
Two meetings with my advisor, the weekly Plaid research group meetings, and one POP seminar later, I am done with my first week. I worked on converting examples I used last summer in Coq into SASyLF and Twelf so that I could get a better grasp of the language. I continued reading the papers I mentioned last week along with:

Mechanizing Metatheory in a Logical Framework

Carsten's thesis

Jason Reed's Higher-Order Constraint Simplification In Dependent Type Theory

TAPL: Types and Programming Languages

Next week, I hope to have a better grasp of the languages to begin working with examples in operational semantics and typing rules. I also have two POP seminars to look forward to!

May 24 - May 30
This week was rather productive; I read some more while I experimented with Twelf and SASyLF. I feel rather comfortable with SASyLF right now, and I am working on getting used to Twelf. I read the first 11 chapters of TAPL and will probably read the rest lesisurely as I have seen most of the basics. Jonathan has been talking to me about unification and the possible abstraction of SASyLF. My todo list for this week:

1. Read Carsten's thesis
2. Work with Twelf
3. Read Nipkow's paper on unification
4. Work examples in unification
5. Abstraction of SASyLF

On a lighter note, one of my best friends is visiting me for a few days, so we visited the Phipps conservatory, Schenley park, the Andy Warhol museum, the Cathedral, and the Shadyside shopping area.

May 31 - June 6
This week I analyzed and re-analyzed Carsten's thesis. His meta-logic is finally starting to make sense. I will be trying to code out some examples in it this weekend/before Tuesday. I worked a few examples in unification from Jason Reed's paper, and will be attempting to code out parts of it in Java. Twelf hacking has been amusing.. though not as amusing as watching adorable chipmunks near the fountain behind campus. My TODO list for this week:

Twelf hacking
Abstract Representation of SASyLF: starting with the abstract syntax
Sample proof in the metalogic
Java representation of Jason's work
Watch the adorable chipmunks in Schenley park

Jun 7 - June 20
Weeks 4 and 5 merged together for me. I got sick at the end of last week and again the beginning of this week, so it was a fun two weeks for me! : )
Workwise I have been with collaborating with Jonathan on the abstract syntax of SASyLF using the metalogic in Carsten's thesis (essentially a formalization of Twelf). I have also been learning a little more about the inner setup of SASyLF in the process. On the side, I have also been working on implementing Jason Reed's unification algorithm in Java. Right now I am experimenting with JastAdd to see how an implementation of the unification algorithm would play out. I will be talking to a few people about the algorithm and JastAdd next week. I also plan to work some examples in Carsten's metalogic, but for some reason that seems to get put off every week. Jonathan will be out of town, so I will be without advisor meetings next week. We made up for it though with three meetings in the span of two days this week.

1) Abstraction of SASyLF
2) Unification algorithm in JastAdd
3) Examples in the metalogic

My cousin's wedding is in New Jersey this weekend! Since I really wanted to visit Philadelphia this summer, I will be going a day early to meet up with a few friends and advisors from last summer. And I will probably go to the Love Park fountain. Next weekend -> Gooooooogle!

June 21 - June 27
My website updates are slightly backlogged because of the exhausting (yet amazing) weekend in San Francisco. I got back had to get a lot of work done since Jonathan is leaving for three weeks on July 5. Highlights of this week:

Meeting w/ Jason Reed: It was extremely enlightening, especially when he walked through the unification algorithm step-by-step.

Meeting w/ Zach Sparks: A fellow undergraduate in Jonathan's group. Jonathan suggested I implement the unification algorithm in JastAdd. Since my compiler theory class is next semester, I essentially had no idea what I was doing. Meeting with Zach was nice because he talked about what troubled him when he started using JastAdd a few weeks ago w/ similar previous experience.

SASyLF -> The metalogic in Carsten's thesis. It is called "M2+" but I have quite figured out how to get the right symbol to show up on the website. Anyway, I did some more reading while trying to figure out the types of rules, judgements, etc. Essentially, M2+ is a higher-order while SASyLF is only second order, so our attempt to ensure this second-order nature is reflected in the abstract syntax.

I left for San Francisco Thursday morning. I had the pleasure of catching buses starting 6:30 am, not to mention one bus didn't show up for half an hour. But it was all good. I was spending a weekend in SF for a Google retreat, not much could depress me. I got to SF ~2:30 pm (a few more delays on the way.. I don't even remember now). Met a few scholars @ airport to catch the BART to the hotel. One notable event was falling off the suitcase I was sitting on @ the airport train station. Since we got to the airport three hours before our first retreat event, a random bunch of 15 scholars went sightseeing. We were @ the Hitlon, so we walked to Coit Tower, Pier 39, Fisherman's Wharf, and back. We took a tonne of pictures! The first event we had was a social. I meet a bunch of more scholars; we also formed groups to solve an exercise which tested our Google search abilities. Unfortunately, we didn't win, but it was fun!

The next day, we had a yummy breakfast at the hotel (the watermelon was amazing!) and then drove to the Google main campus in Mountain View in two huge buses. I sat w/ Sarah, and the weirdness of having a bunch of CS women around definitely came up! We were welcomed by Laszlo Block, essentially head of HR @ Google. They talked about how they use math to determine if a person will be be a successful Google employee, etc, etc. I haven't heard of any other company that does that, so it was interesting. After that we had a demo of Android, which was super cool! The eyes-free option was awesome and really easy. After that, we raided the Google kitchen which was right outside the presentation room. I <3 free food. : )

My next tech talk was on Android, and Pransanjit walked us through the main features of the Android platform. It was a fun presentation that convinced me to push for an Android based project for my senior design project. We then toured the main campus, followed by lunch. I sat w/ a bunch of random people, but really bonded with a Googler. Hopefully, we can keep in touch. Later, I attended a session on giving a good tech interview. It was informative, and reminded me that it was the process, not answer that mattered. We then had an ice cream social in which I randomly got a picture w/ Sergey Brin! I walked past what I thought was a group shot, put my head in and smiled. Next thing I know it was a group shot WITH Sergey. I was completely unaware of that fact.: ) I also got to talk to Chad Hurley (co-founder of Youtube) for about fifteen minutes! He talked about Youtube trends (or to some extent, the lack of them), and the accessibility issues as well as current projects. I never got a picture w/ him, but he is in the background of the group shot w/ Sergey. Finally, we drove back to San Francisco, and I sat w/ Phillipa (who I talked to Chad w/). We had a really good conversation about graduate school.

Dinner was at a South-east Asian grill. It was yummy! I sat with a few more new people. We got back at about 10, and I decided to leave the group since I was tired and they were going to go out. Plus, I am underage so I didn't want to spoil their fun. :). The next day was student presentations which were also interesting. The topics ranged from saving energy in computing to labeling 3D images.

We went exploring after we got out of the retreat. We retraced oiur steps to Fisherman's Wharf, then went to Ghirardelli Square, Fort Mason, drove past the Presidio, and spent a few hours in Golden Gate Park. We finally got back at about 8, and I spent the night at an old friend's place. The next day, we did a mini-trip to Stanford University which was really pretty! I finally caught a flight back to Pittsburgh (extremely reluctantly).

In all, it was an amazing weekend w/ great people, informative presentations, and fun sightseeing. I would do it all over again in a heartbeat! I hope we will stay in touch!

June 28 - July 4
Highlights of this week:

Sleep: I slept all Monday because I was completely exhausted from last weekend. And I think I am still functioning in Eastern time, so that is NOT good.

Sigma: We finally figured out the types of judgements and rules. Moving onto theorems, proof terms, and derivations. And actually understanding them. My assignment is to look at SASyLF proofs for the week, and see how the let-normal form shows up.

Unification: I randomly introduced myself to Rob Simmons this week, and ends up he will be my pseudo-advisor for the next few weeks. We talked about a few substitution algorithms, and we will be looking at Carsten's way of handling cases in proofs next week.

Also, I might be around Pittsburgh two weeks longer than expected, so that should be fun! I will probably only get a week off before school starts, but that should be enough time to get a visa for Argentina, figure out GRE stuff, and get my stuff from storage. That should be a great week!

July 5 - July 11
Jonathan is out of town (for ECOOP), so I was working rather independently this week. I read and reread the fifth chapter of Carsten's thesis, which includes the syntax and explanation for formulas, declarations, proof terms, and, most importantly, case analysis. I struggled with the reflexivity proof for a bit, attempted to understand the diamond lemma in m2+, but that wasn't too successful. Mostly because the proof is of a rather high level, and it didn't convey the basics of M2+ I am trying to understand in a succinct manner. I also decided to write out a few more SASyLF proofs for fun, because there is a limit as to how often I can read the same chapter without some distractions.

Additionally, I explored Pittsburgh on Sunday (Point State Park, the National Aviary, etc). Pictures will be up soon.. My foray into the North Side of Pittsburgh was fun, and I found out that not all science museums are built with 20 year-olds in mind. In particular, the Carnegie Science Center which would have been perfect for a 10 - 14 year-old. A little too basic for me. But it was still fun..

Next week, I hope to meet with Rob at some point of time, and I also plan to keep reading that chapter. My paper-copy of the thesis is starting to look extremely battered right now. : )

July 12 - July 18
This week started off with an impromptu trip to NY. A friend was supposed to visit, but she couldn't last minute, so I decided to go to NY about 6 hours before I caught the flight out. It was eventful (as NY always is). Our destinations included: High Line Park, Little Italy, Chinatown, Pink Berry, Union Square Farmer's Market, Times Square, NY Public Library, Bryant Park, Brookyn Bridge, South Street Seaport, Central Park, Magnolia Bakery, Washington Square Park, amazing lasagne from Whole foods, a random candy store near Serendipity, Serendipity, Crumbs, and Indian food. In short, lots of amazing food that I did not have to cook. : )

Met with Rob on Tuesday, got some concrete ideas to work on that time together proofs in SASyLF and M2+ through basic arithmetic concepts such as commutativity. My main assignments for the week are to write proofs in SASyLF and M2+ using induction on different variables, formalize the syntax of the abstraction we came up with, and work on other examples in M2+ that use case analysis while keeping in touch with Rob and Jonathan. We have a another meeting planned at the beginning of next week, so I hope to have something concrete by then.

July 19 - July 25
More proof writing as we figure out how M2+ works. I have never read a 300 page document so many times before while learning something new every single time I read it. Case analysis is getting more and more "fun," and I can't wait to see how it plays out in the SASyLF Core Calculus. I definitely am grasping concepts faster and feel as though we are making significantly more progress than we were, say, four weeks ago. I flew to Dallas for my sister's birthday which was fun, and now I ready for next week!

July 26 - August 1
The week was spent working on more proofs in M2+ and the SASyLF Core Calculus. Meetings with Jonathan included us (him, Rob, and me) writing a whole proof over the span of about two hours. After which my head hurt, but it was a very rewarding process. Then I would get to type it up in latex which led to some very ugly-looking proofs that Rob would help me make pretty in a matter of minutes. My latex skills are getting better, which is very good. : )

A lot of what we are writing will be useful in a presentation/paper, so I feel better about where the project is headed. I look forward to a productive two more weeks!

August 2 - August 8
A few meetings with Rob and Jonathan this week. Rob and I took over the whiteboards in the fourth floor CS lounge in Wean to figure out the abstract syntax for about 3 hours straight. As usual, Frank and Bob ran into us at various points of our deliberations. I like working in the lounge. : )

But this meant I also missed the PLAID research group meeting which I felt bad about, but turns out Rob is going out of town this weekend, so we were trying to get as much done as we could. It was a rather productive session though this Thursday, and Jonathan didn't seem to mind.

Now I am getting started on the typing rules. Oh, I have never written typing rules before so this is going to be fun. We ended up collapsing the Proof terms and Declarations into one (Proof Terms) by let binding or slightly modifying the term rules, This was done to save us the pain of of writing separate typing and term translation rules for proof terms and declarations. I understand let-binding much better than I did a few weeks ago after working through that process.

I met a lot more people this week from the POP group. Saw "Into the Woods" with a bunch of them. In my opinion, this is the fairy tale little kids should be told, but then I am too much of a realist. Also went to a Stamp Show at the Convention Center this Saurday. I was the only person under 25 there who had not been dragged there by a grandfather. But I love stamps. And I got some cool ones from Hungary, the Cook Islands, and two other countries I don't remember right now.

One more week to go!

August 9 - August 15
My last week is done! This week I:

Finished up most of the type translation rules (except for let and case): Yes, let and case will be the more interesting ones, but for a first shot at writing typing and type translation rules, I am tackling them according the progression of dificulty.

Presented our progress to the POP and PLAID group: I didn't realize how different graduate school presentations can be. This presentation was more of a discussion rather than the accepted undergraduate version of presenting. It was a lot of fun, and my head hurt after it, but it was a great learning experience. It was nice to be able to confidently form complete sentences about what I had been working on for the past 13 weeks.

Discussed w/ Jonathan the option of continuing this project as we write up everything as my honors project: My committee is also on board and so is the Honors College at TCU. Now I need to write up my proposal, get the necessary paperwork done, and make sure my committee at TCU is caught up.

Met w/ Dan Licata : Rob always vaguely referred to Dan's work and its relevance, so it was good to finally sit down with him and actually figure out what he does. Turns out his project on combining binding and computation isn't quite as relevant as expected, but he did know a lot about Beluga. It turns out Beluga has contexts attached to each premise which is what SASyLF does, but Beluga allows different contexts in a theorem while SASyLF does not. However, this is a variation from M2+ in which contexts are attached to the theorems. not the judgments. It will be an interesting avenue to explore in the future.

Now back to the triple-digit weather of Fort Worth, Texas. Oh wait, I have to pack and clean in Pittsburgh before unpacking and emptying out my storage unit in TX. yay!