| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-23 | New IR in VM: Clambda. | Maxime Dénès | |
| This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |