Konstruktive Mathematik ist Mathematik ohne die Verwendung des Prinzips tertium non datur. Es gibt eine Vielzahl unterschiedlicher Modelle für die konstruktive Logik. Eine bestimmte Interpretation der konstruktiven Mathematik ist die Realisierbarkeits-Interpretation. Sie findet Anwendung als ein metamathematisches Werkzeug welches es gestattet, zulässige Regeln oder Äquikonsistenzaussagen für logische Kalküle nachzuweisen. In dieser Dissertation verwenden wir die Realisierbarkeits-Interpretation zum Zwecke der Separierung verschiedener Aussagen über Stetig- keit im Rahmen der konstruktiven Mathematik. Eine Eigenart einiger konstruktiver Formalismen ist die Prädikativität. Prädikative Logik verbietet die Definition einer Menge durch Quantifikation über eine Familie von Mengen, welche die zu definierende Menge enthält. Ausgehend von Realisierbarkeits-Modellen über einer getypten Version partieller kombinatorischer Algebren zeigen wir, dass die zugehörigen Modelle die nötigen Eigenschaften zur Interpretation im- prädikativer Logik und Typ Theorie genau dann besitzen, wenn die zugrundeliegende partielle kombinatorische Algebra äquivalent ist zu einer ungetypten pca. Der Wechsel zwischen den Welten der konstruktiven und der klassischen Mathematik und der Versuch, die konstruktive Logik als eine Methode zu benutzen, um Resultate zu erzielen, welche von Interesse für klassische Mathematiker sind, ist ein wiederkehrendes Thema dieser Dissertation. Ein klassischer Mathematiker erkennt sehr Wohl den Wert eines Lösungsalgorithmus im Vergleich zu einem bloßen Beweis der Existenz einer Lösung, aber er wird gewöhnlich nicht darauf bestehen, dass der Korrektheitsbeweis für den Algorithmus konstruktiv ist. Wir führen eine Klasse von Formeln ein, welche diesen pragmatischen Blickwinkel erfassen soll. Die Klasse ist derart definiert, dass Existenzaussagen einen starken Status haben, Korrektheitsbeweise für Operationen jedoch nur klassisch geführt werden brauchen. Die besagte Klasse von Formeln enthält nur klassisch wahre Formeln. Wir stellen die Axiomatisierung dieser Klasse als ein Problem und bieten Teilergebnisse. Wie die Rekursionstheorie, so ist auch die berechenbare Analysis ein Zweig der klassischen Mathematik. Die berechenbare Analysis wendet das Konzept der Berechenbarkeit an auf Größen der Analysis, indem sie sie mit einer Verallgemeinerung von Gödelisierungen, genannt Darstellungen, ausstattet. Darstellungen können in einer Realisierbarkeits-Kategorie mit reichhaltigen logischen Eigenschaften zusammengefasst werden. Auf diesem Wege können natürliche Darstellungen von Räumen gefunden werden, indem man die Beschreibung der unterliegenden Menge der Räume kategoriell interpretiert. Berechenbarkeits- und Nicht-Berechenbarkeitsresultate können so auf einer abstrakten, logischen Ebene hergeleitet werden. Zuletzt wenden wir uns einer weiteren Anwedung der Realisierbarkeitsmodelle zu, nämlich dem Gebiet der starken Normalisierungbeweise für typtheoretische Kalküle. Wir legen dar warum wir denken, dass der modified realizability topos nicht das geeignete Modell für diesen Zweck ist und schlagen eine Alternative vor.