Code Extraction

Groupoid Infinity Targets


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

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