A Mechanized Theory of Program Refinement - Sorbonne Université Access content directly
Conference Papers Year : 2019

A Mechanized Theory of Program Refinement


We present a mechanized theory of program refinement that allows for the stepwise development of imperative programs in the Coq proof assistant. We formalize a design language with support for gradual refinement and a calculus which enforces correctness-by-construction. A notion of program design captures the hierarchy of refinement steps resulting from a development. The underlying theory follows the predicative programming paradigm where programs and specifications are both easily expressed as predicates, which fit naturally in the dependent type theory of the proof assistant.
Fichier principal
Vignette du fichier
sall-peschanski-chailloux-ICFEM2019-submitted.pdf (349.75 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-02367566 , version 1 (18-11-2019)



Boubacar Demba Sall, Frédéric Peschanski, Emmanuel Chailloux. A Mechanized Theory of Program Refinement. ICFEM 2019 - 21st International Conference on Formal Engineering Methods, Nov 2019, Shenzhen, China. pp.305-321, ⟨10.1007/978-3-030-32409-4_19⟩. ⟨hal-02367566⟩
198 View
190 Download



Gmail Mastodon Facebook X LinkedIn More