A New Synthesis Tool for Agda

dc.contributor.authorSkystedt, Lukas
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerJohansson, Moa
dc.contributor.supervisorNorell, Ulf
dc.date.accessioned2022-10-14T12:26:16Z
dc.date.available2022-10-14T12:26:16Z
dc.date.issued2022sv
dc.date.submitted2020
dc.description.abstractAgda is a dependently typed functional programming language and proof assistant based on constructive type theory. Agda programmers spend most of their time working with unfinished programs where uncompleted parts are marked by holes. These holes can stand for anything from the core, complex parts of the program to trivial details. To allow programmers to focus on the complex parts of the program, Agda includes a synthesis tool called Agsy that can automatically fill in simple holes. Alas, the development of Agsy has not kept up with the evolution of Agda. Hence, Agsy fails to fill some trivial holes. This report describes a replacement for Agsy, named Mimer. To explain the methods used by Mimer, it also presents synthesis algorithms for two simple languages with meta-variables. The first is a simply typed A-calculus with products and sums. The second is a dependently typed A-calculus.sv
dc.identifier.coursecodeDATX05sv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/305712
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.titleA New Synthesis Tool for Agdasv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH

Ladda ner

Original bundle

Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
CSE 22-103 Skystedt.pdf
Storlek:
1.28 MB
Format:
Adobe Portable Document Format
Beskrivning:

License bundle

Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.51 KB
Format:
Item-specific license agreed upon to submission
Beskrivning: