Andrej Bauer: Učinkovito računanje z Dedekindovimi realnimi števili

Povzetek: Običajne implementacije za računanje z eksaktnimi realnimi števili uporabljajo (izpeljanke) Cauchyevih realnih števil, ki so definirana kot Cauchyeva zaporedja racionalnih približkov. Predstavil bom nov način računanja z realnimi števili, kjer za osnovno definicijo vzamemo Dedekindovo konstrukcijo realnih števil z rezi racionalnih števil. Programski jezik, ki smo ga razvili in tudi implementirali, omogoča računanje z rezi, kakor tudi evaluacijo logičnih izrazov s kvantifikatorji.