The Programming Systems Lab at Saarland University led by Gert Smolka was founded in 1990 when Gert Smolka came to Saarbrücken as a research director at DFKI (until 1998) and a professor in Computer Science at Saarland University. We developed the programming systems Mozart (concurrent constraint programming) and Alice (concurrent functional programming) and contributed to the design of the Gecode Constraint Library. We also developed constraint-based methods and tools for the syntactic and semantic processing of natural language. Another important line of research has been the development and verification of computationally efficient tableaux systems for modal logics (PDL, CTL) and simple type theory. Since 2010 our focus has been on interactive theorem proving using the Coq system and formalization and verification in computational type theory.
Publications Teaching Software Formalizations
People who worked at the Programming Systems Lab (1990-2023)