Einführung in Denotational Design, Teil III: Einführung in Agda

Dieser Artikel ist der dritte einer Reihe über Denotational Design. In diesem Artikel lernen wir Agda kennen. Agda ist eine Programmiersprache mit einem sehr ausdrucksstarken Typsystem. Es lassen sich mit Agda fast beliebige formale Aussagen als Typen ausdrücken. Implementierungen – Werte dieser Typen – werden dadurch zu Beweisen, die zeigen, dass diese Aussagen auch zutreffend sind. Wir legen uns im folgenden das Beispiel mit den binären Numeralen aus dem ersten Artikel vor und formalisieren es in Agda. Im nächsten Artikel wenden wir die hier dargestellten Inhalte auf unser Praxisbeispiel mit den Zeitreihen an.

Weiterlesen...

Eine Einführung in Denotational Design Teil II: Zeitreihen

Dieser Artikel ist der zweite einer Serie von Artikeln über Denotational Design. Im vorherigen Teil dieser Reihe hatten wir die theoretische Grundlage von Denotational Design kennen gelernt: Die denotationelle Semantik. In diesem Artikel wollen wir dieses Werkzeug nutzen, um eine konkrete Fachlichkeit zu spezifizieren.

Weiterlesen...

Tutorialtag: einen Tag voll funktionaler Programmierung mit der Active Group

Funktionale Programmierung ist vielseitig und vielschichtig. Bei der Active Group haben wir über alle Mitarbeiter:innen verteilt eine Menge Fachwissen in verschiedensten Bereichen der funktionalen Programmierung angesammelt und uns überlegt, eine Veranstaltung zu organisieren, bei der wir die Möglichkeit bieten, in die unterschiedlichen Bereiche und Sprachen einmal hineinzuschnuppern. Die Form: ein Tutorialtag am 18.04.2024 von 9-18 Uhr, online – zwölf anderthalbstündige Tutorials mit den FP-Expert:innen der Active Group und zum Abschluss ein Ask-Me-Anything mit Dr. Michael Sperber.

Weiterlesen...

Einführung in Denotational Design, Teil I: Denotationelle Semantik

Dieser Artikel ist der Beginn einer Reihe über Denotational Design. In diesem Artikel geht es um die denotationelle Semantik. Im nächsten Artikel wenden wir die hier dargestellte Theorie auf ein Praxisbeispiel an.

Weiterlesen...

Rezension von Sandy Maguire: Algebra-Driven Design

Maguires Buch handelt von Domänenmodellierung mit Algebra und funktionaler Programmierung, oder, anders gesagt, vom konzipieren von Kombinatormodellen. Dieses Thema ist bereits in zahllosen Papers gut untersucht worden, angefangen (vermutlich) mit Peter Hendersons Functional Geometry [Henderson(1982)].

Weiterlesen...