# PML 2 : Integrated Program Verification in ML

## TL;DR

PML 2 introduces a unified ML-like language that integrates programming and proof verification, supporting complex features like recursion, subtyping, and classical logic control, with proof management handled automatically by the type-checker.

## Contribution

It presents PML 2, a novel language combining programming and proof capabilities in an ML-like setting with advanced type features and automated proof management.

## Key findings

- Supports equational reasoning with automatic proof checking
- Handles general recursion and subtyping in proofs
- Simplifies proof development by automating equality management

## Abstract

We present the PML 2 language, which provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).