Proof theory of ultrasubstructural logics and its applications to programming semantics
» Apply now PDF Show all positions
Abstract
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.
| Research field: |
Information and communication technology |
|---|---|
| Supervisors: |
Dr. Tarmo Uustalu Dr. Niccoló Veltri |
| Availability: | This position is available. |
| Offered by: |
School of Information Technologies Department of Software Science |
| Application deadline: | Applications are accepted between June 01, 2020 00:00 and July 03, 2020 23:59 (Europe/Zurich) |
Description
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
Qualifications
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