No Bug November, WILTW
WILTW #6
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 »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 »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 »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 »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 »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:
Additionally, I have started to research real number libraries in Coq for use in a project…
Read more »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 »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 »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!
https://haskellembedded.github.io/posts/2015-12-15-arm.html
Read more »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 »Hello!
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 »