Anja Petković: Andromeda 2.0

Tid: On 2019-11-13 kl 10.00 - 11.45

Föreläsare: Anja Petković, University of Ljubljana

Plats: Kräftriket, House 5, Room 16

Abstract

Andromeda 2.0 is a proof assistant in development in which the user can specify a general type theory (in the sense of Bauer, Haselwarter, and Lumsdaine). I will present the main features it supports, how one operates with judgements, defines the rules of the theory, derives the congruence rules etc. We will illustrate these on some standard examples of type formers like dependent sums and products. This is joint work with Andrej Bauer and Philipp G. Haselwarter.

Innehållsansvarig:webmaster@math.kth.se
Tillhör: Institutionen för matematik
Senast ändrad: 2019-11-08