Singleton types for code inference, continued
- December 30, 2012
In this post you can find out what was cut from the previous post on singleton types. These are more technical considerations that may require some familiarity with type theory. In particular, I’ll discuss linear and dependent types in the context of describing more and more singletons.
Singleton types for code inference
- December 29, 2012
- Last updated on 2012/12/30
Could the compiler guess a part of the program I am currently writing? It’s impossible in general, but it may be possible, and hopefully interesting, in special cases. For a start, I am interested in a situation where there is only one possibility: at the expected type, there is only one possible program – modulo (an approximation of) program equivalence.
In a fixed environment, a type is a singleton type if it has only one inhabitant. How widespread are those? Would a language feature to infer their inhabitants be useful? Can we have more interesting singleton types by enriching the type system?
Don’t expect a structured story with a happy ending: this is only a writing-ideas-down session for something I have been thinking about lately.
OCaml compiler optimizations: we need a representative benchmark suite
- December 18, 2012
- Last updated on 2012/12/20
Verifying a parser for a C compiler (continued)
- December 7, 2012
- Last updated on 2012/12/07
In my last post, I explained my work on verifying a parser for Compcert. I was mainly explaining the solutions I found to my performances problems. Here, I will discuss an other interesting problem I have, concerning the context sensitivity of the C99 grammar.
Emancipate yourself from LTac: Your first Coq plugin
- December 5, 2012
- Last updated on 2012/12/06
I recently started a post-doc in the Gallium team, and it is past due-time for my first blog post. I will not start with a research oriented blog right now (but stay tuned!); and I will rather talk about one of my hobbies: writing Coq plugins in OCaml to build new tactics. I reckon that this deviates a bit from standard practice, so I will try to make things clear.
Performance improvements in the universe checker of Coq
- December 3, 2012
One of my parsing-related
Coq files takes more than two hours to compile, which is pretty annoying
when the file is less than one thousand lines long and does no complex
computations. After some profiling, it appeared that Coq was spending
most of its time in the
Univ module. This module is part of the
Coq kernel, its role is to check that the user is using universes in a
Fixing stack overflows using continuations
- December 1, 2012
Just a few weeks ago, Andrej Bauer wrote two articles ( 1 2 ) about implementing a dependent type theory in Ocaml. In particular, he demonstrates a cool idea to normalize expressions, called « normalization by evaluation ».
However, when trying to evaluate 220, the program overflows the stack. It turns out that there is an easy and methodic way to locate and fix such problems, which we will discuss in that post.