June 2, 2017

This week has been shared between a lot of easy fun putting together all the pieces that I worked on during the last weeks, and a lot of frustration trying to prove the soundness of the system.

Implementation

After several weeks spent trying to understand the API of CDuce − the language our type-system takes it inspiration from and whose code we planned to reuse as much as possible to ease the Implementation −, I eventually understood it enough to start using it for writing the inference engine.

This has been really enjoyable, as all I had to do was plugging together a few functions that where already dealing with all the boring low-level stuff, and everything has been almost instantly working. I could quickly write a prototype of typer for the core lambda-calculus of the language. It is still a little bit too rough on the edges to be presented, but I should (hopefully) be able to present some nice examples for next week.

On the theoretical side

I talked last week about some difficulties with the proof of the soundness of the type-system.

Those difficulties still hold, although some progress has been done. There are a couple of paths that we are currently exploring for a this:

Next week

Next week will be more or less like this one: I'll continue the implementation using all the nice features offered by CDuce. In the same time, I'll keep on working on the proof − I hope that this will be solved before next Friday.

Provided I find the time − which is rather unlikely, but who knows? − I'll also try to make an online demonstration of the engine to show the progress of the implementation.


Commentaires