Learn IRIS

Start Here#

• Getting Started — Install IRIS and write your first program
• Language Guide — Syntax, types, functions, pattern matching, and modules

Tools & Ecosystem#

• Tooling — iris-native, iris-build, and the self-hosted compiler pipeline
• Standard Library — Built-in modules: math, collections, I/O, strings

Architecture & Performance#

• Architecture — Compilation pipeline, native VM, self-hosting
• Benchmarks — Performance measurements against C, OCaml, Haskell, and CPython

Reference#

• Type System — Gradual types, refinement types, contracts, cost annotations
• Verification — LCF proof kernel, graded verification, Lean 4 formalization
• Primitive Reference — All built-in functions with types and examples
• Formal Reference — EBNF grammar, opcodes, effect tags