Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics

TL;DR

This paper introduces a language-independent method for sound reasoning about iteration and recursion in programming languages, based on big-step semantics, with formal proofs and implementation in Coq.

Contribution

It presents a novel, language-agnostic approach for reasoning about iteration and recursion using big-step semantics, with formal proofs and Coq mechanization.

Findings

Proved soundness and relative completeness of the reasoning technique

Applied the method to simplified imperative and functional languages

Mechanized formal results in the Coq proof assistant

Abstract

A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construction of a separate soundness proof is often a laborious undertaking. In language-independent program verification, common aspects of computer programs are addressed to enable sound reasoning for all languages. In this work, we propose a solution for the sound reasoning about iteration and recursion based on the big-step operational semantics of any programming language. We give inductive proofs on the soundness and relative completeness of our reasoning technique. We illustrate the technique at simplified programming languages of the imperative and functional paradigms, with diverse features. We also mechanism all formal results in the Coq proof assistant.