Formal denotational semantics in Homotopy Type Theory

» Apply now PDF Show all positions

Abstract

Voevodsky’s Homotopy Type Theory is an expressive logical framework for the development of formalized mathematics, in particular homotopy theory and higher category theory. This PhD project explores applications of Homotopy Type Theory to denotational semantics of programming languages. Supervisor: Niccolò Veltri Co-supervisor: Tarmo Uustalu

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 May 03, 2021 00:00 and May 31, 2021 23:59 (Europe/Zurich)

Description

The goal of this project is the development of mathematical structures for programming semantics in Homotopy Type Theory (HoTT), crucially employing higher inductive types and HoTT’s characteristic view of types as geometric spaces. The project will mainly study the denotational semantics of programming languages with support for nondeterministic/concurrent behaviour, such as process calculi and transition-based systems. Geometric models of concurrency in the style of Fajstrup, van Glabbeek, Goubault, Mimram et al. will also be investigated. The results will be formalized in proof assistants with support for Homotopy Type Theory, such as Cubical Agda.

Supervisor: Niccolò Veltri
Co-supervisor: Tarmo Uustalu
Name of the department or research group: Laboratory for High-Assurance Software

Responsibilities and tasks:

  • research on this PhD project
  • the PhD student may have to contribute to the teaching activities of the lab as a course assistant

Applicants should fulfill the following requirements:

  • MSc degree in mathematics or computer science
  • knowledge in at least one and interest in all of the following: semantics of programming languages, category theory, certified programming, formalized programming theory