A tutorial describing most of the syntactic constructs of IPL.
A solution to the first Project Euler problem in IPL.
An implementation of the Fibonacci function, and a solution to the second Project Euler problem.
A partial implementation of a problem from the Language Shootout: also demonstrates how classes can be implemented in IPL.
Some examples of how high level constructions in type theory are compiled to clean LLVM.
Describes IPL's approach to modules.
Describes the difference between definitional and propositional equality.
Proof assistants often use unary arithmetic: this does not work in IPL as recursive datatypes are not supported. However, unary arithmetic can be approximated using interfaces and procedures.
IPL's pedigree includes intuitionistic type theory: some theorems in type theory can be directly implemented in IPL. One prominent example is Hedberg's theorem.