arvutiteaduse instituudi lõputööde teemade register


"Translating" (some of) the formalization of NLC from Coq to Agda
Organisatsiooni nimikeeletehnoloogia
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.

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)
Lõputöö kaitsmise aasta2018-2019
JuhendajaErkki Luuk
Suhtlemiskeel(ed)eesti keel, inglise keel
Nõuded kandideerijale
Tase Bakalaureus
Märksõnad #Agda #Coq #natural_language #formalization
Kandideerimise kontakt
Nimi Erkki Luuk
Tel
E-mail erkkil@gmail.com


ati.study@lists.ut.ee