From a practical point of view, we develop Erlang with Dependent Types. Thus we carefully integrate with Erlang platform by generating Erlang AST and trying to be compatible with Erlang kernel through mapping of inductive types to underlying Erlang primitives such as process, receive, and spawn. Erlang extraction is sponsored and supported by Synrc Research Center. Extraction in other languages could also be easily implemented.
Another branch of research is dedicated to evaluation of LLVM lambda generation. It could be direct MIR or LLVM generation, or we could generate Rust/C++ code that could be passed to LLVM optimizer. If you are interested in LLVM target, please take a look at github.com/nponeccop/HNC.
|Infinity Language||Language with HIT|
|MORTE Base Library / System F||Generic Base Library|
|HNC / System F||OM / CoC||Intermediate Languages|
|LLVM Compiler||Jit Interpreter||Execution Environments|
We are very interested in compilation to FPGA. As was shown with interaction nets it is possible to compact packaging of inductive construction in silicon, giving back the inner language of space to the natural encoding. If you are interested in moving this project forward and have a vision how to do it please drop us a line in gitter.im/groupoid/exe chat.