Project Status

Implemented and Awaiting features of the Om/Inf

Compiler Passes

  1. INF — Macro Expansion
  2. TYPE — Typechecking
  3. NORMAL — Normalization
  4. ERASE — Type Information Erasure
  5. COMPACT — Compress Terms
  6. EXTRACT — Extract VM Lambda

Logic

  1. REC — Recursor
  2. INDUCTION — Dependent Eliminator
  3. EQU — Propositional Equality
  4. SIMPLE — Simplification, K combinator
  5. FREGE — Frege, S combinator
  6. PROP — Propositions

Macros

  1. CASE — Patterm Matching
  2. LET — Extract VM Lambda
  3. DATA — Inductive Definition
  4. RECORD — Coinductive Definition

Base Library

  1. IO — Input/Output Free Monad
  2. IOI — Infinity Input/Output Cofree Comonad
  3. Lazy — Lazy Type
  4. Bool — Boolean
  5. Maybe — Maybe
  6. Nat — Natural Number Object
  7. List — Inductive List
  8. Unit — 0-Tuple
  9. Mon — 1-Tuple
  10. Prod — 2-Tuple
  11. Morte — Recursive and Corecursive samples

Backends

  1. Erlang/OTP — BEAM and LING virual machines.
  2. O — CPS Interpreter.
  3. C++ — clang, HN0
  4. LLVM — LLVM
  5. FPGA — FPGA