My primary research areas are parallel and functional programming, covering foundations, program analysis, language design and (parallel) implementation, as well as applications especially in embedded systems, FinTech, and health informatics. I am designing and implementing programming languages for easy-to-use parallelism, exploiting multi-cores and clusters of multi-cores, e.g. Glasgow parallel Haskell (GpH), Glasgow distributed Haskell (GdH), and mobile Haskell (mHaskell). GpH is a parallel extension of Haskell that requires only minimal code changes to introduce parallelism. Language design is combined with program analysis and program verification to enhance performance and security, e.g. by providing formal guarantees on resource bounds (e.g. the Camelot language for resource-safe mobile code).
More recently I have expanded my research areas to also cover: (1) computer security (Secrious project, EP/T017511/1), specifically using serious games for explaining security challenges; (2) AI, specifically high-performance machine-learning for FinTech (BA grant + industry funded PhD), and (3) health informatics, specifically Brain-computer-interfaces (EPSRC proposal).
My research vision is one of formally-grounded design of effective and efficient complex systems. The design of such systems should build on formal foundations, such as type systems and program logics, and use formalisations in provers such as Isabelle/HOL to achieve a high degree of dependability and to be provably effective. To be efficient the system should support, as an essential ingredient, modern computer architectures such as multi- and many-core machines in-the-small and grid- and cloud-architectures in-the-large. This vision is exemplified, by using cost information of a granularity analysis to guide the management of parallelism in GpH; by using formally-driven program transformations to enhance the performance of parallel functional programs; by developing a proof-carrying-code infrastructure to assure bounded space consumption of mobile code; by jointly developing and implementing resource analyses for embedded systems programs, and using the resource bounds in compilation and in specialised resource logics for certification.
See a complete list of Hans-Wolfgang Loidl's publications.
I am a member of the dependable systems group in the School of Mathematical and Computer Sciences of Heriot-Watt University. I am looking for potential PhD students in any of the areas described above. Visit my home page for contact details.