Project Requirements:

  • 1-2 page abstract in PDF format on the topic submitted by the 1.05. The abstract should provide an overview of the practical work with main results being brought out. It may and should include formulas, rules, etc if they are the main results.
  • Practical part (including code, documentation, papers, etc) submitted by the 1.05.
  • Demonstration slides in PDF format submitted by the 1.05
  • Demonstration is at most 20 minutes long, with 5 minutes reserved for questions (including questions from lecturers).
  • Demonstrations can be in English or Estonian, though English is preferred.
  • Documentation and papers should be in English, unless there is a good reason to do them in Estonian.
  • Note that failure to comply with deadlines may result in additional work being required.

Project Topics

Typechecker for PHP Subset (Indrek Täht, Jaanus Tiivoja)

Write a typechecker that will reject invalid PHP programs. The typechecker does not have to be safe (that is typeable programs do not have to execute succefully), but it should reject at least some variants of invalid programs. You can use existing parsers, interpreters, etc, and can write the typechecker in any language, including PHP.

Since PHP is a complex language you can also typecheck only its subset, omitting the more complex constructions.

Since PHP is a dynamic language it will be impossible to fully type it, and thus you'll have to assign Bot type to many terms and use subsumption to promote it to the right type.

Using C library function attributes as type-annotations for improving the precision of static analysis (Toomas Römer)

C library functions have a large number of different attributes attached to them, e.g const, pure and malloc. These can be interpreted as monadic effect types and used to help static analyzers when dealing with library functions.

The goal is not to prove any soundness theorem, but use ideas from type theory to design a clean interface for describing functions whose implementation are not available for analysis.

Add local type inference to Java

Polyglot Java Compilation Framework

Typechecker for Javascript subset

See PHP for details

Typechecker for PHP subset

Research and implement the possibility of programming generic (aka polytypic) programs in Scala.

Implement a typechecker and an interpreter for Types Systems full language in Scala

Implement an interpreter and a typechecker for the full language supporting lambda calculus, simple and advanced extensions, recursive types and full higher order polymorphism for the example language used in Type System lectures.