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 vseh člankov.
Predavanja
- Znanstvena predavanja na blogu
- Video posnetki predavanj na YouTube (nekatera predavanja so samo na blogu)
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.