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

Tag: incremental

My thesis is out!

At last! The definitive, final and comprehensive version of my thesis manuscript is out. I defended it on April 8 in Bologna, Italy, and received both titles of “Dottore di ricerca” and “Docteur” in Computer Science, with great pride and relief. What an adventure! You can find my manuscript on my web page, precisely here; it’s called Certificates for incremental type-checking, and after much hesitation, I chose a blue cover for its printed version (it was a tough choice). It is already a little bit obsolete since I compulsively worked on that material even after its submission to avoid the baby blues, but I will nonetheless advertise it here, and eventually write about my advances in future posts. In short, if you are interested in proof certificates, manipulation of proof objects in a functional language, spine-form LF, incremental type-checking, contextual type theory, or the relationship between natural deduction and the sequent calculus, you might be interested in some parts of my manuscript.

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 »