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

Organisatsiooni nimi
keeletehnoloogia
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 aasta
2018-2019
Juhendaja
Erkki 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