From the practical point of view, we are developing Erlang with Dependent Types. Thus we carefully integrate into Erlang platform by the generation of 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. Other interpreter targets are also could be easily integrated.
The other line of research is dedicated to evaluation of LLVM lambda generation. It could be direct MIR or LLVM generation, or we can generate Rust/C++ code that will bypass to LLVM optimizer. If you are interested in LLVM target, please take a look onto 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 highly interested in compilation to FPGA target. As was shown with interactions 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 boosting this project forward and have a vision how to do it please drop us a line at gitter.im/groupoid/exe public.