"Translating" (some of) the formalization of NLC from Coq to Agda

Organization
keeletehnoloogia
Abstract
"Translating" (some of) the formalization of NLC from Coq to Agda (BSc)

The Coq code w/ the formalization is at https://gitlab.com/eluuk/nlc. The "translation" does not have to be exact in the sense that it can follow other patterns and categories than those specified at https://gitlab.com/eluuk/nlc. The work would require you to know or learn both some Coq and Agda. As it would be probably the first time anyone has used Agda in NL modeling, the work is technically novel but not very difficult, as Coq and Agda are quite similar. The main goal would be to see if NL formalization would be easier to do in Agda than in Coq.

http://wiki.portal.chalmers.se/agda
http://www.morganclaypoolpublishers.com/catalog_Orig/samples/9781970001259_sample.pdf
https://www.researchgate.net/publication/316859028_Verified_Functional_Programming_in_Agda
https://coq.inria.fr/distrib/current/refman/
https://www.labri.fr/perso/casteran/CoqArt/ (the French ver is freely available)
Graduation Theses defence year
2018-2019
Supervisor
Erkki Luuk
Spoken language (s)
Estonian, English
Requirements for candidates
Level
Bachelor
Keywords
#Agda #Coq #natural_language #formalization

Application of contact

 
Name
Erkki Luuk
Phone
E-mail
erkkil@gmail.com