|Porting a type system from Coq to other functional language(s)|
|Organisatsiooni nimi||ATI keeletehnoloogia|
|Kokkuvõte||Porting 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.
#Coq #natural_language #type_system #formalization #functional_languages
|Lõputöö kaitsmise aasta||2019-2020|
|Suhtlemiskeel(ed)||eesti keel, inglise keel|
|Märksõnad||#Coq #natural_language #type_system #formalization #functional_languages|