|"Translating" (some of) the formalization of NLC from Coq to Agda|
|Kokkuvõte||"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.
https://www.labri.fr/perso/casteran/CoqArt/ (the French ver is freely available)
|Lõputöö kaitsmise aasta||2018-2019|
|Suhtlemiskeel(ed)||eesti keel, inglise keel|
|Märksõnad||#Agda #Coq #natural_language #formalization|