証明用プログラミング言語

主に数学の定理証明や形式検証に使われ，論理的厳密性を重視します．

Microsoft Researchが開発した証明支援システム兼関数型プログラミング言語