Introduction to PAF!, a proof assistant for ML programs verification We present here a proof assistant dedicated to the proof of ML programs. This document is oriented from a user’s point of view. We introduce the system progressively, describing its features as they become useful, and justifying our choices all along. par Our system intends to provide a usual predicate calculus to express and prove properties of functional ML terms including higher order functions with polymorphic types. To achieve this goal, functional expressions are embedded in the logic as first class terms, with their usual syntax and evaluation rules.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Maingaud, Séverine; Balat, Vincent; Bubel, Richard; Hähnle, Reiner; Miquel, Alexandre: Specifying imperative ML-like programs using dynamic logic (2011)
- Baro, Sylvain: Introduction to PAF!, a proof assistant for ML programs verification (2004)