Thesis supervisor: Ambrus Kaposi
Location of studies (in Hungarian): ELTE IK Abbreviation of location of studies: ELTE
Description of the research topic:
Dependent type theory is a programming language in which the type of a program can be seen as a mathematical proposition and a program can be seen as the proof of the corresponding type. Martin-Löf type theory is equipped with an equality type which expresses equality of two programs. This type is inductively defined and has the deficiency that programs which provide the same output for the same input cannot be proven equal. Also, logically equivalent propositions are not equal. If we add these properties as axioms to type theory, we lose the ability of running all programs. The goal of our project is to extend type theory with rules which add these properties while retaining computation. Our inspiration is the setoid model of type theory in which a type is interpreted by a set and an equivalence relation representing its equality. Setoid type theory would be an implementation of the lowest (set-level) of homotopy type theory.
The exact details of the topic will be discussed with the prospective student.
Required language skills: English Number of students who can be accepted: 1
Login
