arvutiteaduse instituudi lõputööde teemade register


Porting a type system from Coq to other functional language(s)
Organisatsiooni nimiATI keeletehnoloogia
KokkuvõtePorting a type system from Coq to other functional language(s) (BSc/MSc)

The goal would be to experiment with different functional languages to see which one(s) are better suited for implementing NLC† and natural language (NL) in general. NLC is a type system for NL compositionality. The example implementation of NLC in Coq is at https://gitlab.com/eluuk/nlc. The other functional language(s) could be e.g. Agda, Lean, OCaml, Haskell, F#, F*, TypeScript or Idris. The student and supervisor will jointly decide which language(s) to choose. The porting may use other patterns and categories than those in the gitlab project. Depending on the number of analyzed languages and the extent of the analysis, this could be a BSc or MSc thesis topic.

The work would require you to know or learn some functional languages (including Coq), and presents a great deal of technical novelty, as it may be the first time anyone has used the chosen language(s) for NL modeling. On the other hand, the task is simplified by most functional languages being quite similar. A knowledge of Estonian is a plus (but not required), as the system may be also tested on Estonian examples.

† http://ut.ee/~el/pubs/dev_lopstr
https://coq.inria.fr/distrib/current/refman/
https://www.labri.fr/perso/casteran/CoqArt/

Erkki Luuk
erkkil@gmail.com
#Coq #natural_language #type_system #formalization #functional_languages
Lõputöö kaitsmise aasta2019-2020
JuhendajaErkki Luuk
Suhtlemiskeel(ed)eesti keel, inglise keel
Nõuded kandideerijale
Tase Bakalaureus, Magister
Märksõnad #Coq #natural_language #type_system #formalization #functional_languages
Kandideerimise kontakt
Nimi Erkki Luuk
Tel
E-mail erkkil@gmail.com
Kuulutus PDF kuulutus


ati.study@lists.ut.ee