Typentheorie in der Praxis

Die Typsysteme moderner Programmiersprachen können nicht nur zwischen Zahlen und Zeichen unterscheiden, sondern sind leistungsfähig genug, um Programminvarianten auszudrücken. So wird es Entwicklerinnen und Entwicklern ermöglicht, ganze Klassen von Fehlern zu erkennen, bevor der Code überhaupt ausgeführt wird. Dieser Vortrag zeigt, wie sich typentheoretische Ideen in praktische Software-Engineering-Techniken übersetzen lassen: von der direkten Kodierung von Nebenbedingungen im Typensystem bis hin zum Einsatz von Verfeinerungs- und abhängigen Typen für eine leichtgewichtige formale Verifikation. Diese Methoden sind längst keine akademischen Kuriositäten mehr, sondern etablieren sich im Mainstream über verschiedene Programmiersprachen und Industrien hinweg.

Referent:
Kai Lothar John entwickelt seit vielen Jahren Software, von Luftverkehrssystemen bis zu komplexen C4I-Anwendungen, für die Zuverlässigkeit und Korrektheit entscheidend sind. Er bringt anspruchsvolle technische Konzepte in den Praxisalltag von Teams und zeigt, wie bereits einfache typgetriebene formale Methoden die Softwareentwicklung klarer, sicherer und wartbarer machen. Darüber hinaus ist er in internationalen Standardisierungsorganisationen aktiv und verbindet so moderne Softwarepraktiken mit regulatorischen Anforderungen. Kai begeistert sich dafür, Entwicklerinnen und Entwickler dafür zu gewinnen, wie stärkere Typen und rigoroses Design den Alltag in der Programmierung verbessern können.