Publicação
Experimental Evaluation of Formal Software Development Using Dependently Typed Languages
| dc.contributor.author | Tamasi, Ferenc | |
| dc.date.accessioned | 2019-09-12T14:52:28Z | |
| dc.date.available | 2019-09-12T14:52:28Z | |
| dc.date.issued | 2019 | |
| dc.description.abstract | 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. | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.isbn | 978-972-752-243-9 | |
| dc.identifier.uri | http://hdl.handle.net/10400.22/14585 | |
| dc.language.iso | eng | pt_PT |
| dc.peerreviewed | yes | pt_PT |
| dc.relation.publisherversion | https://web.fe.up.pt/~prodei/dsie19/assets/Proceedings/DSIE_Procedings2019.pdf | pt_PT |
| dc.subject | Formal software development | pt_PT |
| dc.subject | Dependent types | pt_PT |
| dc.subject | Coq | pt_PT |
| dc.subject | Iris | pt_PT |
| dc.subject | Agda | pt_PT |
| dc.subject | Fstar | pt_PT |
| dc.subject | ST monad | pt_PT |
| dc.subject | Hoare monad | pt_PT |
| dc.subject | Dijkstra monad | pt_PT |
| dc.title | Experimental Evaluation of Formal Software Development Using Dependently Typed Languages | pt_PT |
| dc.type | conference object | |
| dspace.entity.type | Publication | |
| oaire.citation.conferencePlace | Porto, Portugal | pt_PT |
| oaire.citation.endPage | 19 | pt_PT |
| oaire.citation.startPage | 12 | pt_PT |
| oaire.citation.title | Proceedings of the 14th Doctoral Symposium in Informatics Engineering | pt_PT |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | conferenceObject | pt_PT |