What I Learned This Week: Subset types, real numbers, and more Coq


This has been a productive week with my Coqplexity project really starting to get off of the ground. Coqplexity is at the point now where it can automatically prove pretty much any polynomial Big O relation (as long as it’s true).

Some more work needs to be done in Coqplexity in order to make it more useful, but the foundation is there, and it’s been a good bit of experience in writing tactics and dealing with real numbers.

So, more stuff about subset types, tactics, and more!

Read more »

What I Learned This Week: Progress Sensitive Security, Erasure


Let’s keep this going! The goal of this is again, to write down some of my thoughts and what I did. This is not necessarily going to be accurate, but maybe it will be useful! Contact me if you find mistakes :).

The past week I have managed to get through another chunk of papers on the following topics:

  • Removing information leaks through the progress covert channel
  • Ensuring data erasure in programs which use untrusted data stores

Additionally, I have started to research real number libraries in Coq for use in a project…

Read more »

What I Learned This Week: Coinduction, Dependent Pattern Matching, and Langsec


I’m starting a small series. The gist of it? What I learned in the past week.

Each post will be a brief summary of some things which I studied in the past week. Not necessarily an in depth exploration of the topics, but you may find useful insight, or at least useful references if something is a topic of interest.

If you find a mistake in my understanding, or have a question, feel free to contact me!

With that out of the way, let’s talk about some of the things I read about this week. Coinduction in Coq, dependent pattern matching in Coq, and some papers in langsec.

Read more »

Absolutely Optimal

Program optimization is strange.

We naturally want our programs to run as quickly and efficiently as possible, but in some sense I have no idea what that actually means. Or, rather, I have no idea what “computation” actually entails.

Read more »

First Post!


I now apparently have a blog. I don’t know if this will ever see an update, or if this will ever be read by anybody, but the intention is to put some ramblings up here.

Read more »