Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Comparing Verification of List Functions in LiquidHaskell and Idris
KTH, School of Electrical Engineering and Computer Science (EECS).
KTH, School of Electrical Engineering and Computer Science (EECS).
2019 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesisAlternative title
Verifiering av listfunktioner i LiquidHaskell och Idris, en jämförelse (Swedish)
Abstract [en]

Formal verification is important for guaranteeing correctness of critical computer programs. LiquidHaskell and Idris are 2 functional programming languages in which formal verification can be performed using the respective type systems. This thesis investigates the differences between LiquidHaskell and Idris when verifying list functions, with respect to expressiveness, annotation overhead and type checking times. The used list functions, as well as their specifications consisting of correctness properties, were carefully selected. No large differences in expressiveness were found between LiquidHaskell and Idris. However, Idris was found to be better than LiquidHaskell without the automation feature PLE, regarding annotation overhead and type checking times. With PLE enabled, no large differences were found.

Abstract [sv]

Formell verifiering är viktigt för att garantera korrekthet av kritiska datorprogram. LiquidHaskell och Idris är 2 funktionella programmeringsspråk där formell verifiering kan göras med hjälp av språkens typsystem. Denna uppsats undersöker skillnaderna mellan LiquidHaskell och Idris vid verifiering av listfunktioner, gällande expressiveness, annotation overhead och typechecking tider. De använda listfunktionerna och tillhörande specifikationer bestående av korrekthetsegenskaper, valdes omsorgsfullt. Resultaten visade inte på några stora skillnader gällande expressiveness mellan LiquidHaskell och Idris. Gällande annotation overhead och typechecking tider visades Idris vara bättre än LiquidHaskell utan automatiseringsfunktionen PLE. Med PLE visade resultaten inte på några stora skillnader.

Place, publisher, year, edition, pages
2019.
Series
TRITA-EECS-EX ; 2019:328
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-255160OAI: oai:DiVA.org:kth-255160DiVA, id: diva2:1338661
Subject / course
Computer and Systems Sciences
Supervisors
Examiners
Available from: 2019-07-29 Created: 2019-07-23 Last updated: 2019-07-29Bibliographically approved

Open Access in DiVA

fulltext(567 kB)31 downloads
File information
File name FULLTEXT01.pdfFile size 567 kBChecksum SHA-512
59c391232d119b0f483eb1fd222b835b9dfd5c775dac119363cd99a29a1cd7f23a488b9ea57c14e541f363aa310dbc2a481088a93e5fa017268240c77551619b
Type fulltextMimetype application/pdf

By organisation
School of Electrical Engineering and Computer Science (EECS)
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 31 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 115 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf