A carregar...
Publicação
Experimental Evaluation of Formal Software Development Using Dependently Typed Languages
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 211.8 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(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.
Descrição
Palavras-chave
Formal software development Dependent types Coq Iris Agda Fstar ST monad Hoare monad Dijkstra monad