Konferenzartikel: M - eine typisierte, funktionale Sprache für das Programmieren-im-Großen

Programmieren-im-Großen (PG) kann man als typisiertes, funktionales Programmieren verstehen. Um diese Denkweise programmiersprachlich zu unterstützen, haben wir M, eine typisierte, funktionale Sprache für das PG, entwickelt. In M bilden Module die elementaren Werte und Schnittstellen die elementaren Typen; funktionale Ausdrücke beschreiben die Komponenten von Familien von Software-Systemen. Durch Reduktion der Ausdrücke werden Komponenten zu einzelnen Software-Systemen kombiniert und gebunden. Grundlage von M ist ein erweiterter Lambda-Kalkül, der die Instanziierung von Modulen syntaktisch explizit macht. Schnittstellen sind als dependent types formalisiert, und die operationale Semantik ist durch Reduktionsregeln definiert. Diese Arbeit skizziert M und in der gebotenen Kürze den zugrundeliegenden Modulkalkül.