5 votes
Accepted

Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?

Here are the systems/languages I know of for representing these kinds of problems at a higher level of abstraction: The Z3 solver has higher-level constructs for words (fixed-length bit-strings), ...
D.W.'s user avatar
  • 12.1k
4 votes
Accepted

Is beta normalization used for program optimization?

Short answer: $\beta$-reduction is done like crazy in any modern optimizing compiler. As you can easily check e.g. for GHC. The caveat is that $\lambda$s usually serve no useful purpose in the ...
cody's user avatar
  • 13.9k
4 votes

Locally nameless representation implementation

Locally nameless discipline is important when one has to normalize expressions with free variables. This happens in dependent type theories, where equality of types is tangled up with equality of ...
Andrej Bauer's user avatar
  • 28.9k
3 votes

Generating grammar from a string

You might be interested in Sequitur (given a single string, it compresses it by finding a grammar that generates just that one string) or in grammar induction (given a set of strings, it finds a ...
D.W.'s user avatar
  • 12.1k

Only top scored, non community-wiki answers of a minimum length are eligible