From OBJ to ML to Coq
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. We are interested here in certain
language features and in languages which help make the user's life
easier for developing programs satisfying their specifications. Our
interest focuses on three implemented specification/programming
languages, OBJ, ML and Coq, which all contributed to a better
understanding of abstractions in modern programming languages such as
types, modules and functors.
full paper