From obj to ml to coq

Jacek Chrząszcz

Jean-Pierre Jouannaud

pp. 216-234

in: Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer (eds), Algebra, meaning, and computation, Berlin, Springer, 2006

Abstract

Rigorous program development is notoriously difficult because it involves many aspects, among which specification, programming, verification, code reuse, maintenance, and version management. Besides, these various tasks are interdependent, requiring going back and forth between them. In this paper, we are interested in certain language features and in languages which help make the user's life easier for developing programs satisfying their specifications.