Andrej Bauer

V svojem delu raziskujem povezave med matematiko in račulništvom. Zanimajo me naslednja področja:

Raziskovalni projekti

Objave

Znanstveni članki:

Znanstvena predavanja:

Bibliografija:

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