Wie lernt man am besten Agda – Eine Quellen­sammlung

Im letzten Artikel der Denotational-Design-Reihe hatten wir die Programmiersprache bzw. den Theorembeweiser Agda kennen gelernt. In diesem kleinen Einschub stelle ich einige Ressourcen vor, mithilfe derer man seine Agda- und Dependent-Typing-Skills vertiefen kann. Ich stelle die Ressourcen in einer Reihenfolge vor, von der ich denke, dass sich diese für mich gut zum Lernen geeignet hätte.

Weiterlesen...

BOB 2024 – Retrospektive

Am 15.03.2023 feierte die BOB, unsere alljährliche Entwickler:innenkonferenz, ihre elfte Ausgabe. Diesmal im Scandic-Hotel Potsdamer Platz, Berlin, eine Location, die einige schon von der SommerBOB 2019 kannten. Bereits am Vorabend hatten sich die ersten zu einem lockeren Austausch bei Pizza und Bier getroffen – vielen Dank an dieser Stelle an NewStore GmbH für die Einladung und die Organisation!

Weiterlesen...

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...