Proof theory of ultrasubstructural logics and its applications to programming semantics
Intuitionistic linear logic is an important “substructural” formalism in the semantics of programming languages. This PhD project is about the proof theory, semantics and applications of yet weaker logics.
Information and Communication Technology|
|Availability:||This position is available.|
School of Information Technologies
Department of Software Science
|Application deadline:||Applications are accepted between September 01, 2020 00:00 and October 02, 2020 23:59 (Europe/Zurich)|
The goal of this project is to work out the proof theory and type theory of certain ultrasubstructural logics, with the view to applications in programming languages. By “ultrasubstructural”, we mean logics weaker than intuitionistic linear logic, such as the logic of skew monoidal categories in the sense of Szlachányi and related logical systems. These are “resourceaware” logics with very fine control over how resources can be consumed. The corresponding type theories can therefore be expected to yield designs for programming languages with fine control of resources.
Responsibilities and tasks:
- The student’s primary responsibility is research on this PhD project
- The student may have contribute to the teaching activities of the lab as a course assistant
Candidates must have a MSc degree in computer science, mathematics or philosophy (logic).
The successful candidate is knowledgeable in at least one and interested in all of the following:
- logic (proof theory)
- functional programming
- semantics of programming languages
- program analysis
- certified programming
- formalized programming theory