Disgruntled Code

Computers / Math / Stuff

No Bug November, WILTW


Hoof! Lots of papers, lots of writing!

Taking a peek into the Firefox verified crypto, and a bunch of Coq libraries and frameworks.

Read more / comment »

What I Learned This Week: Tapir


This week has largely been administrative, with letters written, and servers managed.

I went through the Tapir/LLVM paper, and had some thoughts about theorem proving…

Read more / comment »

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 / comment »

What I Learned This Week: Real Numbers in Coq


This week more or less concludes my search for a real number library in Coq, allowing me to get another project underway which needed real numbers!

Additionally I have been messing a little bit more with subset types, which should prove useful in the very near future.

Read more / comment »

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 / comment »

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 / comment »

A Journey Through Types

I’m giving a talk as an introduction to dependently typed programming languages. The contents of this talk can be found in this post, and the slides can be found here.

Read more / comment »

Arm on Haskell

I wrote a post about setting up Haskell development for ARM over on the Haskell Embedded blog that I’m a part of. You should check it out!


Read more / comment »

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 / comment »

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 / comment »