tutorial.ipl

A tutorial describing most of the syntactic constructs of IPL.

euler.ipl

A solution to the first Project Euler problem in IPL.

fibonacci.ipl

An implementation of the Fibonacci function, and a solution to the second Project Euler problem.

methcall.ipl

A partial implementation of a problem from the Language Shootout: also demonstrates how classes can be implemented in IPL.

compilation.ipl

Some examples of how high level constructions in type theory are compiled to clean LLVM.

modules.ipl

Describes IPL's approach to modules.

equality.ipl

Describes the difference between definitional and propositional equality.

unary_arithmetic.ipl

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.

hedbergs_theorem.ipl

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.