-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
505 lines (491 loc) · 30.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
<!doctype html>
<html>
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width,initial-scale=1">
<title>Anja Petković Komel</title>
<link rel="stylesheet" href="style.css">
</head>
<body>
<header>
<div>
<p> <span class="name">Anja Petković Komel</span> <br/></p>
<p>
<a href="https://www.tuwien.at/en/">TU Wien</a> <br />
Favoritenstrasse 11,
1040 Vienna <br />
<a href='mailto:[email protected]'>
</a> <br />
<a href="https://github.com/anjapetkovic/"><img style="vertical-align:middle" src="img/github-icon.png" width="30" alt="GitHub"><span>anjapetkovic</span></a><br />
<a href="https://bitbucket.org/AnjaPetkovic/"><img style="vertical-align:middle" src="img/bitbucket-icon.jpg" width="30" alt="GitHub">AnjaPetkovic</a><br />
<a href="https://orcid.org/0000-0001-7203-6641"><img style="vertical-align:middle" src="img/orcid.logo.icon.svg" width="30" alt="orcid"><span>0000-0001-7203-6641</span></a>
</p>
</div>
<div>
<a href="img/anja3.jpg"><img src="img/anja3.jpg" width="500" alt="Anja's photo"></a>
</div>
</header>
<nav>
<a href="#aboutMe">About me</a>
<a href="#phd">PhD thesis</a>
<a href="#publications">Publications</a>
<a href="#education">Education</a>
<a href="#employment">Employment</a>
<a href="#teaching">Teaching</a>
<a href="#experience">Experience</a>
</nav>
<main>
<section class="dark" id="aboutMe">
<h1>About me</h1>
<div class="main">
<article>
<p class="main">
I am a postdoctoral researcher under <a href="http://lkovacs.com/">Laura Kovács</a> in the <a href="https://informatics.tuwien.ac.at/orgs/e192-04">FORSYTE</a> group of <a href="https://informatics.tuwien.ac.at/">informatics department</a> of <a href="https://www.tuwien.at/en/">TU Wien</a> 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.
</p>
</article>
</div>
</section>
</section>
<section class="light" id="phd">
<h1>My PhD thesis</h1>
<h2 class="big">Meta-analysis of type theories with an application to the design of formal proofs</h2>
<div class="main column">
<p class="main">
I was a PhD student of
<a href="http://andrej.com">Andrej Bauer</a>
at
<a href="https://www.fmf.uni-lj.si/">Faculty of mathematics and physics,
University of Ljubljana</a>.
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.
</p>
<div class="files">
<a href="img/doctoralThesis.pdf">PDF</a>
<a href="citations/phdthesisbibtex.txt">Bibtex</a>
<!-- <a href="">Defence video</a> -->
</div>
<article>
<div class="content">
<p class="main">
One way of studying compatibility of type theories is by looking at their <span class="keyword">transformations</span>. 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.
</p>
</div>
</article>
<article>
<div class="content">
<p class="main">
A major use case for our definition of type-theoretic transformation is an <span class="keyword">elaboration</span>. 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.
</p>
</div>
<img src="img/diagramElaboration.png" height="200" alt="Elaboration">
</article>
<article>
<div>
<img src="img/diagramEqchk1.png" alt="Equality checking"> <br/>
<img src="img/diagramEqchk2.png" alt="Equality checking">
</div>
<div class="content">
<p class="main">
Proof assistants based on type theories have <span class="keyword">equality checking algorithms</span> 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 <a href="https://www.andromeda-prover.org/">Andromeda 2</a>, 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 <span class="keyword">sound and extensible equality checking algorithm</span> for user-definable type theories. We implemented it in the <a href="https://www.andromeda-prover.org/">Andromeda 2</a> proof assistant.
</p>
<div class="paper">
<h4>
<a href="https://arxiv.org/abs/2103.07397">
An extensible equality checking algorithm for dependent type theories
</a>
</h4>
<p>with Andrej Bauer</p>
<p class="journal">Logical methods in computer science</p>
<div class="files">
<a href="https://arxiv.org/pdf/2103.07397.pdf">PDF</a>
<a href="citations/eqchk-bibtex.txt">Bibtex</a>
<a href="https://github.com/Andromedans/andromeda">Implementation</a>
</div>
</div>
</div>
</article>
</section>
<section class="dark" id="publications">
<h1>Publications and talks</h1>
<div class="main">
<article class="big">
<h2>Peer-reviewed conferences and journals</h2>
<div class="paper">
<h4>
<a href="https://easychair.org/publications/paper/6ZDH">
Scaling CheckMate for Game-Theoretic Security
</a>
</h4>
<p>with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson</p>
<p class="conference">25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)</p>
<div class="files">
<a href="https://easychair.org/publications/paper/6ZDH">PDF</a>
<a href="citations/LPAR2024-bibtex.txt">Bibtex</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://dl.acm.org/doi/10.1145/3576915.3623183">
CheckMate: Automated Game-Theoretic Security Reasoning
</a>
</h4>
<p>with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson</p>
<p class="conference">2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023)</p>
<div class="files">
<a href="https://dl.acm.org/doi/10.1145/3576915.3623183">PDF</a>
<a href="citations/CCS23-bibtex.txt">Bibtex</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://easychair.org/smart-program/FLoC2022/_paper2022868336.pdf">
Automating Security Analysis of Off-Chain Protocols
</a>
</h4>
<p>with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson</p>
<p class="conference">4th International Workshop on Formal Methods for Blockchains</p>
<div class="files">
<a href="https://easychair.org/smart-program/FLoC2022/_paper2022868336.pdf">PDF</a>
<a href="citations/FMBC2022-bibtex.txt">Bibtex</a>
<a href="talks/2022-08-11-FMBC2022/FMBC_talk.pdf">Slides</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://arxiv.org/abs/2103.07397">
An extensible equality checking algorithm for dependent type theories
</a>
</h4>
<p>with Andrej Bauer</p>
<p class="journal">Logical methods in computer science</p>
<div class="files">
<a href="https://arxiv.org/pdf/2103.07397.pdf">PDF</a>
<a href="citations/eqchk-bibtex.txt">Bibtex</a>
<a href="https://github.com/Andromedans/andromeda">Implementation</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://link.springer.com/chapter/10.1007/978-3-030-52200-1_25">
Equality Checking for General Type Theories in Andromeda 2
</a>
</h4>
<p>with Andrej Bauer and Philipp G. Haselwarter</p>
<p class="conference">7th International Conference on Mathematical Software ICMS (2020)</p>
<div class="files">
<a href="https://link.springer.com/content/pdf/10.1007%2F978-3-030-52200-1_25.pdf">PDF</a>
<a href="citations/eqchk-ICMS-bibtex.txt">Bibtex</a>
<a href="talks/2020-07-15-ICMS2020/slides.pdf">Slides</a>
</div>
</div>
</article>
<article>
<h2>International seminars (mostly peer-reviewed)</h2>
<div class="paper">
<h4>
<a href="https://easychair.org/smart-program/Vampire23/Accepted.html">
Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
</a>
</h4>
<p>
Anja Petković Komel, <span class="speaker">Michael Rawson</span>, Martin Suda,
</p>
<p class="conference">The 7th Vamire Workshop, 2023</p>
<div class="files">
<a href="talks/2023-Vampire23/Vampire23abstract">Abstract</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://sites.google.com/g.uporto.pt/wil2022/program">
The essence of type-theoretic elaboration
</a>
</h4>
<p>
<span class="speaker">Anja Petković Komel</span>,
</p>
<p class="conference">Women in Logic, 2022</p>
<div class="files">
<a href="talks/2022-07-31-WIL2022/abstract.pdf">Abstract</a>
<a href="talks/2022-07-31-WIL2022/essence-of-elaboration.pdf">Slides</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://europroofnet.github.io/wg6-kickoff-stockholm/programme">
The essence of elaboration
</a>
</h4>
<p>
<span class="speaker">Anja Petković Komel</span>,
</p>
<p class="conference">Workshop on Syntax and Semantics of Type Thoery, Stockholm, 2022, invited talk</p>
<div class="files">
<a href="talks/2022-05-21-EPNWG6/essence-of-elaboration.pdf">Slides</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://hott-uf.github.io/2021/">
Towards an elaboration theorem
</a>
</h4>
<p>
<span class="speaker">Anja Petković Komel</span>,
</p>
<p class="conference">HoTT/UF 2021, invited talk</p>
<div class="files">
<a href="https://www.icloud.com/keynote/0xQo428lRzMDGsGxDSe-jIUUQ#ElaborationTheorem">Slides</a>
<a href="https://www.youtube.com/watch?v=Rxe7Bk3f5D4&list=PL_XB0KjjROOadsaztXs57E8b-FTBqlcCt&index=4">Video</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://types21.liacs.nl/download/equality-checking-for-dependent-type-theories/">
Equality checking for dependent type theories
</a>
</h4>
<p>Andrej Bauer and <span class="speaker">Anja Petković Komel</span></p>
<p class="conference">TYPES 2021</p>
<div class="files">
<a href="talks/2021-06-17-TYPES2021/abstract.pdf">Abstract</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://types21.liacs.nl/download/ssprove-a-foundational-framework-for-modular-cryptographic-proofs-in-coq/">
Equality checking for Finitary type theories
</a>
</h4>
<p>
Andrej Bauer,
Philipp G. Haselwarter, and
<span class="speaker">Anja Petković</span>
</p>
<p class="conference">HoTTEST Conference 2020, invited talk</p>
<div class="files">
<a href="talks/2020-06-18-HoTTEST2020/eqchk_presentation_HoTTEST2020.pdf">Slides</a>
<a href="https://youtu.be/yHjmPJuTvWM">Video</a>
</div>
</div>
<div class="paper">
<h4>
<span class="cancelled">Cancelled</span>
<a href="https://types2020.di.unito.it/abstracts/BookOfAbstractsTYPES2020.pdf">
On equality checking for general type theories: Implementation in Andromeda 2
</a>
</h4>
<p>Andrej Bauer, Philipp G. Haselwarter, Anja Petković</p>
<p class="conference">TYPES 2020</p>
<div class="files">
<a href="talks/2020-03-03-TYPES2020/eqchk.pdf">Abstract</a>
</div>
</div>
<div class="paper">
<h4>
<a href="https://logic.math.su.se/seminar/">
Andromeda 2.0
</a>
</h4>
<p><span class="speaker">Anja Petković</span></p>
<p class="conference">Stockholm Logic Seminar</p>
<div class="files">
<a href="talks/2019-11-13-StockholmSeminar/andromeda-presentation-Stockholm2019.pdf">Slides</a>
<a href="talks/2019-11-13-StockholmSeminar/index.html">Code</a>
</div>
</div>
</article>
</div>
</section>
<section class="light" id="education">
<h1>Education</h1>
<div class="main">
<article>
<p class="main">
<ul style="font-size: x-large;">
<li>2017 - 2021: PhD from <a href="https://www.fmf.uni-lj.si/">Faculty of mathematics and physics,
University of Ljubljana</a>. <br/>
Thesis title: <span class="keyword"> Meta-analysis of type theories with an application to the design of formal proofs</span><br/>
Thesis adviser: <a href="http://andrej.com">Andrej Bauer</a>
<div class="files">
<a href="img/doctoralThesis.pdf">PDF</a>
<a href="citations/phdthesisbibtex.txt">Bibtex</a>
<!-- <a href="">Defence video</a> -->
</div>
</li>
<li> 2015 - 2017: Master of Mathematics from <a href="https://www.fmf.uni-lj.si/">Faculty of mathematics and physics, University of Ljubljana</a>, graduated with honors. <br/>
Thesis title: <span class="keyword">Computing fixed points of monotone piecewise linear functions</span> <br/>
Thesis adviser: <a href="https://www.fmf.uni-lj.si/si/imenik/32646/">Alex Simpson</a>
<div class="files">
<a href="img/magisterij.pdf">PDF</a>
<a href="https://bitbucket.org/AnjaPetkovic/evaulating-mu-terms">Code</a>
</div>
</li>
<li>2012 - 2015: Bachelor of mathematics from <a href="https://www.fmf.uni-lj.si/">Faculty of mathematics and physics, University of Ljubljana</a>, graduated with honors. <br/>
Thesis title: <span class="keyword">Compactly dominated spaces are homotopy equivalent to compact spaces</span> <br/>
Thesis adviser: <a href="https://www.fmf.uni-lj.si/~smrekar/">Jaka Smrekar</a>
</li>
</ul>
</p>
</article>
</div>
</section>
<section class="light" id="employment">
<h1>Employment</h1>
<div class="main">
<article>
<p class="main">
<ul style="font-size: x-large;">
<li>January 2022 - present: <span class="keyword">Postdoctoral Researcher</span> at <a href="https://informatics.tuwien.ac.at/">Informatics department</a> of <a href="https://www.fmf.uni-lj.si/">TU Wien</a>, Austria with <a href="http://lkovacs.com/">Laura Kovács</a>.
</li>
<li>July 2023 - August 2024: <span class="keyword">Career break</span>: Maternity leave.
</li>
<li>October 2017 - December 2021: <span class="keyword">Researcher & PhD student & TA</span> at <a href="https://www.fmf.uni-lj.si/">Faculty of mathematics and physics,
University of Ljubljana</a>, Slovenia with <a href="http://andrej.com">Andrej Bauer</a>.
</li>
</ul>
</p>
</article>
</div>
</section>
<section class="dark" id="teaching">
<h1>Teaching</h1>
<div class="main">
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.
<article>
<h2>Introduction to type theories (Faculty of Informatics, TU Wien)</h2>
<p>
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:
<ul>
<li> Martin-Löf type theory (MLTT) - where we described the most common dependent types and ingredients of type theories.</li>
<li> Agda (proof assistant based on MLTT) - where we got to know how to use MLTT to formalize proofs.</li>
<li> Calculus of inductive constructions (CIC) - where we described the differences and nuances between different type theories.</li>
<li> 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.</li>
<li> Meta-theory of type theories - where we formally defined a type theory and related it to first-order and other higher-order theories.</li>
</ul>
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.
</p>
</article>
<article>
<h2>Formal methods in infromatics (Faculty of Informatics, TU Wien)</h2>
<p>
I was a TA for master students of informatics.
<ul>
<li>In autumn 2023, I marked students' exams.</li>
<li>In spring 2023, I marked students' exams.</li>
<li>In autumn 2022, I marked students' exams.</li>
<li>In spring 2012, I marked students' exams.</li>
</ul>
</p>
</article>
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.
<article>
<h2>Logic and sets (Faculty of Mathematics and Physics, University of Ljubljana)</h2>
<p>
I was a TA for first year undergraduate mathematics students taking a course on foundations of mathematics: first-order logic and set theory.
<ul>
<li>In autumn 2020, I was a TA for one group and I marked students' exams.</li>
<li>In autumn 2019, I was a TA for one group and I marked students' exams.</li>
<li>In autumn 2018, I was a TA for one group and I marked students' exams.</li>
<li>In autumn 2017, I was a TA for one group and I marked students' exams.</li>
</ul>
</p>
</article>
<article>
<h2>Introduction to programming (Faculty of Mathematics and Physics, University of Ljubljana)</h2>
<p>
I was a TA for first year undergraduate mathematics and financial mathematics students, givng them an introducotry course on programming in python.
<ul>
<li>In spring 2021, I was a TA for one group and I marked students' exams.</li>
<li>In spring 2020, I was a TA for one group and I marked students' projects.</li>
<li>In spring 2019, I was a TA for one group and I marked students' exams.</li>
</ul>
</p>
</article>
<article>
<h2>Teaching mathematics and physics in English (Faculty of Mathematics and Physics, University of Ljubljana)</h2>
<p>
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.
<ul>
<li>In spring 2021, I was a TA for the course I marked students' coursework.</li>
</ul>
</p>
</article>
</div>
</section>
<section class="dark" id="experience">
<h1>Experience and service</h1>
<div class="main">
<article>
<h2>Software</h2>
<p>
<a href="https://github.com/apre-group/checkmate">CheckMate</a> 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.
</p>
<p>
<a href="https://www.andromeda-prover.org/">Andromeda</a> 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.
</p>
</article>
<article>
<h2>Community service</h2>
<ul>
<li><a href="https://hott-uf.github.io/2025/" />HoTT/UF 2025</a>, programme committee.</li>
<li><a href="https://tacas.info/artifacts-25.php" />TACAS 2025</a>, artefact evaluation committee.</li>
<li>Cost action: CA20111 <a href="https://www.cost.eu/actions/CA20111/" />European Research Network on Formal Proofs</a>, management committee, gender balance coordinator. </li>
<li><a href="https://popl23.sigplan.org/home/CPP-2023" />CPP 2023</a>, programme committee, Best Reviewer Award.</li>
<li><a href="https://hott-uf.github.io/2023/" />HoTT/UF 2023</a>, organizing committee, programme committee, local organiser.</li>
<li><a href="https://europroofnet.github.io/women-epn-2023/" />Women in EuroProofNet 2023</a>, organizing committee.</li>
<li><a href="https://womencourage.acm.org/2023/" />Womencourage 2023</a>, poster evaluation committee.</li>
<li><a href="https://icfp22.sigplan.org/" />ICFP 2022</a>, organizing committee, virtualization chair.</li>
<li><a href="https://hott-uf.github.io/2022/" />HoTT/UF 2022</a>, organizing committee.</li>
<li><a href="https://europroofnet.github.io/women-epn-2022/" />Women in EuroProofNet 2022</a>, organizing committee.</li>
<li><a href="https://conferences.matheo.si/event/30/">Women in Mathematics on Mediterranean Shores</a>, Bled, Slovenia, September 2019, organizing committee.</li>
</ul>
</article>
<article>
<h2>Outreach to society and media</h2>
<p>
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 <a href="https://edulab.ifs.tuwien.ac.at/programme/volksschule-algorithmen/">workshops for school children at TU Wien</a>, 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 (<a href="talks/2022-10-18-Paris-Seminar/2022-Oct-Paris-gender-gap-CS.pdf">slides</a>). In June 2022 I participated at a round table about the profession of a scientist, organized by Slovenian national radio station Val 202 (<a
href="https://val202.rtvslo.si/podkast/frekvenca-x/31057643/174877423">audio</a>). From September 2019 to January 2022 I posed <a href="uganke.html">mathematical riddles</a> at the science show <a href="https://4d.rtvslo.si/oddaja/ugriznimo_znanost/65345770">Ugriznimo znanost</a> on Slovenian national television RTVSLO.
In March 2020 I gave an interview for Metina Lista science podcasts (<a
href="https://metinalista.si/meta-phodcast-110-anja-petkovic-matematicarka/">audio</a>) and in November 2019 an interview at the occasion of 100. anniversary of University of Ljubljana on Slovenian national radio station Val 202 (<a href="https://val202.rtvslo.si/2019/10/frekvenca-x-170/">audio</a>). In December 2018 I co-organised a round table called Women in Science and Technology (<a href="http://videolectures.net/single_okrogla_miza_zenske_v_znanosti/">video.</a>) with the collegues from Jožef Stefan Institute.
</p>
</article>
</div>
</section>
<!-- <section class="dark" id="participation">
<h1>Conference and Worksop participation</h1>
<div class="main">
<article>
<ul style="font-size: medium; align-items: baseline;">
<li>July 2021: HoTT/UF 2021, Online</li>
<li>June 2021: TYPES 2021, Online</li>
<li>April 2021: EPIT spring school, Online</li>
<li>July 2020: ICMS 2020, Online</li>
<li>June 2020: HoTTEST conference 2020, Online</li>
<li>December 2019: Workshop on Foundations and Applications of Univalent Mathematics, Herrsching, Germany</li>
<li>September 2019: Women in Mathematics on Mediterranean Shores, Bled, Slovenia</li>
<li>August 2019: Homotopy Type Theory 2019 Summer school and conference, Pittsburgh, Pennsylvania, USA</li>
<li>June 2019: TYPES 2019, Oslo, Norway</li>
<li>April 2019: UniMath spring school, Birmingham, UK</li>
<li>January 2019: POPL 2019, Cascais, Portugal</li>
<li>October 2018: EUTypes2018 meeting, Aarhus, Denmark</li>
<li>September 2018: Autumn school "Proof and Computation", Fischbachau, Germany</li>
<li>August 2018: Dagstuhl seminar "Formalization of Mathematics in Type Theory", Dagstuhl, Germany</li>
<li>July 2018: EuroScience Open Forum 2018, Toulouse, France</li>
<li>June 2018: Toposes in Como, summer school, Como, Italy</li>
<li>May 2018: Types, Sets and Constructions - Workshop: Types, Homotopy Type theory, and Verification, Bonn,
Germany</li>
<li>May 2018: Non-commutative structures 2018, Pororož, Slovenia</li>
<li>December 2017: UniMath winter school, Birmingham, UK </li>
<li>July 2017: EUTypes summer school, Ohrid, Macedonia</li>
<li>June 2017: MFPS & CALCO 2017, Ljubljana, Slovenia</li>
</ul>
</article>
</div>
</section> -->
</main>
</body>
</html>