Matija Pretnar: Symmetric programming

Abstract: In computer science, symmetry in data structures, such as binary search trees, is sometimes handled with clever tricks that merge symmetric cases, but even more often by duplicating code. In the seminar, we will explore an approach based on group actions, which captures symmetric constructions directly and uniformly. The approach also generalizes proofs relying on the principle of "without loss of generality," an established technique whose precise computational meaning is becoming increasingly important with the growing use of formal proof assistants.