alain
alain
Currently in dcalc, we have an anotation on each scope let biding indicating what kind is it. This was required for the compilation without exceptions (#158) since some but not...
To simplify the internals of the Catala compiler, it should be possible to use the "a la carte" framework. The main idea behind "a la carte" is to split the...
This is the first attempt to build a Coq backend for Catala, and it is in a very early stage of development. Currently, there isn't much in this file; it...
Currently we use custom printers when doing code generation. This is quite error-prone since it makes it possible to generate nonsense code. For example, ocaml code is printed in two...
derive should generate functoriality properties for param1 translation of non-inductive predicates
ocaml version: 4.14.0 Coq version : 8.16.1 coq-elpi version: 1.15.6 I'm trying to synthesize induction principles for terms builds using Autosubst using coq-elpi's derive. Here is a minimal example with...
Dear Bindlib maintainers, We are using your library in Catala and we are very happy about it. However, while trying to implement heuristics for some optimization scheme, we find that...
This pull request aims to give access to GLPK parameters from the lp-glpk backend. Most parameters were already accessible from the lp-glpk-js backend but not from lp-glpk. I needed the...
# Overview This proposal suggests a design enhancement for the default calculus, which could improve the compilation process and increase the language's expressiveness. # Motivation The idea comes from a...