V svojem delu raziskujem povezave med matematiko in računalništvom. Zanimajo me naslednja področja:
- osnove matematike in logika
- konstruktivna in izračunljiva matematika
- homotopska teorija tipov
- matematične osnove programskih jezikov
- eksaktno znanstveno računanje
Življenjepis · ORCID 0000-0001-5378-0547
Raziskovalni projekti
- Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE), vodja projekta, Renaissance Philanthropy
- Type Theory for Data-Intensive Formalization (TyDiForm), vodja projekta, Air Force Office of Scientific Research
- Računsko intenzivne metode, član, Agencija Republike Slovenije za raziskave in razvoj
Objave
Glej stran Objave za celotno bibliografijo in povezave do izbranih člankov.
Predavanja
Glej stran Predavanja za izbor lekcij in predavanj s konferenc.
Programska oprema
- Andromeda
- Dokazovalnik z uporabniško določenimi teorijami tipov.
- Eff
- Funkcijski programski jezik z algebraičnimi učinki in prestrezniki.
- Programming Languages Zoo
- Zbirka miniaturnih programskih jezikov za učenje načrtovanja in implementacije programskih jezikov.
- Marshall
- Programski jezik za eksaktno realno aritmetiko, zasnovan na Dedekindovih realnih številih.
- Coop
- Prototipni programski jezik za programiranje s tekači (komodeli).
- Alg
- Program za enumeracijo končnih modelov enosortnih teorij prvega reda.
- RZ
- Orodje za avtomatsko generiranje programskih specifikacij iz matematičnih teorij.
- Analytica
- Avtomatski dokazovalnik implementiran v Mathematici.
- repozitoriji in gisti
- Ostali projekti na GitHub.
Formalizirana matematika
- HoTT library
- Knjižnica HoTT je formalizacija homotopske teorije tipov v dokazovalnem pomočniku Coq.
- General type theories
- Formalizacija splošnih teorij tipov v dokazovalniku Coq.