Maksim TrifunovskiSoftware Engineer • Programming Languages Researcher
Projects
About Me
I am a rising senior at Wesleyan University pursuing a double
major in Mathematics and Computer Science. My main areas of interest
include Number Theory, Abstract Algebra, Mathematical Logic,
Algorithms and Type Theory.
Outside of academics, I love watching and playing sports,
as well as video gaming. I am a big supporter of the New England
Patriots and Juventus. During my free time, I play Dota 2 with my friends.
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].
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.
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.