About me

I am a postdoctoral researcher under Laura Kovács in the FORSYTE group of informatics department of TU Wien in Vienna, Austria. My main research interests lie in type theory, its applications to proof assistants, automated theorem proving, its applications to blockchain protocols, and logic.

My PhD thesis

Meta-analysis of type theories with an application to the design of formal proofs

I was a PhD student of Andrej Bauer at Faculty of mathematics and physics, University of Ljubljana. In my thesis, I analyze the meta-theory of type theory and its applications to proof assistants. I focus on two aspects: interactions of type theories via transformations and a general user-extensible equality checking algorithm.

PDF Bibtex

One way of studying compatibility of type theories is by looking at their transformations. To accommodate for the use in proof assistants, the transformations we consider are syntactic in nature, they preserve derivability and are general enough to be applicable to a large class of type theories. The transformations preserve some syntactic structure (like judgement kinds and syntactic classes) and they interact nicely with substitutions of variables and instantiations of metavariables: with the action on expressions they form a relative monad for syntax.

A major use case for our definition of type-theoretic transformation is an elaboration. When designing a type theory, especially for using it in a proof assistant, one often faces a dilemma of how verbose the syntax should be. Terms annotated with full typing information are easily amenable to algorithmic processing and have good meta-theoretic properties. However, the syntax can quickly become too verbose to handle, so more economic terms that omit typing information are much more usable in practice. One can also omit other evidence, like proof of termination for recursive functions, or explicit universe levels. One common solution to this problem is to design two type theories: a fully annotated type theory S (the elaboration) that resides in the kernel of the proof assistant and an economic one T for the users input. The theories are connected via two maps: the retrogression transformation (r) that forgets the additional information, and the elaboration map (l) which uses a derivation to construct the missing data. We then prove two theorems: that elaboration is universal and that every finitary type theory has an elaboration. We also investigate some algorithmic properties of elaboration.

Proof assistants based on type theories have equality checking algorithms as their essential components. The algorithms free the users from proving mostly trivial judgemental equalities, and povide computation-by-normalization engines. Some systems, like Agda and Dedukti, allow the users to extend the built-in equality checkers. However, in a proof assistant that supports arbitrary user-definable type theories, like Andromeda 2, an equality checking algorithm highly depends on the given rules or may not even be available. Still, the proof assistant should provide support for equality checking that is easy to use and works well in the common, well-behaved cases. For this purpose we have developed a sound and extensible equality checking algorithm for user-definable type theories. We implemented it in the Andromeda 2 proof assistant.

An extensible equality checking algorithm for dependent type theories

with Andrej Bauer

Logical methods in computer science

PDF Bibtex Implementation

Publications and talks

Peer-reviewed conferences and journals

Scaling CheckMate for Game-Theoretic Security

with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson

25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)

PDF Bibtex

CheckMate: Automated Game-Theoretic Security Reasoning

with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson

2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023)

PDF Bibtex

Automating Security Analysis of Off-Chain Protocols

with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson

4th International Workshop on Formal Methods for Blockchains

PDF Bibtex Slides

An extensible equality checking algorithm for dependent type theories

with Andrej Bauer

Logical methods in computer science

PDF Bibtex Implementation

Equality Checking for General Type Theories in Andromeda 2

with Andrej Bauer and Philipp G. Haselwarter

7th International Conference on Mathematical Software ICMS (2020)

PDF Bibtex Slides

International seminars (mostly peer-reviewed)

The essence of type-theoretic elaboration

Anja Petković Komel,

Women in Logic, 2022

Abstract Slides

The essence of elaboration

Anja Petković Komel,

Workshop on Syntax and Semantics of Type Thoery, Stockholm, 2022, invited talk

Slides

Towards an elaboration theorem

Anja Petković Komel,

HoTT/UF 2021, invited talk

Slides Video

Equality checking for dependent type theories

Andrej Bauer and Anja Petković Komel

TYPES 2021

Abstract

Equality checking for Finitary type theories

Andrej Bauer, Philipp G. Haselwarter, and Anja Petković

HoTTEST Conference 2020, invited talk

Slides Video

Cancelled On equality checking for general type theories: Implementation in Andromeda 2

Andrej Bauer, Philipp G. Haselwarter, Anja Petković

TYPES 2020

Abstract

Andromeda 2.0

Anja Petković

Stockholm Logic Seminar

Slides Code

Education

2017 - 2021: PhD from Faculty of mathematics and physics, University of Ljubljana.
Thesis title: Meta-analysis of type theories with an application to the design of formal proofs
Thesis adviser: Andrej Bauer
PDF Bibtex
2015 - 2017: Master of Mathematics from Faculty of mathematics and physics, University of Ljubljana, graduated with honors.
Thesis title: Computing fixed points of monotone piecewise linear functions
Thesis adviser: Alex Simpson
PDF Code
2012 - 2015: Bachelor of mathematics from Faculty of mathematics and physics, University of Ljubljana, graduated with honors.
Thesis title: Compactly dominated spaces are homotopy equivalent to compact spaces
Thesis adviser: Jaka Smrekar

Employment

January 2022 - present: Postdoctoral Researcher at Informatics department of TU Wien, Austria with Laura Kovács.
July 2023 - August 2024: Career break: Maternity leave.
October 2017 - December 2021: Researcher & PhD student & TA at Faculty of mathematics and physics, University of Ljubljana, Slovenia with Andrej Bauer.

Teaching

During the three years of my postdoc at TU Wien, I had the chance to teach the students. I was honoured to get to design and lecure the course on type theories, teaching students the basics of type theories as mathematical foundation, as well as formalizing mathematics and software correctness in a proof assistant.

Introduction to type theories (Faculty of Informatics, TU Wien)

I had the honour to present type theories to students of informatics and mathematics at TU Wien. The purpose of this course was to familiarize the students with the concept of a type theory, the most commonly used type theories in practice and how we use type theories in proof assistants. The course fosuced on the mathematical foundation, the type theories and it comprised of the following topics:

Martin-Löf type theory (MLTT) - where we described the most common dependent types and ingredients of type theories.
Agda (proof assistant based on MLTT) - where we got to know how to use MLTT to formalize proofs.
Calculus of inductive constructions (CIC) - where we described the differences and nuances between different type theories.
Coq (proof assistant based on CIC) - where we gdt to know how to use CIC to formalize proofs in the most commonly used proof assistant.
Meta-theory of type theories - where we formally defined a type theory and related it to first-order and other higher-order theories.

The students were graded based on 4 homeworks (two theoretical and two formalizations (one in Coq and one in Agda)) and an oral exam at the end.

Formal methods in infromatics (Faculty of Informatics, TU Wien)

I was a TA for master students of informatics.

In autumn 2023, I marked students' exams.
In spring 2023, I marked students' exams.
In autumn 2022, I marked students' exams.
In spring 2012, I marked students' exams.

During the four years of my PhD I had the chance to teach the students of mathematics and physics at University of Ljubljana. Besides the courses listed below I conducted a workshop on advanced uses of Mathematica. Prior to that I was a tutor and demonstrator for mathematics and analysis courses at Faculty for mathematics and physics, University of Ljubljana.

Logic and sets (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for first year undergraduate mathematics students taking a course on foundations of mathematics: first-order logic and set theory.

In autumn 2020, I was a TA for one group and I marked students' exams.
In autumn 2019, I was a TA for one group and I marked students' exams.
In autumn 2018, I was a TA for one group and I marked students' exams.
In autumn 2017, I was a TA for one group and I marked students' exams.

Introduction to programming (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for first year undergraduate mathematics and financial mathematics students, givng them an introducotry course on programming in python.

In spring 2021, I was a TA for one group and I marked students' exams.
In spring 2020, I was a TA for one group and I marked students' projects.
In spring 2019, I was a TA for one group and I marked students' exams.

Teaching mathematics and physics in English (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for master students in pedagogical mathematics and pedagogical physics. We discussed different approaches to teaching mathematics in English and covered vocabulary for various highschool level topics.

In spring 2021, I was a TA for the course I marked students' coursework.

Experience and service

Software

CheckMate is a framework designed to automatically check security properties of games that arise from off-chain (blockchain) protocols. The framework yields a strategy (if it exists) for the following properties: weak immunity, collusion resilience and practicality.

Andromeda is an implementation of (standard) finitary type theories, allowing the user to define their own type theory. It is based on an ML style meta-language that supports proof development via runners and bidirectional evaluation. It implements a user-extensible equality checkig algorithm.

Community service

Cost action: CA20111 European Research Network on Formal Proofs, management committee, gender balance coordinator.
CPP 2023, programme committee.
HoTT/UF 2023, organizing committee, programme committee, local organiser.
Women in EuroProofNet 2023, organizing committee.
ICFP 2022, organizing committee, virtualization chair.
HoTT/UF 2022, organizing committee.
Women in EuroProofNet 2022, organizing committee.
Women in Mathematics on Mediterranean Shores, Bled, Slovenia, September 2019, organizing committee.

Outreach to society and media

I believe the mission of scientists is not only discovering new science, but also communicating science and science-related issues to others, from fellow scientists to the general public. In the years 2022 and 2023 I helped organise workshops for school children at TU Wien, to help them learn the concept of algorithm in a playful way. In October 2022 I gave a talk about gender balance in computer science for students at ENS Paris-Scalay (slides). In June 2022 I participated at a round table about the profession of a scientist, organized by Slovenian national radio station Val 202 (audio). From September 2019 to January 2022 I posed mathematical riddles at the science show Ugriznimo znanost on Slovenian national television RTVSLO. In March 2020 I gave an interview for Metina Lista science podcasts (audio) and in November 2019 an interview at the occasion of 100. anniversary of University of Ljubljana on Slovenian national radio station Val 202 (audio). In December 2018 I co-organised a round table called Women in Science and Technology (video.) with the collegues from Jožef Stefan Institute.