IFL 2012 - Invited speaker
Fritz Henglein, from the Department of Computer Science at the University of Copenhagen, is the invited speaker of IFL 2012. Fritz Henglein's research interests are in semantic, logical and algorithmic aspects of programming languages, specifically type inference, type-based program analysis, algorithmic functional programming and domain-specific languages, and the application of programming language technology, presently in enterprise systems (Project 3gERP and health care process modeling (Project TrustCare).
After undergraduate studies at Technische Universität München, he obtained his Ph.D. from Rutgers University and joined New York University, Utrecht University and DIKU, the Department of Computer Science at the University of Copenhagen. After starting Hafnium ApS to keep the Y2K bug at bay and being on the start-up faculty of the IT University of Copenhagen to increase IT proficiency, he rejoined DIKU as professor with special duties in programming languages. He is now head of the algorithms and programming languages group at DIKU. His goal is to contribute to the development of software that comes with technical and legal guarantees of having no defects (which should be considered a very modest ambition indeed).
Invited talk title
Have your cake and eat it, too: Generic sorting and partitioning in linear time and fully abstractly—simultaneously
Abstract
Discrimination is a generalization of both sorting and partitioning: It partitions list elements according to a user-specifiable equivalence or ordering relation and, for ordering relations, lists the resulting blocks in ascending order. We show how discriminators (discrimination functions) can be defined generically by structural recursion on representations of ordering and equivalence relations. They improve the asymptotic performance of generic comparison-based sorting and partitioning and yet do not to expose more information about the input elements than their pairwise ordering, respectively equivalence relation. For a large class of order and equivalence representations, including all standard orders for regular recursive first-order types, the discriminators execute in worst-case linear time.
The generic discriminators can be coded compactly using list comprehensions, with order and equivalence representations specified using Generalized Algebraic Data Types (GADTs). We give examples of the uses of discriminators, including most-significant-digit lexicographic sorting, type isomorphism with an associative-commutative operator, and database joins.
Since practical efficiency requires a thread-local bucket table reused by all same-thread discriminator calls we argue that built-in primitive types, notably pointers (references), should come with efficient discriminators since they, in contrast to binary comparison operations or hashing functions, facilitate the construction of discriminators for abstract types that are both highly efficient and representation independent.