Anja Petković Komel (original) (raw)

About me

I am a researcher in the formal verification team of the Argot Collective. My main research interests lie in automated theorem proving and type theory, and its applications to blockchain protocols.

Publications and talks

Peer-reviewed conferences and journals

Preprints

International seminars (mostly peer-reviewed)

Employment

Experience and service

Software

act is a high-level specification language for EVM programs and a verification framework to prove properties of smart contracts. Its verification backends enable automated proof of equivalence to EVM bytecode and an extraction of smart contract as a state transition system to interactive theorem provers (Rocq, Lean) to enable expressing and proving invariants of smart contracts. The framework is designed to be extensible to other verification backends (SMT checks, CheckMate).

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

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.

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:

In a similar fashion I thought the material at Oregon Programming Languages Summer School (OPLSS 2025), the materials and videos available here.

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

I was a TA for master students of informatics.

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.

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.

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.

Education

My PhD thesis

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

I was a PhD student ofAndrej Bauer atFaculty 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.

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.

Elaboration

Equality checking
Equality checking

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.