Enhancing Proof Development in Liquid- Haskell: Implementation and Evaluation of Typed Holes
| dc.contributor.author | De Sousa Bernardo, Matheus | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data och informationsteknik | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering | en |
| dc.contributor.examiner | Seger, Carl-Johan | |
| dc.contributor.supervisor | Kovács, András | |
| dc.date.accessioned | 2026-01-09T12:08:18Z | |
| dc.date.issued | 2025 | |
| dc.date.submitted | ||
| dc.description.abstract | Refinement type systems provide mechanisms for specifying and verifying programs beyond what mainstream type systems can express. LiquidHaskell extends Haskell with refinement types, and beyond that, has evolved to be used as a theorem prover, akin to Agda or Idris. Unfortunately, it lacks a fundamental feature present in most proof assistants: the ability to inspect goals during proof development, for example, with typed holes. In this thesis, I implement typed hole support for LiquidHaskell addressing this limitation and taking an initial step towards more interactivity in LiquidHaskell. | |
| dc.identifier.coursecode | DATX05 | |
| dc.identifier.uri | http://hdl.handle.net/20.500.12380/310857 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Refinement types | |
| dc.subject | LiquidHaskell | |
| dc.subject | typed holes | |
| dc.subject | proof assistants | |
| dc.subject | interactive development | |
| dc.subject | type-driven development | |
| dc.subject | program verification | |
| dc.title | Enhancing Proof Development in Liquid- Haskell: Implementation and Evaluation of Typed Holes | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master's Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |