V svojem delu raziskujem povezave med matematiko in račulniš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
Raziskovalni projekti
- Type Theory for Data-Intensive Formalization (TyDiForm), nosilec projekta, Air Force Office of Scientific Research
- Računsko intenzivne metode, član, Agencija Republike Slovenije za raziskave in razvoj
Objave
Znanstveni članki:
- članki na math.andrej.com
- članki na arXiv.org
Znanstvena predavanja:
- predavanja na math.andrej.com
- posnetki predavanj na YouTube
Bibliografija:
- uradna bibliografija COBISS
- DBLP
- Google scholar
- MathSciNet (lahko zahteva avtentikacijo)
- ORCID 0000-0001-5378-0547
Blog:
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.
Programska oprema
- Coop
- Programski jezik za programiranje s tekači, oziroma komodeli.
- Andromeda
- Andromeda je implementacija teorije odvisnih tipov z refleksijo enakosti. Ta teorija tipov je zelo ekspresivna, saj omogoča dodajanje novih sodbenih enakosti.
- Eff
- Eff je funkcijski programski jezik s splošnimi prestrezniki, ki poleg izjem prestrezajo tudi druge računske učinke, kot so stanje in vhod/izhod. S prestrezniki lahko implementiramo transakcije, preusmerjanje, sestopanje, večopravilnost, in mnoge ostale programske konstrukte.
- Programming Languages Zoo
- Programming Languages Zoo je zbirka miniaturnih programskih jezikov, ki prikazuje različne koncepte in tehnike načrtovanja in implementacije programskih jezikov. Je primerna odskočna deska za vse, ki želijo implementirati svoj programski jezik, ali se samo naučiti, kako se to dela.
- Marshall
- Marshall je programski jezik za eksaktno realno aritmetiko, zasnovan na idejah iz abstraktne Stoneove dualnosti.
- Alg
- Alg je program za enumeracijo končnih modelov enosortnih teorij prvega reda. Te vsebujejo grupe, kolobarje, obsege, mreže, delne ureditve, grafe, in mnoge druge.
- RZ
- RZ je orodje za avtomatsko generiranje programskih specifikacij iz matematičnih teorij. S tem RZ omogoča programerjem in matematikom načrtovanje podatkovnih struktur, ki pravilno implementirajo matematične strukture (algebre, realna števila, Hilbertove propstore ipd.)
- Analytica
- Avtomatski dokazovalnik implementiran v Mathematici.
- repozitoriji in gisti
- ostali projekti na GitHub