Projects tagged ‘certification’ and ‘proof’

Here is a piece of software related to the paper: Extended Static Checking of Functional Programs We present a Hoare logic for a programming language equipped with recursive, higher-order functions ... [More] , algebraic data types, and a polymorphic type system in the style of Hindley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions. These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactive theorem provers. Although the technical apparatus that we exploit is by now standard, its application to functional programming languages appears to be new, and (we claim) deserves attention. As a sample application, we check the partial correctness of a balanced binary search tree implementation. [Less]

OverviewThe 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 ... [More] ensures that the program is correct with respect to its specification. InstallationRequirementsTo 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. InstructionsDownload the source code and follow the usual sequence: # ./configure # make [Less]