Repository logo
 
Thumbnail Image
Publication

Experimental Evaluation of Formal Software Development Using Dependently Typed Languages

2019Conference object Unknown
http://hdl.handle.net/10400.22/14585
Use this identifier to reference this record.

Authors

Tamasi, Ferenc

Advisor(s)

Abstract(s)

We 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.

Description

Keywords

Formal software development Dependent types Coq Iris Agda Fstar ST monad Hoare monad Dijkstra monad

URI

http://hdl.handle.net/10400.22/14585

Pedagogical Context

Citation

Research Projects

Organizational Units

Journal Issue

Publisher

Collections

ISEP – CISTER – Comunicações em eventos científicos

CC License