Tamasi, Ferenc2019-09-122019-09-122019978-972-752-243-9http://hdl.handle.net/10400.22/14585We will evaluate three dependently typed languages, and their supporting tools and libraries, by implementing the same tasks in each language. One task will demonstrate the basic dependent type support of each language, the other task will show how to do basic imperative programming combined with theorem proving, to ensure both resource safety and functional correctness.engFormal software developmentDependent typesCoqIrisAgdaFstarST monadHoare monadDijkstra monadconference object