Computers / Math / Stuff
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 »
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 »
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 »
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 »
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 / comment »
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 »
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 »
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 »
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 »