Code Extraction

Groupoid Infinity Targets


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

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 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 chat.