A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

Month: August, 2011

Reversing data structures

A reversed list is not really a list anymore. It is isomorphic to a list, but it is not a list. Let me explain why. Read the rest of this entry »


Building terms, incrementally

Here is the first post of a series about incremental verification in programming languages. This problem has become more-or-less the main subject of my Ph.D, and this is an exercise in explaining it from scratch, exploring all the possible alternatives.

Eventually, the goal is to have a clear foundation for supporting better typing incrementality in programming and proof development tools. By incrementality, I mean the ability to have feedback of type errors upon any change during the development. This requires the ability to check changes in programs or proofs and not have to retype a whole development or file as it is the case too often. Read the rest of this entry »

An OCaml hack: recover the abstraction of abstract types

Here is a scoop: in OCaml, your abstract types aren’t really abstract (unfortunately). This is because some magical functions in the standard library don’t respect the abstraction of data types:, Hashtbl.hash, Pervasive.(=) — yes, the very equality you use everyday — etc. The problem is that if you contribute to a large project written in OCaml and you want to take advantage of abstract types, these functions become your worst enemies because they are breaking the abstraction you were carefully designing. You’ll probably end up as I did finding and removing by hand every occurrence of these magical functions in your code. The following is for you then. Read the rest of this entry »

Set the root directory of a project in Emacs with dir-locals.el

Hi, and welcome to my blog. I’ll try to write here about the stuff I do, use or discover during my work as a Ph.D in Computer Science. There will hopefully be a bit of science (proof theory), some code (functional programming), some tips and tricks for developers.

For a gentle start, I’d like to share a nice little trick I put together for Emacs. I am developing in a big project (Coq) with multiple subdirectories, which compilation is managed by GNU make. When I open a file in a subdirectory and then hit M-x compile, make complains because I am now in the subdirectory and not at the root of the project anymore. So I took the habit for hitting very fast M-x cd .. every time I open a new file in a subdirectory. Annoying… Read the rest of this entry »