Code Extraction

Groupoid Infinity Targets

Interpreters

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.

LLVM

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 LanguageLanguage with HIT
MORTE Base Library / System FGeneric Base Library
HNC / System FOM / CoCIntermediate Languages
C++RustOErlangTarget Languages
LLVM CompilerJit InterpreterExecution Environments

FPGA

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.