Overview

The Pangolin programming language is a functional language. In this language, the programmer can write logic assertions about the computed values. These assertions are proven statically, which ensures that the program is correct with respect to its specification.

Installation

Requirements

To compile Pangolin, you need:

• the latest Objective Caml compiler, ocaml-3.10.
• the latest version of menhir (tarball).
• the latest version of alphaCaml (tarball).

To handle proof obligations, Pangolin uses:

• the latest version of Ergo.
• optionally the latest version of Simplify (in the ESC/Java package).
• the latest version of Coq.

Instructions

Download the source code and follow the usual sequence:

# ./configure
# make