Intrinsic Verification of a Regular Expression Matcher

---

During the summer of 2015, I was working on a research project with Professor Daniel R. Licata and Joomy Korkut. Our goal was to revisit an algorithm for a Regular Expression Matcher by Rob Harper and implement it in Agda, while proving its correctness as well.
Since Agda is a total language, hence all computations must terminate, we had to explicitly deal with the case of the Kleene star regular expression, since it matches zero or more occurences of it. Hence we used standard regular expressions which are a subset of regular expressions where Kleene star is replaced with Kleene plus, which matches one or more occurences instead of zero. Here is the specification for our matcher function:

match : (r : StdRegExp) → (s : List Char) → (k : List StdRegExp) → Maybe (Σ (List Char × List Char) (λ { (p , s') → (p ++ s' ≡ s) × (p ∈Lˢ r) × s' ∈Lᵏ k}))

As you can see this function takes a standard regular expression r, a string (list of characters) s, and a stack of regular expressions that are yet to be matched k, and returns a value of type Maybe, which means, it will either return None, if we could not match, or Some pair of strings p and s', such that p is a prefix of s and s' is a suffix, which together make up s. Furthermore the regular expression r matches with p, and the stack of remaining regular expressions k matches with s'.
Hence if we want to try to match the string "a", with the regular expression (Lit "a"), we would call match (Lit "a") ["a"] [] and get a result Some (["a"] , [] , ["a"]++[] = ["a"] , ["a"] ∈Lˢ (Lit "a") , [] ∈Lᵏ []). Notice we call the function with the empty stack at the beginning. You can check the code for all the cases.
We wrote another type of matcher, which uses a higher order function continuation passing style, where instead of a stack of regular expressions that are yet to be matched, we have a function which does that. Here is the specification of that matcher:

match : (C : Set) → (r : StdRegExp) → (s : List Char) → (k : ∀ {p s'} → p ++ s' ≡ s → p ∈Lˢ r → Maybe C) → RecursionPermission s → Maybe C

In this matcher, we also pass a so called "Recursion Permission" which helps Agda see that every future recursive call to match has a smaller string, so that the function terminates.
You can also notice that the way we defined the matchers in both cases, we have soundness of successful matching, so we have proved soundness intrinsically. We Proved the completness of our function extrinsically.
In the end we also wrote an extractor, which can extract parts of a string that match with specific parts of the regular expression, for example if we had a regular expression for matching emails, and we had the email "johndoe@domain.com", we can extract [johndoe, domain, com].

• Paper
• Code

Close

FoodyCall

---

During WesHack 2014, we created a food ordering app for 2 of the university dining places. The app allows a person to see the menu for the restaurant open at the current time, and pick desired meal. After selecting the meal, the app sends a message to the restaurant with the details of the order and waits for a response. When it receives a confirmation, it gives the customer the order number with which the customer can then pick up the food. The frontend was written in JS, while the backend was done in Python, using Flask, and MongoDB for our database. We also used Twilio to handle sending and receiving messages. You can find the code on the github link below.

• Client: Wesleyan University
• Date: September 2014
• Code: FoodyCall

Close

Effect of climate change on the distribution of Caribou (Rangifer Tarandus)

---

An Evolutionary Bioinformatics final project talking about the potential distribution of the Caribou, its main food source, the Cladonia Rangiferina and its main predator, Canis Lupus in the year 2070.
The data for the distribution of Caribou and Canis Lupus was gathered from vertnet.com, while the data for Cladonia Rangiferina was gathered from gbif.org. We then analyzed the data using MaxEnt (Maximum entropy modeling) and global climate predictions obtained from worldclim.org. The poster and paper for the project can be found on the github link below.

• Date: December 2015
• Code: GitHub

Close