» 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: Tarmo Uustalu
Niccoló Veltri
Availability: This position is available.
Offered by: 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)

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